From 587f127e93481de02dd345d8b001935b453fcaf9 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Sun, 1 Mar 2015 17:22:34 +0100
Subject: [PATCH] coq-contribs: fix various packages

---
 pkgs/development/coq-modules/contribs/all.nix |  6 +-
 .../coq-modules/contribs/default.nix          | 57 ++++++++++++++++++-
 2 files changed, 58 insertions(+), 5 deletions(-)

diff --git a/pkgs/development/coq-modules/contribs/all.nix b/pkgs/development/coq-modules/contribs/all.nix
index fe01fbf5891..d01c32bdb0a 100644
--- a/pkgs/development/coq-modules/contribs/all.nix
+++ b/pkgs/development/coq-modules/contribs/all.nix
@@ -47,7 +47,7 @@ EuclideanGeometry = "11n8877zksgksdfcj7arjx0zcfhsrvg83lcp6yb2bynvfp80gyzb";
 EulerFormula = "1nhh49rf6wza2m5qmz5l5m24m299qn3v80wqzvf51lybadzll2h6";
 ExactRealArithmetic = "1p32g13sx2z5rj3q6390ym8902gvl5x16wdhgz5i75y44s6kmkb1";
 Exceptions = "0w2b16nr80f70dxllmhbqwfr1aw26rcfbak5bdyc0fna8hqp4q3p";
-#FOUnify = "1vwp5rwvs5ng4d13l9jjh4iljasfqmc5jpla8rga4v968bp84nw6";
+FOUnify = "1vwp5rwvs5ng4d13l9jjh4iljasfqmc5jpla8rga4v968bp84nw6";
 FSSecModel = "0fi78vqfrw4vrmdw215ic08rw8y6aia901wqs4f1s9z2idd6m8qy";
 FSets = "1n54s2vr6snh31jnvr79q951vyk0w0w6jrnwnlz9d3vyw47la9js";
 Fairisle = "0gg9x69qr0zflaryniqnl8d34kjdij0i55fcb1f1i5hmrwn2sqn6";
@@ -135,10 +135,10 @@ RulerCompassGeometry = "02vm80xvvw22pdxrag3pv5zrhqf8726i9jqsiv4bnjqavj5z2hdr";
 SMC = "0ca3ar1y9nyj5147r18babqsbg2q2ywws8fdi91xb5z9m3i97nv1";
 Schroeder = "0mfbjmw4a48758k88yv01494wnywcp5yamkl394axvvbbna9h8b6";
 SearchTrees = "1jyps6ddm8klmxjm50p2j9i014ij7imy3229pwz3dkzg54gxzzxb";
-#Semantics = "157db1y5zgxs9shl7rmqg89gxfa4cqxwlf6qys0jh3j0wsxs8580";
+Semantics = "157db1y5zgxs9shl7rmqg89gxfa4cqxwlf6qys0jh3j0wsxs8580";
 Shuffle = "14v1m4s9k49w30xrnyncjzgqjcckiga8wd2vnnzy8axrwr9zq7iq";
 SquareMatrices = "07dlykg3w59crc54qqdqxq6hf8rmzvwwfr1g8z8v2l8h4yvfnhfl";
-Ssreflect = "1capfvkdnsv95ik0yj9kpwj4smm7i7n2n98d6rlv68bdd2abw9f3";
+Ssreflect = "07hv0ixv68d8vrpf9s6gxazxaz5fwpmhqrd6cqw7xp8m8gspxifz";
 Stalmarck = "0vcbkzappq1si4hxbnb9bjkfk82j3jklb8g8ia83h1mdhzr7xdpz";
 Streams = "1spcqnvwayahk12fd13vzh922ypzrjkcmws9gcy12qdqp04h8bnc";
 String = "1wy7g66yq9y8m8y3gq29q7whfdm98g3cj9jxm5yibdzfahfdzzni";
diff --git a/pkgs/development/coq-modules/contribs/default.nix b/pkgs/development/coq-modules/contribs/default.nix
index fb231bfdeac..289a4d75921 100644
--- a/pkgs/development/coq-modules/contribs/default.nix
+++ b/pkgs/development/coq-modules/contribs/default.nix
@@ -4,6 +4,15 @@ let
   mkContrib = import ./mk-contrib.nix;
   all = import ./all.nix;
   overrides = {
+    Additions = self: {
+      patchPhase = ''
+        for p in binary_strat dicho_strat generation log2_implementation shift
+        do
+          substituteInPlace $p.v \
+          --replace 'Require Import Euclid.' 'Require Import Coq.Arith.Euclid.'
+        done
+      '';
+    };
     BDDs = self: {
       buildInputs = self.buildInputs ++ [ contribs.IntMap ];
       patchPhase = ''
@@ -13,6 +22,7 @@ let
         32d30
         < extraction
         EOF
+        coq_makefile -f Make -o Makefile
       '';
       postInstall = ''
         mkdir -p $out/bin
@@ -25,6 +35,7 @@ let
         17d16
         < rauzy/algorithme1/extraction
         EOF
+        coq_makefile -f Make -o Makefile
       '';
       postInstall = ''
         mkdir -p $out/bin
@@ -38,6 +49,7 @@ let
         2d1
         < -R ../QArithSternBrocot QArithSternBrocot
         EOF
+        coq_makefile -f Make -o Makefile
       '';
     };
     CoRN = self: {
@@ -47,7 +59,9 @@ let
         2d1
         < -R ../MathClasses/ MathClasses
         EOF
+        coq_makefile -f Make -o Makefile.coq
       '';
+      enableParallelBuilding = true;
       installFlags = self.installFlags + " -f Makefile.coq";
     };
     Counting = self: {
@@ -70,6 +84,7 @@ let
         < -I ../Counting/src
         < -R ../Counting/theories Counting
         EOF
+        coq_makefile -f Make -o Makefile
       '';
     };
     FingerTree = self: {
@@ -78,6 +93,22 @@ let
         21d20
         < extraction
         EOF
+        coq_makefile -f Make -o Makefile
+      '';
+    };
+    FOUnify = self: {
+      patchPhase = ''
+        patch Make <<EOF
+        8c8
+        < -custom "\$(CAMLOPTLINK) -pp '\$(CAMLBIN)\$(CAMLP4)o' -o unif unif.mli unif.ml main.ml" unif.ml unif
+        ---
+        > -custom "\$(CAMLOPTLINK) -pp 'camlp5o' -o unif unif.mli unif.ml main.ml" unif.ml unif
+        EOF
+        coq_makefile -f Make -o Makefile
+      '';
+      postInstall = ''
+        mkdir -p $out/bin
+        cp unif $out/bin/
       '';
     };
     Goedel = self: {
@@ -85,8 +116,9 @@ let
       patchPhase = ''
         patch Make <<EOF
         2d1
-	< -R ../../Eindhoven/Pocklington Pocklington
+        < -R ../../Eindhoven/Pocklington Pocklington
         EOF
+        coq_makefile -f Make -o Makefile
       '';
     };
     Graphs = self: {
@@ -96,6 +128,7 @@ let
         2d1
         < -R ../../Cachan/IntMap IntMap
         EOF
+        coq_makefile -f Make -o Makefile
       '';
       postInstall = ''
         mkdir -p $out/bin
@@ -110,6 +143,7 @@ let
         2d1
         < -R ../../Sophia-Antipolis/Algebra/ Algebra
         EOF
+        coq_makefile -f Make -o Makefile
       '';
     };
     Markov = self: { configurePhase = "coq_makefile -o Makefile -R . Markov markov.v"; };
@@ -129,6 +163,7 @@ let
         < -R ../../Sophia-Antipolis/Algebra Algebra
         < -R ../../Nijmegen/LinAlg LinAlg
         EOF
+        coq_makefile -f Make -o Makefile
       '';
     };
     PTSF = self: {
@@ -138,6 +173,7 @@ let
         1d0
         < -R ../../Paris/PTSATR/ PTSATR
         EOF
+        coq_makefile -f Make -o Makefile
       '';
     };
     RelationExtraction = self: {
@@ -146,6 +182,20 @@ let
         31d30
         < test
         EOF
+        coq_makefile -f Make -o Makefile
+      '';
+    };
+    Semantics = self: {
+      patchPhase = ''
+        patch Make <<EOF
+        18a19
+        > interp.mli
+        EOF
+      '';
+      configurePhase = ''
+        coq_makefile -f Make -o Makefile
+        make extract_interpret.vo
+        rm -f str_little.ml.d
       '';
     };
     SMC = self: {
@@ -155,12 +205,13 @@ let
         2d1
         < -R ../../Cachan/IntMap IntMap
         EOF
+        coq_makefile -f Make -o Makefile
       '';
     };
     Ssreflect = self: {
       patchPhase = ''
         substituteInPlace Makefile \
-	--replace "/bin/mkdir" "mkdir"
+        --replace "/bin/mkdir" "mkdir"
       '';
     };
     Stalmarck = self: {
@@ -173,6 +224,7 @@ let
         2d1
         < -R ../ZornsLemma ZornsLemma
         EOF
+        coq_makefile -f Make -o Makefile
       '';
     };
     TreeAutomata = self: {
@@ -182,6 +234,7 @@ let
         2d1
         < -R ../../Cachan/IntMap IntMap
         EOF
+        coq_makefile -f Make -o Makefile
       '';
     };
   };