The Proverbot9001 comparison numbers were run using our own infrastructure, not the extracted CoqGym data. As a result, we were only able to run on projects that supported Coq 8.10, 8.11, or 8.12. Unless otherwise noted, projects were run using Coq 8.11.0.
| Project | Status |
|---|---|
| "weak-up-to" | Success |
| "buchberger" | Success (git) |
| "jordan-curve-theorem" | Success (git, Coq 8.10) |
| "dblib" | Success |
| "disel" | Success |
| "zchinese" | Success (git, "v8.9" branch) |
| "zfc" | Success |
| "dep-map" | Success |
| "chinese" | Success |
| "UnifySL" | Success (Coq 8.10.2) |
| "hoare-tut" | Success (git) |
| "huffman" | Success |
| "PolTac" | Success (Coq 8.12.0) |
| "angles" | Success |
| "coq-procrastination" | Success (git) |
| "coq-library-undecidability" | Success |
| "tree-automata" | Success (Coq 8.10.1) |
| "coquelicot" | Success (updated, skip linearizing theories/SF_seq.v) |
| "fermat4" | Success (git,b) |
| "demos" | Success |
| "coqoban" | Success |
| "goedel" | Success (Coq 8.10) |
| "verdi-raft" | Success |
| "verdi" | Success (git) |
| "zorns-lemma" | Success (git) |
| "coqrel" | Failed: Coq Anomaly "Uncaught exception Option.IsNone" |
| "fundamental-arithmetics" | Success |