From 736a425208ef526412a961e97e157b44eea050c5 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Mon, 3 Dec 2018 13:18:50 +0000
Subject: [Nix-ci] Fix Unicoq

---
 dev/ci/nix/default.nix             |  2 +-
 dev/ci/nix/unicoq.nix              | 11 ----------
 dev/ci/nix/unicoq/META             |  2 ++
 dev/ci/nix/unicoq/default.nix      | 19 ++++++++++++++++
 dev/ci/nix/unicoq/unicoq-num.patch | 44 ++++++++++++++++++++++++++++++++++++++
 5 files changed, 66 insertions(+), 12 deletions(-)
 delete mode 100644 dev/ci/nix/unicoq.nix
 create mode 100644 dev/ci/nix/unicoq/META
 create mode 100644 dev/ci/nix/unicoq/default.nix
 create mode 100644 dev/ci/nix/unicoq/unicoq-num.patch

(limited to 'dev')

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.nix b/dev/ci/nix/unicoq.nix
deleted file mode 100644
index 093c262cde..0000000000
--- a/dev/ci/nix/unicoq.nix
+++ /dev/null
@@ -1,11 +0,0 @@
-{ stdenv, coq }:
-
-stdenv.mkDerivation {
-  name = "coq${coq.coq-version}-unicoq-0.0-git";
-  src = fetchTarball https://github.com/unicoq/unicoq/archive/master.tar.gz;
-
-  buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 num ]);
-
-  configurePhase = "coq_makefile -f Make -o Makefile";
-  installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
-}
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/default.nix b/dev/ci/nix/unicoq/default.nix
new file mode 100644
index 0000000000..36f40dbe33
--- /dev/null
+++ b/dev/ci/nix/unicoq/default.nix
@@ -0,0 +1,19 @@
+{ stdenv, coq }:
+
+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
-- 
cgit v1.2.3