Last updated: 2017-08-02 10:37:53 +0100

Upstream URL: git clone http://chriswarbo.net/git/haskell-te.git


View repository

View issue tracker

Contents of follows

Haskell Theory Exploration

This repository is designed to allow reproducible experiments in theory exploration, in the Haskell language. Many separate tools are used in this implementation, tied together using the Nix expression language.

Quick Summary


The files ending .smt2 in the benchmarks directory are theories which will be benchmarked. They are as follows:

Each file has a partner in benchmarks/ground-truth containing the statements considered "interesting" for that theory.

More extensive benchmarking is performed using the TE Benchmarks project, which includes a corpus of definitions and statements. Subsets of these definitions are sampled (deterministically), and the applicable statements are used as the ground truth.

We use asv to run the benchmarks and manage the results. Use asv run to run them, asv publish to generate a HTML report, etc.

Note that benchmarking can take a while. In particular, there's a large up-front cost as we gather all results during the 'setup' phase; the benchmark functions themselves (defined in benchmarks/*.py) are fast since they just extract data from these results.

Our policy is to commit benchmark results (which will include the raw input/output data and specs of the machine) to git to ensure reproducibility. We don't commit the HTML reports, since they can be generated automatically. When committing new results, keep in mind that the raw data can get quite large, and these will hang around forever in git. Hence only include those which are reliable (e.g. don't run benchmarks at the same time as other resource-intensive programs).


 Johansson, Dan Rosén and Nicholas Smallbone 2013
 Roy McCasland, Lucas Dixon and Alan Bundy 2012