Skip to content

Instantly share code, notes, and snippets.

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.