From bb1ad2a59f0c9c6b62a1c70023a9ee31866b9a01 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Thu, 29 Nov 2018 17:01:47 +0000 Subject: [Nix-ci] Add formal-topology --- dev/ci/nix/default.nix | 10 ++++++++-- dev/ci/nix/formal-topology.nix | 4 ++++ 2 files changed, 12 insertions(+), 2 deletions(-) create mode 100644 dev/ci/nix/formal-topology.nix (limited to 'dev') diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix index 4acfae48e4..ac4894dfd3 100644 --- a/dev/ci/nix/default.nix +++ b/dev/ci/nix/default.nix @@ -2,7 +2,7 @@ , branch , wd , project ? "xyz" -, bn ? "release" +, bn ? "master" }: with pkgs; @@ -28,9 +28,14 @@ let math-classes = src = fetchTarball "https://github.com/coq-community/math-classes/archive/master.tar.gz"; }); in +let corn = (coqPackages.corn.override { inherit coq bignums math-classes; }) + .overrideAttrs (o: { + src = fetchTarball "https://github.com/coq-community/corn/archive/master.tar.gz"; + }); in + let unicoq = callPackage ./unicoq.nix { inherit coq; }; in -let callPackage = newScope { inherit coq mathcomp bignums coqprime math-classes unicoq; }; in +let callPackage = newScope { inherit coq mathcomp bignums coqprime corn math-classes unicoq; }; in # Environments for building CI libraries with this Coq let projects = { @@ -45,6 +50,7 @@ let projects = { fiat_crypto = callPackage ./fiat_crypto.nix {}; fiat_crypto_legacy = callPackage ./fiat_crypto_legacy.nix {}; flocq = callPackage ./flocq.nix {}; + formal-topology = callPackage ./formal-topology.nix {}; GeoCoq = callPackage ./GeoCoq.nix {}; HoTT = callPackage ./HoTT.nix {}; math_classes = callPackage ./math_classes.nix {}; diff --git a/dev/ci/nix/formal-topology.nix b/dev/ci/nix/formal-topology.nix new file mode 100644 index 0000000000..70ba541577 --- /dev/null +++ b/dev/ci/nix/formal-topology.nix @@ -0,0 +1,4 @@ +{ corn }: +{ + buildInputs = [ corn ]; +} -- cgit v1.2.3 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 +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 From 43525f9ee12a40bf3ad2c2521832fd7fc3a658f8 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Mon, 3 Dec 2018 15:31:52 +0000 Subject: [Nix-ci] Add QuickChick --- dev/ci/nix/default.nix | 11 ++++++++++- dev/ci/nix/quickchick.nix | 5 +++++ 2 files changed, 15 insertions(+), 1 deletion(-) create mode 100644 dev/ci/nix/quickchick.nix (limited to 'dev') diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix index 35f44f8e84..2c6e5b37bc 100644 --- a/dev/ci/nix/default.nix +++ b/dev/ci/nix/default.nix @@ -16,6 +16,11 @@ let mathcomp = coqPackages.mathcomp.overrideAttrs (o: { name = "coq-git-mathcomp-git"; src = fetchTarball https://github.com/math-comp/math-comp/archive/master.tar.gz; }); in +let ssreflect = coqPackages.ssreflect.overrideAttrs (o: { + inherit (mathcomp) src; + }); in +let coq-ext-lib = coqPackages.coq-ext-lib; in +let simple-io = coqPackages.simple-io; in let bignums = coqPackages.bignums.overrideAttrs (o: if bn == "release" then {} else if bn == "master" then { src = fetchTarball https://github.com/coq/bignums/archive/master.tar.gz; } else @@ -35,7 +40,10 @@ let corn = (coqPackages.corn.override { inherit coq bignums math-classes; }) let unicoq = callPackage ./unicoq { inherit coq; }; in -let callPackage = newScope { inherit coq mathcomp bignums coqprime corn math-classes unicoq; }; in +let callPackage = newScope { inherit coq + bignums coq-ext-lib coqprime corn math-classes + mathcomp simple-io ssreflect unicoq; +}; in # Environments for building CI libraries with this Coq let projects = { @@ -57,6 +65,7 @@ let projects = { mathcomp = {}; mtac2 = callPackage ./mtac2.nix {}; oddorder = callPackage ./oddorder.nix {}; + quickchick = callPackage ./quickchick.nix {}; VST = callPackage ./VST.nix {}; }; in diff --git a/dev/ci/nix/quickchick.nix b/dev/ci/nix/quickchick.nix new file mode 100644 index 0000000000..b057160cb8 --- /dev/null +++ b/dev/ci/nix/quickchick.nix @@ -0,0 +1,5 @@ +{ ocamlPackages, ssreflect, coq-ext-lib, simple-io }: +{ + buildInputs = [ ssreflect coq-ext-lib simple-io ] + ++ (with ocamlPackages; [ ocaml findlib ocamlbuild num ]); +} -- cgit v1.2.3 From dec2994980e00eff72f474aed6da94b97c3d703a Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Thu, 24 Jan 2019 09:58:33 +0000 Subject: [nix-CI] Split the build inputs Coq and the Coq libraries can now be excluded (by setting the NOCOQ environment variable). --- dev/ci/nix/CoLoR.nix | 2 +- dev/ci/nix/Corn.nix | 2 +- dev/ci/nix/GeoCoq.nix | 2 +- dev/ci/nix/README.md | 7 +++++++ dev/ci/nix/default.nix | 9 ++++++++- dev/ci/nix/fiat_crypto.nix | 2 +- dev/ci/nix/formal-topology.nix | 2 +- dev/ci/nix/math_classes.nix | 2 +- dev/ci/nix/mtac2.nix | 3 ++- dev/ci/nix/oddorder.nix | 2 +- dev/ci/nix/quickchick.nix | 4 ++-- dev/ci/nix/shell | 8 +++++++- 12 files changed, 33 insertions(+), 12 deletions(-) (limited to 'dev') diff --git a/dev/ci/nix/CoLoR.nix b/dev/ci/nix/CoLoR.nix index 4c5cfd83da..3fcf177aec 100644 --- a/dev/ci/nix/CoLoR.nix +++ b/dev/ci/nix/CoLoR.nix @@ -1,5 +1,5 @@ { bignums }: { - buildInputs = [ bignums ]; + coqBuildInputs = [ bignums ]; } diff --git a/dev/ci/nix/Corn.nix b/dev/ci/nix/Corn.nix index 18c7750279..0d22a6b91b 100644 --- a/dev/ci/nix/Corn.nix +++ b/dev/ci/nix/Corn.nix @@ -1,5 +1,5 @@ { bignums, math-classes }: { - buildInputs = [ bignums math-classes ]; + coqBuildInputs = [ bignums math-classes ]; } diff --git a/dev/ci/nix/GeoCoq.nix b/dev/ci/nix/GeoCoq.nix index a86fb2c44a..45d688285e 100644 --- a/dev/ci/nix/GeoCoq.nix +++ b/dev/ci/nix/GeoCoq.nix @@ -1,5 +1,5 @@ { mathcomp }: { - buildInputs = [ mathcomp ]; + coqBuildInputs = [ mathcomp ]; configure = "./configure.sh"; } diff --git a/dev/ci/nix/README.md b/dev/ci/nix/README.md index 1685b084e9..6f32abef95 100644 --- a/dev/ci/nix/README.md +++ b/dev/ci/nix/README.md @@ -17,3 +17,10 @@ build-system of that project: `configure`, `make`, and `clean`. Therefore, after changing the working directory to the root of the sources of that project, the contents of these variables can be evaluated to respectively set-up, build, and clean the project. + +## Variant: nocoq + +The dependencies of the third-party developments are split into `buildInputs` +and `coqBuildInputs`. The second list gathers the Coq libraries. In case you +only want the non-coq dependencies (because you want to use Coq from your `PATH`), +set the environment variable `NOCOQ` to some non-empty value. diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix index 2c6e5b37bc..277e9ee08f 100644 --- a/dev/ci/nix/default.nix +++ b/dev/ci/nix/default.nix @@ -2,6 +2,7 @@ , branch , wd , project ? "xyz" +, withCoq ? true , bn ? "master" }: @@ -75,10 +76,16 @@ else let prj = projects."${project}"; in +let inherit (stdenv.lib) optional optionals; in + stdenv.mkDerivation { name = "shell-for-${project}-in-${branch}"; - buildInputs = [ coq ] ++ (prj.buildInputs or []); + buildInputs = + optional withCoq coq + ++ (prj.buildInputs or []) + ++ optionals withCoq (prj.coqBuildInputs or []) + ; configure = prj.configure or "true"; make = prj.make or "make"; diff --git a/dev/ci/nix/fiat_crypto.nix b/dev/ci/nix/fiat_crypto.nix index 7b37e6e8e4..0f0ee91387 100644 --- a/dev/ci/nix/fiat_crypto.nix +++ b/dev/ci/nix/fiat_crypto.nix @@ -1,6 +1,6 @@ { coqprime }: { - buildInputs = [ coqprime ]; + coqBuildInputs = [ coqprime ]; configure = "git submodule update --init --recursive && ulimit -s 32768"; make = "make new-pipeline c-files"; } diff --git a/dev/ci/nix/formal-topology.nix b/dev/ci/nix/formal-topology.nix index 70ba541577..53b9b1182b 100644 --- a/dev/ci/nix/formal-topology.nix +++ b/dev/ci/nix/formal-topology.nix @@ -1,4 +1,4 @@ { corn }: { - buildInputs = [ corn ]; + coqBuildInputs = [ corn ]; } diff --git a/dev/ci/nix/math_classes.nix b/dev/ci/nix/math_classes.nix index b0fa2fe795..8edc3c8358 100644 --- a/dev/ci/nix/math_classes.nix +++ b/dev/ci/nix/math_classes.nix @@ -1,6 +1,6 @@ { bignums }: { - buildInputs = [ bignums ]; + coqBuildInputs = [ bignums ]; configure = "./configure.sh"; } diff --git a/dev/ci/nix/mtac2.nix b/dev/ci/nix/mtac2.nix index 9a2353c5cf..4acc326c02 100644 --- a/dev/ci/nix/mtac2.nix +++ b/dev/ci/nix/mtac2.nix @@ -1,5 +1,6 @@ { coq, unicoq }: { - buildInputs = [ unicoq ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 ]); + buildInputs = with coq.ocamlPackages; [ ocaml findlib camlp5 ]; + coqBuildInputs = [ unicoq ]; configure = "./configure.sh"; } diff --git a/dev/ci/nix/oddorder.nix b/dev/ci/nix/oddorder.nix index 3b8fdbab51..2341bb3173 100644 --- a/dev/ci/nix/oddorder.nix +++ b/dev/ci/nix/oddorder.nix @@ -1,4 +1,4 @@ { mathcomp }: { - buildInputs = [ mathcomp ]; + coqBuildInputs = [ mathcomp ]; } diff --git a/dev/ci/nix/quickchick.nix b/dev/ci/nix/quickchick.nix index b057160cb8..46bf02ae3c 100644 --- a/dev/ci/nix/quickchick.nix +++ b/dev/ci/nix/quickchick.nix @@ -1,5 +1,5 @@ { ocamlPackages, ssreflect, coq-ext-lib, simple-io }: { - buildInputs = [ ssreflect coq-ext-lib simple-io ] - ++ (with ocamlPackages; [ ocaml findlib ocamlbuild num ]); + buildInputs = with ocamlPackages; [ ocaml findlib ocamlbuild num ]; + coqBuildInputs = [ ssreflect coq-ext-lib simple-io ]; } diff --git a/dev/ci/nix/shell b/dev/ci/nix/shell index 2e4462ed40..a5f8ee8f54 100755 --- a/dev/ci/nix/shell +++ b/dev/ci/nix/shell @@ -17,4 +17,10 @@ else BN="" fi -nix-shell ./dev/ci/nix/ --show-trace --argstr wd $PWD --argstr branch $BRANCH $PROJECT $BN +if [ "$NOCOQ" ]; then + NOCOQ="--arg withCoq false" +else + NOCOQ="" +fi + +nix-shell ./dev/ci/nix/ --show-trace --argstr wd $PWD --argstr branch $BRANCH $PROJECT $BN $NOCOQ -- cgit v1.2.3