This page contains pointers to the detailed results, logs, Coq problem files and conversion programs for the evaluations of the proof search procedure from the paper:
L. Czajka: Practical proof search for Coq by type inhabitation.
The proof search procedure described in the paper is implemented as a component of CoqHammer (src/tactics/ and theories/Tactics/ directories). The version used for our evaluations (modulo minor changes) is in the sauto branch.
All evaluations were performed on a 48-core server with 2.2GHz AMD Opteron CPUs and 320GB RAM. Each problem was always assigned one CPU core.
At the end of the theories/Tactics/Tactics.v file there are the tactics we used for the standalone evaluations: fcrush (our procedure), ecrush (combination of Coq tactics), ccrush (Chlipala's crush). These tactics combine appropriate tactics with unfolding and induction. The old preliminary version of our procedure combined with unfolding and induction (Reconstr.fcrush) is at the end of theories/Tactics/Reconstr.v.
The tactics used for the "raw" standalone evaluation without induction or unfolding are also present in the above files. See the READMEs in the result files.
The names of the 12 variants of the tactics used for reconstruction can be found here. The code of the tactics is in the theories/Tactics/Tactics.v file.
The first file above also contains the conversion programs and instructions on how to replicate the evaluation.
The first file above also contains the conversion programs and instructions on how to replicate the evaluation.
The three variants of our procedure used for the ILTP evaluation are in the theories/Tactics/Tactics.v file: hprover, tprover, syelles.
All converted Coq problems for the evaluations on the collection of Coq developments and on CompCert may be also found in the repository https://github.com/lukaszcz/coqhammer-eval (together with a few other converted developments which we didn't evaluate).