aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rwxr-xr-xdev/ci/ci-bedrock2.sh2
-rw-r--r--dev/ci/user-overlays/09410-maximedenes-thread-program.sh13
-rw-r--r--dev/doc/release-process.md6
-rw-r--r--dev/top_printers.mli1
4 files changed, 20 insertions, 2 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/user-overlays/09410-maximedenes-thread-program.sh b/dev/ci/user-overlays/09410-maximedenes-thread-program.sh
new file mode 100644
index 0000000000..985c2db74e
--- /dev/null
+++ b/dev/ci/user-overlays/09410-maximedenes-thread-program.sh
@@ -0,0 +1,13 @@
+if [ "$CI_PULL_REQUEST" = "9410" ] || [ "$CI_BRANCH" = "thread-program" ]; then
+
+ math_classes_CI_REF=program-mode-flag
+ math_classes_CI_GITURL=https://github.com/maximedenes/math-classes
+
+ ltac2_CI_REF=program-mode-flag
+ ltac2_CI_GITURL=https://github.com/maximedenes/ltac2
+
+
+ equations_CI_REF=thread-program
+ equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
+
+fi
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