Skip to content

Instantly share code, notes, and snippets.

Keshav Kini kini

Block or report user

Report or block kini

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
@kini
kini / acl2-cert-dimmer-for-comint.el
Last active May 23, 2018
An Emacs snippet for ACL2 certification in shell buffers
View acl2-cert-dimmer-for-comint.el
;; ACL2 certification dimmer function
(defun acl2-cert-dimmer-for-comint (str)
"When cert.pl says it has certified something, go back and
dim the text where it said it was making that thing. This way
you can easily tell at a glance what books are still certifying."
(let ((pos-in-str nil)
;; This is broken; comint-last-input-end isn't really the
;; end of the last input. I should probably search to the
;; previous prompt, or something.
(beginning-of-output comint-last-input-end))
@kini
kini / foo.bib
Last active Nov 21, 2016
minimal org-ref example
View foo.bib
@article{greenwade93,
author = "George D. Greenwade",
title = "The {C}omprehensive {T}ex {A}rchive {N}etwork ({CTAN})",
year = "1993",
journal = "TUGBoat",
volume = "14",
number = "3",
pages = "342--351"
}
@kini
kini / permute.c
Last active Jun 13, 2016
Heap's algorithm for iterating over permutations of n
View permute.c
#include <stdlib.h>
#include <stdio.h>
#include <string.h>
#include <stdbool.h>
bool print_permutation(unsigned int n,
unsigned int permutation[n],
unsigned int count[n]) {
printf("Permutation: [");
for (unsigned int i = 0; i < n; i++) {
@kini
kini / bash_aliases.sh
Last active Jun 7, 2016
better random numbers for bash
View bash_aliases.sh
random () {
# note: $RANDOM only gives 15 bits of entropy, and the apparently
# commonly used $RANDOM$RANDOM is non-uniform as it misses such
# numbers as 4294967295. This command will grab 4 bytes from
# /dev/urandom, interpret them as a 4-byte unsigned integer, and
# format them in decimal representation. It can be used as a
# replacement for $RANDOM when you want a full 32 bits of entropy.
od -An -t u4 -N4 < /dev/urandom | tr -d '[[:space:]]'
}
export -f random
@kini
kini / lab3.org
Last active Oct 28, 2015
README for Lab 3, CS 429 Fall 2015
View lab3.org

Compiler Lab: Generating Assembly Code

Introduction

  • Assigned: Oct. 14
  • Due: Oct. 30, 11:59 PM

Note: Keshav Kini (krkini@utexas.edu) is the lead TA for this lab assignment.

View lab2.org

Bomb Lab: Defusing a Binary Bomb

Introduction

  • Assigned: Sep. 28
  • Due: Oct. 12

Note: Keshav Kini (krkini@utexas.edu) is the lead TA for this lab assignment.

@kini
kini / reverselike.org
Last active Aug 29, 2015
ReverseLike in ACL2 with constrained functions
View reverselike.org

ReverseLike in ACL2 with constrained functions

This document describes a toy example of how ACL2’s “constrained functions” feature can be used to verify some higher-order statements, despite ACL2 being a first-order theorem prover.

Suppose we have a function called $reverse$ which when applied to a list returns a list containing the same elements in reverse order. Consider the following proposition.

View keybase.md

Keybase proof

I hereby claim:

  • I am kini on github.
  • I am kini (https://keybase.io/kini) on keybase.
  • I have a public key whose fingerprint is 75ED 46F8 A0C4 C645 32AB B79D 7492 7B7C A81A 950F

To claim this, I am signing this object:

View test-against-newest-dependency.sh
#!/bin/bash
set -ex
PACKAGE="$1"
DEPENDENCY="$2"
TMPDIR="$(mktemp -d)"
pushd "$TMPDIR"
cabal get --pristine "$PACKAGE"
@kini
kini / configure.output
Last active Aug 29, 2015
GHC 7.8.2 building on GHC 7.8.3
View configure.output
checking for gfind... no
checking for find... /usr/bin/find
checking for sort... /usr/bin/sort
checking for ghc... /opt/ghc/7.8.3/bin/ghc
checking version of ghc... 7.8.3
checking build system type... x86_64-unknown-linux-gnu
checking host system type... x86_64-unknown-linux-gnu
checking target system type... x86_64-unknown-linux-gnu
Build platform inferred as: x86_64-unknown-linux
Host platform inferred as: x86_64-unknown-linux
You can’t perform that action at this time.