aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rwxr-xr-xdev/ci/ci-bedrock2.sh2
-rwxr-xr-xdev/ci/ci-fiat_parsers.sh (renamed from dev/ci/ci-fiat-parsers.sh)0
-rw-r--r--dev/ci/nix/default.nix16
-rw-r--r--dev/ci/nix/iris.nix4
-rw-r--r--dev/ci/nix/lambda-rust.nix4
-rw-r--r--dev/ci/nix/unicoq/META2
-rw-r--r--dev/ci/nix/unicoq/default.nix11
-rw-r--r--dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh9
-rw-r--r--dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh6
-rw-r--r--dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh6
-rw-r--r--dev/ci/user-overlays/09172-ejgallego-proof_rework.sh9
-rw-r--r--dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh9
-rw-r--r--dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh6
-rw-r--r--dev/ci/user-overlays/09263-maximedenes-parsing-state.sh12
-rw-r--r--dev/core_dune.dbg2
-rw-r--r--dev/doc/release-process.md6
-rw-r--r--dev/top_printers.mli1
17 files changed, 48 insertions, 57 deletions
diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh
index 5205946261..2ac78d3c2b 100755
--- a/dev/ci/ci-bedrock2.sh
+++ b/dev/ci/ci-bedrock2.sh
@@ -6,4 +6,4 @@ ci_dir="$(dirname "$0")"
FORCE_GIT=1
git_download bedrock2
-( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && make )
+( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make )
diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat_parsers.sh
index ac74ebf667..ac74ebf667 100755
--- a/dev/ci/ci-fiat-parsers.sh
+++ b/dev/ci/ci-fiat_parsers.sh
diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
index 277e9ee08f..94e0a666e2 100644
--- a/dev/ci/nix/default.nix
+++ b/dev/ci/nix/default.nix
@@ -39,11 +39,21 @@ let corn = (coqPackages.corn.override { inherit coq bignums math-classes; })
src = fetchTarball "https://github.com/coq-community/corn/archive/master.tar.gz";
}); in
+let stdpp = coqPackages.stdpp.overrideAttrs (o: {
+ src = fetchTarball "https://gitlab.mpi-sws.org/iris/stdpp/-/archive/master/stdpp-master.tar.bz2";
+ }); in
+
+let iris = (coqPackages.iris.override { inherit coq stdpp; })
+ .overrideAttrs (o: {
+ src = fetchTarball "https://gitlab.mpi-sws.org/iris/iris/-/archive/master/iris-master.tar.bz2";
+ propagatedBuildInputs = [ stdpp ];
+ }); in
+
let unicoq = callPackage ./unicoq { inherit coq; }; in
let callPackage = newScope { inherit coq
- bignums coq-ext-lib coqprime corn math-classes
- mathcomp simple-io ssreflect unicoq;
+ bignums coq-ext-lib coqprime corn iris math-classes
+ mathcomp simple-io ssreflect stdpp unicoq;
}; in
# Environments for building CI libraries with this Coq
@@ -62,6 +72,8 @@ let projects = {
formal-topology = callPackage ./formal-topology.nix {};
GeoCoq = callPackage ./GeoCoq.nix {};
HoTT = callPackage ./HoTT.nix {};
+ iris = callPackage ./iris.nix {};
+ lambda-rust = callPackage ./lambda-rust.nix {};
math_classes = callPackage ./math_classes.nix {};
mathcomp = {};
mtac2 = callPackage ./mtac2.nix {};
diff --git a/dev/ci/nix/iris.nix b/dev/ci/nix/iris.nix
new file mode 100644
index 0000000000..b55cccc7c6
--- /dev/null
+++ b/dev/ci/nix/iris.nix
@@ -0,0 +1,4 @@
+{ stdpp }:
+{
+ coqBuildInputs = [ stdpp ];
+}
diff --git a/dev/ci/nix/lambda-rust.nix b/dev/ci/nix/lambda-rust.nix
new file mode 100644
index 0000000000..0d07c3028a
--- /dev/null
+++ b/dev/ci/nix/lambda-rust.nix
@@ -0,0 +1,4 @@
+{ iris }:
+{
+ coqBuildInputs = [ iris ];
+}
diff --git a/dev/ci/nix/unicoq/META b/dev/ci/nix/unicoq/META
deleted file mode 100644
index 30dd8b5559..0000000000
--- a/dev/ci/nix/unicoq/META
+++ /dev/null
@@ -1,2 +0,0 @@
-archive(native) = "unicoq.cmxa"
-plugin(native) = "unicoq.cmxs"
diff --git a/dev/ci/nix/unicoq/default.nix b/dev/ci/nix/unicoq/default.nix
index 36f40dbe33..54c67ac0fd 100644
--- a/dev/ci/nix/unicoq/default.nix
+++ b/dev/ci/nix/unicoq/default.nix
@@ -1,4 +1,10 @@
-{ stdenv, coq }:
+{ stdenv, writeText, coq }:
+
+let META = writeText "META" ''
+ archive(native) = "unicoq.cmxa"
+ plugin(native) = "unicoq.cmxs"
+''; in
+
stdenv.mkDerivation {
name = "coq${coq.coq-version}-unicoq-0.0-git";
@@ -12,8 +18,9 @@ stdenv.mkDerivation {
installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
postInstall = ''
+ cp ${META} META
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
+ install -m 0644 META src/unicoq.a $OCAMLFIND_DESTDIR/Unicoq
'';
}
diff --git a/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh b/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh
deleted file mode 100644
index 6e89741e29..0000000000
--- a/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "6914" ] || [ "$CI_BRANCH" = "primitive-bool-list" ]; then
-
- bignums_CI_REF=primitive-integers
- bignums_CI_GITURL=https://github.com/vbgl/bignums
-
- mtac2_CI_REF=primitive-integers
- mtac2_CI_GITURL=https://github.com/vbgl/Mtac2
-
-fi
diff --git a/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh b/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh
deleted file mode 100644
index 2df8affd14..0000000000
--- a/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9102" ] || [ "$CI_BRANCH" = "ltac+remove_aliases" ]; then
-
- elpi_CI_REF=ltac+remove_aliases
- elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
-
-fi
diff --git a/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh b/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh
deleted file mode 100644
index f2a113b118..0000000000
--- a/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9150" ] || [ "$CI_BRANCH" = "build+warn_50" ]; then
-
- mtac2_CI_REF=build+warn_50
- mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
-
-fi
diff --git a/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh b/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh
deleted file mode 100644
index f532fdfc52..0000000000
--- a/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9172" ] || [ "$CI_BRANCH" = "proof_rework" ]; then
-
- ltac2_CI_REF=proof_rework
- ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
-
- mtac2_CI_REF=proof_rework
- mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
-
-fi
diff --git a/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh b/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh
new file mode 100644
index 0000000000..23eb24c304
--- /dev/null
+++ b/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "9173" ] || [ "$CI_BRANCH" = "proofview+proof_info" ]; then
+
+ ltac2_CI_REF=proofview+proof_info
+ ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+ fiat_parsers_CI_REF=proofview+proof_info
+ fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat
+
+fi
diff --git a/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh b/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh
deleted file mode 100644
index efcdd2e97f..0000000000
--- a/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9220" ] || [ "$CI_BRANCH" = "stm-shallow-logic" ]; then
-
- paramcoq_CI_REF=stm-shallow-logic
- paramcoq_CI_GITURL=https://github.com/maximedenes/paramcoq
-
-fi
diff --git a/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh b/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh
deleted file mode 100644
index ebd1b524da..0000000000
--- a/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9263" ] || [ "$CI_BRANCH" = "parsing-state" ]; then
-
- mtac2_CI_REF=proof-mode
- mtac2_CI_GITURL=https://github.com/maximedenes/Mtac2
-
- ltac2_CI_REF=proof-mode
- ltac2_CI_GITURL=https://github.com/maximedenes/ltac2
-
- equations_CI_REF=proof-mode
- equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
-
-fi
diff --git a/dev/core_dune.dbg b/dev/core_dune.dbg
index cf9c5bd39a..4e1035f7b6 100644
--- a/dev/core_dune.dbg
+++ b/dev/core_dune.dbg
@@ -1,10 +1,10 @@
load_printer threads.cma
load_printer str.cma
-load_printer gramlib.cma
load_printer config.cma
load_printer clib.cma
load_printer dynlink.cma
load_printer lib.cma
+load_printer gramlib.cma
load_printer byterun.cma
load_printer kernel.cma
load_printer library.cma
diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
index d05b6c8eef..60c0886896 100644
--- a/dev/doc/release-process.md
+++ b/dev/doc/release-process.md
@@ -92,7 +92,11 @@
### These steps are the same for all releases (beta, final, patch-level) ###
- [ ] Send an e-mail on Coqdev announcing that the tag has been put so that
- package managers can start preparing package updates.
+ package managers can start preparing package updates (including a
+ `coq-bignums` compatible version).
+- [ ] Ping **@erikmd** to update the Docker images in `coqorg/coq`
+ (requires `coq-bignums` in `extra-dev` for a beta / in `released`
+ for a final release).
- [ ] Draft a release on GitHub.
- [ ] Get **@maximedenes** to sign the Windows and MacOS packages and
upload them on GitHub.
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index 5eac3e2b9c..4d874cdd12 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -161,6 +161,7 @@ val ppobj : Libobject.obj -> unit
val cast_kind_display : Constr.cast_kind -> string
val constr_display : Constr.constr -> unit
val print_pure_constr : Constr.types -> unit
+val print_pure_econstr : EConstr.types -> unit
val pploc : Loc.t -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 05:28:20 +0000