[Nix-ci] Fix Unicoq

4 files changed, 55 insertions, 1 deletions

diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
index ac4894dfd3..35f44f8e84 100644
--- a/dev/ci/nix/default.nix
+++ b/dev/ci/nix/default.nix
@@ -33,7 +33,7 @@ let corn = (coqPackages.corn.override { inherit coq bignums math-classes; })
     src = fetchTarball "https://github.com/coq-community/corn/archive/master.tar.gz";
   }); in
 
-let unicoq = callPackage ./unicoq.nix { inherit coq; }; in
+let unicoq = callPackage ./unicoq { inherit coq; }; in
 
 let callPackage = newScope { inherit coq mathcomp bignums coqprime corn math-classes unicoq; }; in
 
diff --git a/dev/ci/nix/unicoq/META b/dev/ci/nix/unicoq/META
new file mode 100644
index 0000000000..30dd8b5559
--- /dev/null
+++ b/dev/ci/nix/unicoq/META
@@ -0,0 +1,2 @@
+archive(native) = "unicoq.cmxa"
+plugin(native) = "unicoq.cmxs"
diff --git a/dev/ci/nix/unicoq.nix b/dev/ci/nix/unicoq/default.nix
index 093c262cde..36f40dbe33 100644
--- a/dev/ci/nix/unicoq.nix
+++ b/dev/ci/nix/unicoq/default.nix
@@ -4,8 +4,16 @@ stdenv.mkDerivation {
   name = "coq${coq.coq-version}-unicoq-0.0-git";
   src = fetchTarball https://github.com/unicoq/unicoq/archive/master.tar.gz;
 
+  patches = [ ./unicoq-num.patch ];
+
   buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 num ]);
 
   configurePhase = "coq_makefile -f Make -o Makefile";
   installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
+
+  postInstall = ''
+    install -d $OCAMLFIND_DESTDIR
+    ln -s $out/lib/coq/${coq.coq-version}/user-contrib/Unicoq $OCAMLFIND_DESTDIR/
+    install -m 0644 ${./META} src/unicoq.a $OCAMLFIND_DESTDIR/Unicoq
+  '';
 }
diff --git a/dev/ci/nix/unicoq/unicoq-num.patch b/dev/ci/nix/unicoq/unicoq-num.patch
new file mode 100644
index 0000000000..6d96d94dfc
--- /dev/null
+++ b/dev/ci/nix/unicoq/unicoq-num.patch
@@ -0,0 +1,44 @@
+commit f29bc64ee3d8b36758d17e1f5d50812e0c93063b
+Author: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
+Date:   Thu Nov 29 08:59:22 2018 +0000
+
+    Make explicit dependency to num
+
+diff --git a/Make b/Make
+index 550dc6a..8aa1309 100644
+--- a/Make
++++ b/Make
+@@ -9,7 +9,7 @@ src/logger.ml
+ src/munify.mli
+ src/munify.ml
+ src/unitactics.mlg
+-src/unicoq.mllib
++src/unicoq.mlpack
+ theories/Unicoq.v
+ test-suite/munifytest.v
+ test-suite/microtests.v
+diff --git a/Makefile.local b/Makefile.local
+new file mode 100644
+index 0000000..88be365
+--- /dev/null
++++ b/Makefile.local
+@@ -0,0 +1 @@
++CAMLPKGS += -package num
+diff --git a/src/unicoq.mllib b/src/unicoq.mllib
+deleted file mode 100644
+index 2b84e2d..0000000
+--- a/src/unicoq.mllib
++++ /dev/null
+@@ -1,3 +0,0 @@
+-Logger
+-Munify
+-Unitactics
+diff --git a/src/unicoq.mlpack b/src/unicoq.mlpack
+new file mode 100644
+index 0000000..2b84e2d
+--- /dev/null
++++ b/src/unicoq.mlpack
+@@ -0,0 +1,3 @@
++Logger
++Munify
++Unitactics