aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ci')
-rw-r--r--dev/ci/nix/CoLoR.nix5
-rw-r--r--dev/ci/nix/CompCert.nix7
-rw-r--r--dev/ci/nix/Corn.nix5
-rw-r--r--dev/ci/nix/Elpi.nix4
-rw-r--r--dev/ci/nix/GeoCoq.nix5
-rw-r--r--dev/ci/nix/HoTT.nix6
-rw-r--r--dev/ci/nix/VST.nix6
-rw-r--r--dev/ci/nix/bedrock2.nix5
-rw-r--r--dev/ci/nix/bignums.nix5
-rw-r--r--dev/ci/nix/coq.nix9
-rw-r--r--dev/ci/nix/coq_dpdgraph.nix7
-rw-r--r--dev/ci/nix/cross_crypto.nix5
-rw-r--r--dev/ci/nix/default.nix72
-rw-r--r--dev/ci/nix/fiat_crypto.nix6
-rw-r--r--dev/ci/nix/fiat_crypto_legacy.nix6
-rw-r--r--dev/ci/nix/flocq.nix7
-rw-r--r--dev/ci/nix/math_classes.nix6
-rw-r--r--dev/ci/nix/mtac2.nix5
-rw-r--r--dev/ci/nix/oddorder.nix4
-rwxr-xr-xdev/ci/nix/shell20
-rw-r--r--dev/ci/nix/unicoq.nix14
21 files changed, 209 insertions, 0 deletions
diff --git a/dev/ci/nix/CoLoR.nix b/dev/ci/nix/CoLoR.nix
new file mode 100644
index 0000000000..4c5cfd83da
--- /dev/null
+++ b/dev/ci/nix/CoLoR.nix
@@ -0,0 +1,5 @@
+{ bignums }:
+
+{
+ buildInputs = [ bignums ];
+}
diff --git a/dev/ci/nix/CompCert.nix b/dev/ci/nix/CompCert.nix
new file mode 100644
index 0000000000..db1721e5f5
--- /dev/null
+++ b/dev/ci/nix/CompCert.nix
@@ -0,0 +1,7 @@
+{ ocamlPackages }:
+
+{
+ buildInputs = with ocamlPackages; [ ocaml findlib menhir ];
+ configure = "./configure -ignore-coq-version x86_64-linux";
+ make = "make all check-proof";
+}
diff --git a/dev/ci/nix/Corn.nix b/dev/ci/nix/Corn.nix
new file mode 100644
index 0000000000..18c7750279
--- /dev/null
+++ b/dev/ci/nix/Corn.nix
@@ -0,0 +1,5 @@
+{ bignums, math-classes }:
+
+{
+ buildInputs = [ bignums math-classes ];
+}
diff --git a/dev/ci/nix/Elpi.nix b/dev/ci/nix/Elpi.nix
new file mode 100644
index 0000000000..0a6ed20295
--- /dev/null
+++ b/dev/ci/nix/Elpi.nix
@@ -0,0 +1,4 @@
+{ ocamlPackages }:
+{
+ buildInputs = with ocamlPackages; [ ocaml findlib elpi ];
+}
diff --git a/dev/ci/nix/GeoCoq.nix b/dev/ci/nix/GeoCoq.nix
new file mode 100644
index 0000000000..a86fb2c44a
--- /dev/null
+++ b/dev/ci/nix/GeoCoq.nix
@@ -0,0 +1,5 @@
+{ mathcomp }:
+{
+ buildInputs = [ mathcomp ];
+ configure = "./configure.sh";
+}
diff --git a/dev/ci/nix/HoTT.nix b/dev/ci/nix/HoTT.nix
new file mode 100644
index 0000000000..dea0aeeb55
--- /dev/null
+++ b/dev/ci/nix/HoTT.nix
@@ -0,0 +1,6 @@
+{ autoconf, automake }:
+{
+ buildInputs = [ autoconf automake ];
+ configure = "./autogen.sh && ./configure";
+ make = "make all validate";
+}
diff --git a/dev/ci/nix/VST.nix b/dev/ci/nix/VST.nix
new file mode 100644
index 0000000000..3e2629a0b6
--- /dev/null
+++ b/dev/ci/nix/VST.nix
@@ -0,0 +1,6 @@
+{}:
+
+rec {
+ make = "make IGNORECOQVERSION=true";
+ clean = "${make} clean";
+}
diff --git a/dev/ci/nix/bedrock2.nix b/dev/ci/nix/bedrock2.nix
new file mode 100644
index 0000000000..552d9297e2
--- /dev/null
+++ b/dev/ci/nix/bedrock2.nix
@@ -0,0 +1,5 @@
+{}:
+{
+ configure = "git submodule update --init --recursive";
+ clean = "(cd deps/bbv && make clean); (cd deps/riscv-coq && make clean); (cd compiler && make clean); (cd bedrock2 && make clean)";
+}
diff --git a/dev/ci/nix/bignums.nix b/dev/ci/nix/bignums.nix
new file mode 100644
index 0000000000..1d931c858e
--- /dev/null
+++ b/dev/ci/nix/bignums.nix
@@ -0,0 +1,5 @@
+{ ocamlPackages }:
+
+{
+ buildInputs = with ocamlPackages; [ ocaml findlib camlp5 ];
+}
diff --git a/dev/ci/nix/coq.nix b/dev/ci/nix/coq.nix
new file mode 100644
index 0000000000..ecd280e58d
--- /dev/null
+++ b/dev/ci/nix/coq.nix
@@ -0,0 +1,9 @@
+{ stdenv, callPackage, branch, wd }:
+
+let coq = callPackage wd { buildDoc = false; doInstallCheck = false; coq-version = "8.9"; }; in
+
+coq.overrideAttrs (o: {
+ name = "coq-local-${branch}";
+ src = fetchGit "${wd}";
+ enableParallelBuilding = true;
+})
diff --git a/dev/ci/nix/coq_dpdgraph.nix b/dev/ci/nix/coq_dpdgraph.nix
new file mode 100644
index 0000000000..611e2fcca5
--- /dev/null
+++ b/dev/ci/nix/coq_dpdgraph.nix
@@ -0,0 +1,7 @@
+{ autoconf, ocamlPackages }:
+
+{
+ buildInputs = [ autoconf ] ++ (with ocamlPackages; [ ocaml findlib camlp5 ocamlgraph ]);
+ configure = "autoconf && ./configure";
+ make = "make all test-suite";
+}
diff --git a/dev/ci/nix/cross_crypto.nix b/dev/ci/nix/cross_crypto.nix
new file mode 100644
index 0000000000..98f74f9474
--- /dev/null
+++ b/dev/ci/nix/cross_crypto.nix
@@ -0,0 +1,5 @@
+{}:
+{
+ configure = "git submodule update --init --recursive";
+ clean = "make cleanall";
+}
diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
new file mode 100644
index 0000000000..4acfae48e4
--- /dev/null
+++ b/dev/ci/nix/default.nix
@@ -0,0 +1,72 @@
+{ pkgs ? import <nixpkgs> {}
+, branch
+, wd
+, project ? "xyz"
+, bn ? "release"
+}:
+
+with pkgs;
+
+# Coq from this directory
+let coq = callPackage ./coq.nix { inherit branch wd; }; in
+
+# Third-party libraries, built with this Coq
+let coqPackages = mkCoqPackages coq; in
+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 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
+ { src = fetchTarball bn; }
+ ); in
+let coqprime = coqPackages.coqprime.override { inherit coq bignums; }; in
+let math-classes =
+ (coqPackages.math-classes.override { inherit coq bignums; })
+ .overrideAttrs (o: {
+ src = fetchTarball "https://github.com/coq-community/math-classes/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
+
+# Environments for building CI libraries with this Coq
+let projects = {
+ bedrock2 = callPackage ./bedrock2.nix {};
+ bignums = callPackage ./bignums.nix {};
+ CoLoR = callPackage ./CoLoR.nix {};
+ CompCert = callPackage ./CompCert.nix {};
+ coq_dpdgraph = callPackage ./coq_dpdgraph.nix {};
+ Corn = callPackage ./Corn.nix {};
+ cross_crypto = callPackage ./cross_crypto.nix {};
+ Elpi = callPackage ./Elpi.nix {};
+ fiat_crypto = callPackage ./fiat_crypto.nix {};
+ fiat_crypto_legacy = callPackage ./fiat_crypto_legacy.nix {};
+ flocq = callPackage ./flocq.nix {};
+ GeoCoq = callPackage ./GeoCoq.nix {};
+ HoTT = callPackage ./HoTT.nix {};
+ math_classes = callPackage ./math_classes.nix {};
+ mathcomp = {};
+ mtac2 = callPackage ./mtac2.nix {};
+ oddorder = callPackage ./oddorder.nix {};
+ VST = callPackage ./VST.nix {};
+}; in
+
+if !builtins.hasAttr project projects
+then throw "Unknown project “${project}”; choose from: ${pkgs.lib.concatStringsSep ", " (builtins.attrNames projects)}."
+else
+
+let prj = projects."${project}"; in
+
+stdenv.mkDerivation {
+ name = "shell-for-${project}-in-${branch}";
+
+ buildInputs = [ coq ] ++ (prj.buildInputs or []);
+
+ configure = prj.configure or "true";
+ make = prj.make or "make";
+ clean = prj.clean or "make clean";
+
+}
diff --git a/dev/ci/nix/fiat_crypto.nix b/dev/ci/nix/fiat_crypto.nix
new file mode 100644
index 0000000000..7b37e6e8e4
--- /dev/null
+++ b/dev/ci/nix/fiat_crypto.nix
@@ -0,0 +1,6 @@
+{ coqprime }:
+{
+ buildInputs = [ coqprime ];
+ configure = "git submodule update --init --recursive && ulimit -s 32768";
+ make = "make new-pipeline c-files";
+}
diff --git a/dev/ci/nix/fiat_crypto_legacy.nix b/dev/ci/nix/fiat_crypto_legacy.nix
new file mode 100644
index 0000000000..3248665579
--- /dev/null
+++ b/dev/ci/nix/fiat_crypto_legacy.nix
@@ -0,0 +1,6 @@
+{}:
+
+{
+ configure = "./etc/ci/remove_autogenerated.sh";
+ make = "make print-old-pipeline-lite old-pipeline-lite lite-display";
+}
diff --git a/dev/ci/nix/flocq.nix b/dev/ci/nix/flocq.nix
new file mode 100644
index 0000000000..e153043557
--- /dev/null
+++ b/dev/ci/nix/flocq.nix
@@ -0,0 +1,7 @@
+{ autoconf, automake }:
+
+{
+ buildInputs = [ autoconf automake ];
+ configure = "./autogen.sh && ./configure";
+ make = "./remake";
+}
diff --git a/dev/ci/nix/math_classes.nix b/dev/ci/nix/math_classes.nix
new file mode 100644
index 0000000000..b0fa2fe795
--- /dev/null
+++ b/dev/ci/nix/math_classes.nix
@@ -0,0 +1,6 @@
+{ bignums }:
+
+{
+ buildInputs = [ bignums ];
+ configure = "./configure.sh";
+}
diff --git a/dev/ci/nix/mtac2.nix b/dev/ci/nix/mtac2.nix
new file mode 100644
index 0000000000..9a2353c5cf
--- /dev/null
+++ b/dev/ci/nix/mtac2.nix
@@ -0,0 +1,5 @@
+{ coq, unicoq }:
+{
+ buildInputs = [ unicoq ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 ]);
+ configure = "./configure.sh";
+}
diff --git a/dev/ci/nix/oddorder.nix b/dev/ci/nix/oddorder.nix
new file mode 100644
index 0000000000..3b8fdbab51
--- /dev/null
+++ b/dev/ci/nix/oddorder.nix
@@ -0,0 +1,4 @@
+{ mathcomp }:
+{
+ buildInputs = [ mathcomp ];
+}
diff --git a/dev/ci/nix/shell b/dev/ci/nix/shell
new file mode 100755
index 0000000000..2e4462ed40
--- /dev/null
+++ b/dev/ci/nix/shell
@@ -0,0 +1,20 @@
+#!/usr/bin/env sh
+
+## This file should be run from the root of the Coq source tree
+
+BRANCH=$(git rev-parse --abbrev-ref HEAD)
+echo "Branch: $BRANCH in $PWD"
+
+if [ "$#" -ne 1 ]; then
+ PROJECT=""
+else
+ PROJECT="--argstr project $1"
+fi
+
+if [ "$BN" ]; then
+ BN="--argstr bn ${BN}"
+else
+ BN=""
+fi
+
+nix-shell ./dev/ci/nix/ --show-trace --argstr wd $PWD --argstr branch $BRANCH $PROJECT $BN
diff --git a/dev/ci/nix/unicoq.nix b/dev/ci/nix/unicoq.nix
new file mode 100644
index 0000000000..f10afd5680
--- /dev/null
+++ b/dev/ci/nix/unicoq.nix
@@ -0,0 +1,14 @@
+{ stdenv, fetchzip, coq }:
+
+stdenv.mkDerivation {
+ name = "coq${coq.coq-version}-unicoq-0.0-git";
+ src = fetchzip {
+ url = "https://github.com/vbgl/unicoq/archive/8b33e37700e92bfd404bf8bf9fe03f1be8928d97.tar.gz";
+ sha256 = "0s4z0wjxlp56ccgzxgk04z7skw90rdnz39v730ffkgrjl38rr9il";
+ };
+
+ buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 num ]);
+
+ configurePhase = "coq_makefile -f Make -o Makefile";
+ installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
+}
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:28:05 +0000