1. Source code is packaged and distributed as a MSI executable (sic!). Luckily, it can be unarchived using Wine:<p># theoremDistrib url = https://download.microsoft.com/download/D/1/D/D1D6FCF9-4D04-49FE-9952-0D295B180CF4/4ct.msi<p>HOME=$TMPDIR wine msiexec /qn /i ${theoremDistrib} TARGETDIR=$out<p>2. 4CT is proved originally in Coq v7.3.1, however the distributed source code is adapted for Coq v8 (exact version not specified).<p>All Coq version are available at https://coq.inria.fr/distrib/<p>3. Building Coq v8.1 is easy, according to documentation. The only thing is, it requires Ocaml v.3.07 or later<p><pre><code> - Objective Caml version 3.07 or later
(available at http://caml.inria.fr/)
</code></pre>
And we know what does it mean "... or later". Go grab 3.07 otherwise it won't compile.<p>4. Another problem is ssreflect library. Quoting proof's README:<p>"The required extension package, named "ssreflect" (for "small-scale
reflection") is distributed separately. It consists of a single extended ML
(.ml4) file, which compiles to a library that must be linked with the Coq
system, using either the -load-ml-object command line switch (for bytecode
systems, not recommended) or, preferably, the coqmktop utility to produce
a new Coq system binary. The definition of the COQC variable in the Makefile
should be adjusted to refer to this new system (it defaults to ./ssrcoq.exe).<p><pre><code> Note that this directory contains a copy of the vernacular files needed to</code></pre>
support the ssreflect extensions (ssreflect.v and ssrbool.v)."<p>So 0) get Ocaml 1) build Coq, 2) build another Coq using coqmktop and those two files 3) compile proof<p>---<p>Overall this results in a pretty long reproducibility chain. Can you capture this chain, without making patches to original proof?