diff options
author | Vincent Laporte <Vincent.Laporte@gmail.com> | 2015-03-01 17:22:34 +0100 |
---|---|---|
committer | Vincent Laporte <Vincent.Laporte@gmail.com> | 2015-03-01 17:53:51 +0100 |
commit | 587f127e93481de02dd345d8b001935b453fcaf9 (patch) | |
tree | cdf0a1e25858af4605c75e18ec757f3a1f3a6294 /pkgs/development/coq-modules | |
parent | d8912db092aca760bbfcb31a9a51c0b12112ac7d (diff) | |
download | nixlib-587f127e93481de02dd345d8b001935b453fcaf9.tar nixlib-587f127e93481de02dd345d8b001935b453fcaf9.tar.gz nixlib-587f127e93481de02dd345d8b001935b453fcaf9.tar.bz2 nixlib-587f127e93481de02dd345d8b001935b453fcaf9.tar.lz nixlib-587f127e93481de02dd345d8b001935b453fcaf9.tar.xz nixlib-587f127e93481de02dd345d8b001935b453fcaf9.tar.zst nixlib-587f127e93481de02dd345d8b001935b453fcaf9.zip |
coq-contribs: fix various packages
Diffstat (limited to 'pkgs/development/coq-modules')
-rw-r--r-- | pkgs/development/coq-modules/contribs/all.nix | 6 | ||||
-rw-r--r-- | pkgs/development/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 fe01fbf58913..d01c32bdb0af 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 fb231bfdeac6..289a4d759214 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 ''; }; }; |