Skip to content

Instantly share code, notes, and snippets.

@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.