Work log 2016-08-25

Annoyances building QuickSpec signatures. We have existing code in MLSpec (to write the sign code) and nix-eval (to wrap around the boilerplate) but they’re getting stuck with the fact that tip-benchmark-sig is not an element of the regular haskellPackages set.

Turns out we were also using an old nix-eval, which didn’t allow overriding the Haskell package set.

Used env vars to pass parameters around, which lets us short-circuit parts of the script. We could try doing it in bits instead?

quickspecBench now creates a Haskell package (from smtlib code), annotates it, extracts quickspecable functions, writes a QuickSpec signature, extends that signature with variables of the appropriate types and spits out a command to explore the generated signature, including the appropriate wrappers required to ensure Haskell packages, etc.

Whilst nix-shell is used in the wrapper, there is no embedded use (e.g. via nix-eval), so we can use bench as the top-level command in the nix-shell wrapper and benchmark the QuickSpec run at full speed.