Reproduce Gonthier Four Colour Theorem proof challenge (make no proof patches)

1 point

6 years ago

1. Source code is packaged and distributed as a MSI executable (sic!). Luckily, it can be unarchived using Wine:

# theoremDistrib url = https://download.microsoft.com/download/D/1/D/D1D6FCF9-4D04-49FE-9952-0D295B180CF4/4ct.msi

HOME=$TMPDIR wine msiexec /qn /i ${theoremDistrib} TARGETDIR=$out

2. 4CT is proved originally in Coq v7.3.1, however the distributed source code is adapted for Coq v8 (exact version not specified).

All Coq version are available at https://coq.inria.fr/distrib/

3. Building Coq v8.1 is easy, according to documentation. The only thing is, it requires Ocaml v.3.07 or later

     - Objective Caml version 3.07 or later
       (available at http://caml.inria.fr/)

And we know what does it mean "... or later". Go grab 3.07 otherwise it won't compile.

4. Another problem is ssreflect library. Quoting proof's README:

"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).

  Note that this directory contains a copy of the vernacular files needed to

support the ssreflect extensions (ssreflect.v and ssrbool.v)."

So 0) get Ocaml 1) build Coq, 2) build another Coq using coqmktop and those two files 3) compile proof

---

Overall this results in a pretty long reproducibility chain. Can you capture this chain, without making patches to original proof?