WIP reproduce the Four Color Theorem proof by Gonthier

4ct-proof.nix

#! /usr/bin/env nix-build
{ pkgs ? import (builtins.fetchTarball https://github.com/NixOS/nixpkgs/archive/2fa9bd50597c3089cc00abb3f20d7510fcc8ad6a.tar.gz) { }
}:
let
  inherit (pkgs) stdenv lib;
  theoremDistrib = pkgs.fetchurl {
    url = https://download.microsoft.com/download/D/1/D/D1D6FCF9-4D04-49FE-9952-0D295B180CF4/4ct.msi;
    sha256 = null;
  };
  theoremSrc = stdenv.mkDerivation {
    name = "four-color-theorem-src";
    buildInputs = [ pkgs.wine ];
    buildCommand = ''
      HOME=$TMPDIR wine msiexec /qn /i ${theoremDistrib} TARGETDIR=$out
    '';
  };
  proof = stdenv.mkDerivation {
    name = "four-color-theorem-proof";
    src = theoremSrc;
    patches = 
      let patchMake = pkgs.writeText "patchMake" ''
            diff --git a/Make b/Make
            index c375b89..1a8c600 100755
            --- a/Make
            +++ b/Make
            @@ -1 +1,4 @@
            -dedekind.v realcategorical.v fourcolor.v dbhub.v
            +fourcolor.v
            +realcategorical.v
            +dedekind.v
            +funs.v
          '';
          patchFuns = pkgs.writeText "patchFuns" ''
            diff --git a/funs.v b/funs.v
            index 2866c21..3a789cc 100755
            --- a/funs.v
            +++ b/funs.v
            @@ -10,12 +10,12 @@ Unset Strict Implicit.
             
             (* Shorthand for some basic equality lemmas lemmas. *)
             
            -Definition erefl := refl_equal.
            -Definition esym := sym_eq.
            -Definition nesym := sym_not_eq.
            -Definition etrans := trans_eq.
            -Definition congr1 := f_equal.
            -Definition congr2 := f_equal2.
            +Notation erefl := refl_equal.
            +Notation esym := sym_eq.
            +Notation nesym := sym_not_eq.
            +Notation etrans := trans_eq.
            +Notation congr1 := f_equal.
            +Notation congr2 := f_equal2.
             (* Force at least one implicit when used as a view. *)
             Prenex Implicits esym nesym.
 
          '';
          patchReal = pkgs.writeText "patchReal" ''
            diff --git a/real.v b/real.v
            index 4ec4f25..23a3e73 100755
            --- a/real.v
            +++ b/real.v
            @@ -17,6 +17,8 @@
             (* setoid rewriting in denominators -- it might be worth setting 1/0 = 0 to *)
             (* just to elude this problem.                                              *)
             
            +Require Import ssreflect.
            +
             Set Implicit Arguments.
             Unset Strict Implicit.
             Import Prenex Implicits.
          '';
      in [ patchMake patchReal patchFuns ];
    buildInputs = with pkgs; [ coq coqPackages.ssreflect ];
    configurePhase = ''
      rm -rf ssreflect* &&
      rm -rf ssrbool* &&    
      coq_makefile -f Make -o Makefile
    '';
  };
in proof