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 / 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 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 / foo.bib
Last active Nov 21, 2016
minimal org-ref example
View foo.bib
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 / 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 /
Last active Jun 7, 2016
better random numbers for bash
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 /
Last active Oct 28, 2015
README for Lab 3, CS 429 Fall 2015

Compiler Lab: Generating Assembly Code


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

Note: Keshav Kini ( is the lead TA for this lab assignment.


Bomb Lab: Defusing a Binary Bomb


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

Note: Keshav Kini ( is the lead TA for this lab assignment.

kini /
Last active Aug 29, 2015
ReverseLike in ACL2 with constrained functions

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.


Keybase proof

I hereby claim:

  • I am kini on github.
  • I am 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:

set -ex
TMPDIR="$(mktemp -d)"
pushd "$TMPDIR"
cabal get --pristine "$PACKAGE"
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.