Skip to content

Instantly share code, notes, and snippets.

View tchajed's full-sized avatar

Tej Chajed tchajed

354 followers · 16 following
View GitHub Profile
@tchajed
tchajed / _verus_to_smt2.sh
Last active July 30, 2024 19:09
Generate SMT2 from Verus
#!/bin/sh
verus --log smt example.rs
# output is in .verus-log/root.smt2
# alternately, consider --log-all (the VIR and AIR may be useful)
@tchajed
tchajed / _dafny_to_smt2.sh
Last active October 18, 2023 16:13
Getting SMT2 verification condition from Dafny
#!/bin/sh
dafny verify --solver-log example.smt2 --boogie /normalizeNames:0 example.dfy
@tchajed
tchajed / iris-release.sh
Last active April 12, 2024 10:19
Script to release Iris and std++
#!/usr/bin/env bash
# iris-release.sh prepares a commit for https://github.com/coq/opam to
# add a new version of std++ and Iris to the Coq opam repository.
#
# Requires a clone of opam-coq-archive. The opam files from std++ and Iris are
# retrieved by downloading their releases by tag.
set -eu
@tchajed
tchajed / bash-colors.sh
Created April 7, 2020 15:28
ANSI escapes for colors in bash
#!/bin/bash
info() {
echo -e "\033[34m$1\033[0m"
}
error() {
echo -e "\033[31m$1\033[0m"
}
@tchajed
tchajed / iteration.dfy
Created October 15, 2019 15:31
Iterating over sequences and sets in Dafny
method sum_seq(xs: seq<int>) returns (z:int) {
var sum := 0;
var i := 0;
while i < |xs|
invariant i <= |xs|
{
sum := sum + xs[i];
i := i + 1;
}
return sum;
@tchajed
tchajed / args.sh
Last active June 26, 2024 14:52
Starting a bash script
#!/bin/bash
# basic manual argument parsing
usage() {
echo "Usage: $0 [--foo FOO] [-v]" 1>&2
}
foo=""
verbose=false
@tchajed
tchajed / svimrc
Last active September 17, 2019 12:20
let blacklists = ["https://mail.google.com/*", "https://docs.google.com/document/*]
let newtab = "https://www.google.com"
@tchajed
tchajed / keybase.md
Created September 16, 2019 15:23

Keybase proof

I hereby claim:

  • I am tchajed on github.
  • I am tchajed (https://keybase.io/tchajed) on keybase.
  • I have a public key ASBxd3t8HGdTAbKbOqOp5jrcJk3pusQbgsd5umQdsV0NTgo

To claim this, I am signing this object:

@tchajed
tchajed / RecordUpdater.v
Last active July 23, 2018 19:53
Small library for creating record updaters in Coq
Definition Reader E T := E -> T.
Definition get {E} : Reader E E := fun e => e.
Definition pure {E T} (x:T) : Reader E T := fun _ => x.
Definition ap {E A B} (f: Reader E (A -> B)) : Reader E A -> Reader E B :=
fun x => fun e => f e (x e).
Infix "<*>" := (ap) (at level 11, left associativity).
@tchajed
tchajed / man.fish
Last active August 19, 2016 15:34 — forked from supermarin/.env
Colored `man` pages on OS X
# Fish users
# Save this file as ~/.config/fish/functions/man.fish
function man
env \
LESS_TERMCAP_mb=\e"[1;31m" \
LESS_TERMCAP_md=\e"[1;31m" \
LESS_TERMCAP_me=\e"[0m" \
LESS_TERMCAP_se=\e"[0m" \
LESS_TERMCAP_so=\e"[1;44;33m" \