Back to results

Testing Projects Status

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