branch: elpa/proof-general
commit 0d15f057b33e0aff12816784b275a5288d48d446
Author: Hendrik Tews <hend...@askra.de>
Commit: Hendrik Tews <hend...@askra.de>
CI: update to Rocq 9.1+rc1
- Add Rocq 9.1+rc1 and Ubuntu 25 to the release table. Mark
8.20.1/29.4 as historic pair.
- Include 9.1+rc1 in testing. Because there is no opam package
rocq-prover any more (see
https://github.com/rocq-prover/rocq/issues/20742), only rocq-core is
installed in these containers. Switch to Debian 13 Trixie with OCaml
5.3.0.
- Ubuntu 20.4 Focal Fossa reached end of live, therefore the actively
supported and tested Coq moved from 8.11.2 to 8.15.2 and Emacs moved
from 26.3 to 27.1.
- Coq 8.9.1 is more than 6 year old, so 8.10.2 with Emacs 26.3 is now
the oldest passively supported pair.
- Improve cipg.ml a little bit such that the commands for the ci-coq
and coq-emacs containers are correct.
- Add relevant Debian and Ubuntu releases in README.md.
- Fix tests that assumed Stdlib is present.
---
.github/workflows/test.yml | 66 +++++------
ci/compile-tests/002-require-no-dependencies/a.v | 2 +-
ci/compile-tests/002-require-no-dependencies/b.v | 2 +-
ci/doc/README.md | 99 +++++++++--------
ci/doc/coq-emacs-releases.org | 6 +-
ci/doc/currently-used-ci-coq-versions | 2 +-
ci/doc/currently-used-coq-emacs-versions | 29 ++---
ci/simple-tests/coq-test-goals-present.el | 114 ++++++++++++-------
.../coq-test-par-job-needs-compilation-quick.el | 6 +-
ci/tools/cipg.ml | 122 ++++++++++++++++-----
10 files changed, 272 insertions(+), 176 deletions(-)
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index baa2832d453..5255262938c 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -30,7 +30,6 @@ jobs:
# The content between the CIPG markers is automatically
# changed by the cipg program. Do not change these markers.
# CIPG change marker: build-emacs-versions
- - 26.3
- 27.1
- 27.2
- 28.1
@@ -109,14 +108,6 @@ jobs:
# The content between the CIPG markers is automatically
# changed by the cipg program. Do not change these markers.
# CIPG change marker: test-coq-emacs-versions
- - coq-8.11.2-emacs-26.3
- - coq-8.11.2-emacs-30.1
- - coq-8.12.2-emacs-27.1
- - coq-8.12.2-emacs-30.1
- - coq-8.13.2-emacs-27.2
- - coq-8.13.2-emacs-30.1
- - coq-8.14.1-emacs-27.2
- - coq-8.14.1-emacs-30.1
- coq-8.15.2-emacs-27.1
- coq-8.15.2-emacs-28.1
- coq-8.15.2-emacs-30.1
@@ -126,18 +117,16 @@ jobs:
- coq-8.17.1-emacs-30.1
- coq-8.18.0-emacs-29.3
- coq-8.18.0-emacs-30.1
- - coq-8.19.2-emacs-26.3
- coq-8.19.2-emacs-27.1
- coq-8.19.2-emacs-28.2
- coq-8.19.2-emacs-29.3
- coq-8.19.2-emacs-29.4
- coq-8.19.2-emacs-30.1
- - coq-8.20.1-emacs-26.3
- coq-8.20.1-emacs-27.1
- coq-8.20.1-emacs-28.2
- coq-8.20.1-emacs-29.3
+ - coq-8.20.1-emacs-29.4
- coq-8.20.1-emacs-30.1
- - coq-9.0.0-emacs-26.3
- coq-9.0.0-emacs-27.1
- coq-9.0.0-emacs-27.2
- coq-9.0.0-emacs-28.1
@@ -147,6 +136,15 @@ jobs:
- coq-9.0.0-emacs-29.3
- coq-9.0.0-emacs-29.4
- coq-9.0.0-emacs-30.1
+ - coq-9.1-rc1-emacs-27.1
+ - coq-9.1-rc1-emacs-27.2
+ - coq-9.1-rc1-emacs-28.1
+ - coq-9.1-rc1-emacs-28.2
+ - coq-9.1-rc1-emacs-29.1
+ - coq-9.1-rc1-emacs-29.2
+ - coq-9.1-rc1-emacs-29.3
+ - coq-9.1-rc1-emacs-29.4
+ - coq-9.1-rc1-emacs-30.1
# CIPG change marker end
# don't cancel all in-progress jobs if one matrix job fails:
fail-fast: false
@@ -188,14 +186,6 @@ jobs:
# The content between the CIPG markers is automatically
# changed by the cipg program. Do not change these markers.
# CIPG change marker: compile-coq-emacs-versions
- - coq-8.11.2-emacs-26.3
- - coq-8.11.2-emacs-30.1
- - coq-8.12.2-emacs-27.1
- - coq-8.12.2-emacs-30.1
- - coq-8.13.2-emacs-27.2
- - coq-8.13.2-emacs-30.1
- - coq-8.14.1-emacs-27.2
- - coq-8.14.1-emacs-30.1
- coq-8.15.2-emacs-27.1
- coq-8.15.2-emacs-28.1
- coq-8.15.2-emacs-30.1
@@ -205,18 +195,16 @@ jobs:
- coq-8.17.1-emacs-30.1
- coq-8.18.0-emacs-29.3
- coq-8.18.0-emacs-30.1
- - coq-8.19.2-emacs-26.3
- coq-8.19.2-emacs-27.1
- coq-8.19.2-emacs-28.2
- coq-8.19.2-emacs-29.3
- coq-8.19.2-emacs-29.4
- coq-8.19.2-emacs-30.1
- - coq-8.20.1-emacs-26.3
- coq-8.20.1-emacs-27.1
- coq-8.20.1-emacs-28.2
- coq-8.20.1-emacs-29.3
+ - coq-8.20.1-emacs-29.4
- coq-8.20.1-emacs-30.1
- - coq-9.0.0-emacs-26.3
- coq-9.0.0-emacs-27.1
- coq-9.0.0-emacs-27.2
- coq-9.0.0-emacs-28.1
@@ -226,6 +214,15 @@ jobs:
- coq-9.0.0-emacs-29.3
- coq-9.0.0-emacs-29.4
- coq-9.0.0-emacs-30.1
+ - coq-9.1-rc1-emacs-27.1
+ - coq-9.1-rc1-emacs-27.2
+ - coq-9.1-rc1-emacs-28.1
+ - coq-9.1-rc1-emacs-28.2
+ - coq-9.1-rc1-emacs-29.1
+ - coq-9.1-rc1-emacs-29.2
+ - coq-9.1-rc1-emacs-29.3
+ - coq-9.1-rc1-emacs-29.4
+ - coq-9.1-rc1-emacs-30.1
# CIPG change marker end
# don't cancel all in-progress jobs if one matrix job fails:
fail-fast: false
@@ -263,14 +260,6 @@ jobs:
# The content between the CIPG markers is automatically
# changed by the cipg program. Do not change these markers.
# CIPG change marker: simple-coq-emacs-versions
- - coq-8.11.2-emacs-26.3
- - coq-8.11.2-emacs-30.1
- - coq-8.12.2-emacs-27.1
- - coq-8.12.2-emacs-30.1
- - coq-8.13.2-emacs-27.2
- - coq-8.13.2-emacs-30.1
- - coq-8.14.1-emacs-27.2
- - coq-8.14.1-emacs-30.1
- coq-8.15.2-emacs-27.1
- coq-8.15.2-emacs-28.1
- coq-8.15.2-emacs-30.1
@@ -280,18 +269,16 @@ jobs:
- coq-8.17.1-emacs-30.1
- coq-8.18.0-emacs-29.3
- coq-8.18.0-emacs-30.1
- - coq-8.19.2-emacs-26.3
- coq-8.19.2-emacs-27.1
- coq-8.19.2-emacs-28.2
- coq-8.19.2-emacs-29.3
- coq-8.19.2-emacs-29.4
- coq-8.19.2-emacs-30.1
- - coq-8.20.1-emacs-26.3
- coq-8.20.1-emacs-27.1
- coq-8.20.1-emacs-28.2
- coq-8.20.1-emacs-29.3
+ - coq-8.20.1-emacs-29.4
- coq-8.20.1-emacs-30.1
- - coq-9.0.0-emacs-26.3
- coq-9.0.0-emacs-27.1
- coq-9.0.0-emacs-27.2
- coq-9.0.0-emacs-28.1
@@ -301,6 +288,15 @@ jobs:
- coq-9.0.0-emacs-29.3
- coq-9.0.0-emacs-29.4
- coq-9.0.0-emacs-30.1
+ - coq-9.1-rc1-emacs-27.1
+ - coq-9.1-rc1-emacs-27.2
+ - coq-9.1-rc1-emacs-28.1
+ - coq-9.1-rc1-emacs-28.2
+ - coq-9.1-rc1-emacs-29.1
+ - coq-9.1-rc1-emacs-29.2
+ - coq-9.1-rc1-emacs-29.3
+ - coq-9.1-rc1-emacs-29.4
+ - coq-9.1-rc1-emacs-30.1
# CIPG change marker end
# don't cancel all in-progress jobs if one matrix job fails:
fail-fast: false
@@ -342,7 +338,6 @@ jobs:
# The content between the CIPG markers is automatically
# changed by the cipg program. Do not change these markers.
# CIPG change marker: indent-emacs-versions
- - 26.3
- 27.1
- 27.2
- 28.1
@@ -380,7 +375,6 @@ jobs:
# The content between the CIPG markers is automatically
# changed by the cipg program. Do not change these markers.
# CIPG change marker: qrhl-emacs-versions
- - 26.3
- 27.1
- 27.2
- 28.1
diff --git a/ci/compile-tests/002-require-no-dependencies/a.v
b/ci/compile-tests/002-require-no-dependencies/a.v
index cbe7525f552..12053fcec6c 100644
--- a/ci/compile-tests/002-require-no-dependencies/a.v
+++ b/ci/compile-tests/002-require-no-dependencies/a.v
@@ -19,6 +19,6 @@
(* This is line 21 *)
-Require Coq.Bool.Bool.
+Require Init.Datatypes.
Definition a : nat := 0.
(* This is line 24 *)
diff --git a/ci/compile-tests/002-require-no-dependencies/b.v
b/ci/compile-tests/002-require-no-dependencies/b.v
index 411a8c6114e..c98601134ff 100644
--- a/ci/compile-tests/002-require-no-dependencies/b.v
+++ b/ci/compile-tests/002-require-no-dependencies/b.v
@@ -19,6 +19,6 @@
(* This is line 21 *)
-Require Coq.Bool.Bool.
+Require Init.Datatypes.
Require c.
(* This is line 24 *)
diff --git a/ci/doc/README.md b/ci/doc/README.md
index 227e2db99c2..383ed5f6695 100644
--- a/ci/doc/README.md
+++ b/ci/doc/README.md
@@ -68,13 +68,12 @@ releases (e.g., 8.19.1 and 8.19.2). For testing Proof
General we only
use the latest bug fix release of certain Coq releases (e.g., we do
test 8.19.2 but neither 8.19.0 nor 8.19.1). One reason is that testing
original minor releases (e.g., 8.19.0) or outdated bug fix releases
-(e.g., 8.19.1) does not make much sense. Another reason is that
-`coqorg/coq` does only provide containers for the latest bug fix
-release of each minor release. Admittedly, the effects of only testing
-the latest bug fix release are not always optimal. For instance, in
-2024, Coq 8.11 is tested, because Ubuntu 20.04 Focal Fossa was
-released with Coq 8.11.0, however, Proof General testing uses Coq
-8.11.2.
+(e.g., 8.19.1) does not make much sense. Another reason is the number
+of needed containers and the space they occupy. Admittedly, the
+effects of only testing the latest bug fix release are not always
+optimal. For instance, in 2024, Coq 8.11 is tested, because Ubuntu
+20.04 Focal Fossa was released with Coq 8.11.0, however, Proof General
+testing uses Coq 8.11.2.
# Generic strategy {#generic}
@@ -95,14 +94,28 @@ standard support. For Debian these are the releases whose
end of live
date is in the future. For Ubuntu these are the releases whose end of
standard support date is in the future.
-Currently, the first actively supported versions are
+Currently, the relevant Debian and Ubuntu releases that still enjoy
+standard support are
+
+<!-- The content between the CIPG markers is automatically changed by
+ !-- the cipg program. Do not change these markers. -->
+<!-- CIPG change marker: lts-versions -->
+| release | Coq | Emacs | EOL |
+|------------------|---------|-------|---------|
+| ubu 25 plucky | 8.20.1 | 30.1 | 2026/01 |
+| deb 12 bookworm | 8.16.1 | 28.2 | 2026/06 |
+| ubu 22 jammy jel | 8.15.0 | 27.1 | 2027/04 |
+| ubu 24 noble num | 8.18.0 | 29.3 | 2029/06 |
+<!-- CIPG change marker end -->
+
+The oldest actively supported versions therefore are
<!-- The content between the CIPG markers is automatically changed by
!-- the cipg program. Do not change these markers. -->
<!-- CIPG change marker: coq-emacs-versions -->
-| Coq | 8.11.2 |
+| Coq | 8.15.2 |
|-------+-------|
-| Emacs | 26.3 |
+| Emacs | 27.1 |
<!-- CIPG change marker end -->
The set of passively supported Coq/Emacs version pairs is work in
@@ -169,28 +182,28 @@ This results in
<!-- The content between the CIPG markers is automatically changed by
!-- the cipg program. Do not change these markers. -->
<!-- CIPG change marker: container-number -->
-71
+60
<!-- CIPG change marker end -->
containers.
<!-- The content between the CIPG markers is automatically changed by
!-- the cipg program. Do not change these markers. -->
<!-- CIPG change marker: container-table -->
-| | 26.2 | 26.3 | 27.1 | 27.2 | 28.1 | 28.2 | 29.1 | 29.2 | 29.3 |
29.4 | 30.1 |
-|---------+------+------+------+------+------+------+------+------+------+------+------|
-| 8.9.1 | H | | | | | | | | |
| |
-| 8.10.2 | | H | | | | | | | |
| |
-| 8.11.2 | | SUP | | | | | | | |
| N |
-| 8.12.2 | | SUP | H | | | | | | |
| N |
-| 8.13.2 | | SUP | | H | | | | | |
| N |
-| 8.14.1 | | SUP | | H | | | | | |
| N |
-| 8.15.2 | | SUP | SUP | | H | | | | |
| N |
-| 8.16.1 | | SUP | SUP | | | SUP | | | |
| N |
-| 8.17.1 | | X | X | X | X | X | X | X | X | X
| X |
-| 8.18.0 | | X | X | X | X | X | X | X | X | X
| X |
-| 8.19.2 | | X | X | X | X | X | X | X | X | X
| X |
-| 8.20.1 | | X | X | X | X | X | X | X | X | X
| X |
-| 9.0.0 | | X | X | X | X | X | X | X | X | X
| X |
+| | 26.3 | 27.1 | 27.2 | 28.1 | 28.2 | 29.1 | 29.2 | 29.3 | 29.4 |
30.1 |
+|---------+------+------+------+------+------+------+------+------+------+------|
+| 8.10.2 | H | | | | | | | | |
|
+| 8.11.2 | H | | | | | | | | |
|
+| 8.12.2 | | H | | | | | | | |
|
+| 8.13.2 | | | H | | | | | | |
|
+| 8.14.1 | | | H | | | | | | |
|
+| 8.15.2 | | SUP | | H | | | | | | N
|
+| 8.16.1 | | SUP | | | SUP | | | | | N
|
+| 8.17.1 | | SUP | | | SUP | H | | | | N
|
+| 8.18.0 | | X | X | X | X | X | X | X | X | X
|
+| 8.19.2 | | X | X | X | X | X | X | X | X | X
|
+| 8.20.1 | | X | X | X | X | X | X | X | X | X
|
+| 9.0.0 | | X | X | X | X | X | X | X | X | X
|
+| 9.1+rc1 | | RC | RC | RC | RC | RC | RC | RC | RC |
RC |
<!-- CIPG change marker end -->
In the table above,
@@ -288,28 +301,28 @@ This results in
<!-- The content between the CIPG markers is automatically changed by
!-- the cipg program. Do not change these markers. -->
<!-- CIPG change marker: testrun-number -->
-38
+37
<!-- CIPG change marker end -->
version pairs for the Proof General interaction tests with Coq.
<!-- The content between the CIPG markers is automatically changed by
!-- the cipg program. Do not change these markers. -->
<!-- CIPG change marker: testrun-table -->
-| | 26.2 | 26.3 | 27.1 | 27.2 | 28.1 | 28.2 | 29.1 | 29.2 | 29.3 |
29.4 | 30.1 |
-|---------+------+------+------+------+------+------+------+------+------+------+------|
-| 8.9.1 | | | | | | | | | |
| |
-| 8.10.2 | | | | | | | | | |
| |
-| 8.11.2 | | SUP | | | | | | | |
| N |
-| 8.12.2 | | | H | | | | | | |
| N |
-| 8.13.2 | | | | H | | | | | |
| N |
-| 8.14.1 | | | | H | | | | | |
| N |
-| 8.15.2 | | | SUP | | H | | | | |
| N |
-| 8.16.1 | | | | | | SUP | | | |
| N |
-| 8.17.1 | | | | | | | H | | |
| N |
-| 8.18.0 | | | | | | | | | SUP |
| N |
-| 8.19.2 | | X | X | | | X | | | X | H
| N |
-| 8.20.1 | | X | X | | | X | | | X |
| N |
-| 9.0.0 | | X | X | N | N | X | N | N | X | N
| N |
+| | 26.3 | 27.1 | 27.2 | 28.1 | 28.2 | 29.1 | 29.2 | 29.3 | 29.4 |
30.1 |
+|---------+------+------+------+------+------+------+------+------+------+------|
+| 8.10.2 | | | | | | | | | |
|
+| 8.11.2 | | | | | | | | | |
|
+| 8.12.2 | | | | | | | | | |
|
+| 8.13.2 | | | | | | | | | |
|
+| 8.14.1 | | | | | | | | | |
|
+| 8.15.2 | | SUP | | H | | | | | | N
|
+| 8.16.1 | | | | | SUP | | | | | N
|
+| 8.17.1 | | | | | | H | | | | N
|
+| 8.18.0 | | | | | | | | SUP | | N
|
+| 8.19.2 | | X | | | X | | | X | H | N
|
+| 8.20.1 | | X | | | X | | | X | H |
SUP |
+| 9.0.0 | | X | N | N | X | N | N | X | N | X
|
+| 9.1+rc1 | | RC | RC | RC | RC | RC | RC | RC | RC |
RC |
<!-- CIPG change marker end -->
See [Container build strategy](#contbuild) for an explanation of the
@@ -319,7 +332,7 @@ In summary, all Proof General testing jobs run
<!-- The content between the CIPG markers is automatically changed by
!-- the cipg program. Do not change these markers. -->
<!-- CIPG change marker: total-checks-number -->
-146
+140
<!-- CIPG change marker end -->
github checks.
diff --git a/ci/doc/coq-emacs-releases.org b/ci/doc/coq-emacs-releases.org
index 31cfec5e3f2..e1cfbfa7e25 100644
--- a/ci/doc/coq-emacs-releases.org
+++ b/ci/doc/coq-emacs-releases.org
@@ -13,10 +13,12 @@
| date | coq | emacs | distribution name | EOL | historic |
|---------+---------+-------+-------------------+----------+----------|
+| 2025/07 | 9.1-rc1 | | | | |
| 2025/03 | 9.0.0 | | | | |
| 2025/02 | | 30.1 | | | |
| 2025/01 | 9.0-rc1 | | | | |
-| 2025/01 | 8.20.1 | | | | |
+| 2025/04 | | 30.1 | ubu 25 plucky | 2026/01 | |
+| 2025/01 | 8.20.1 | | | | X |
| 2024/09 | 8.20.0 | | | | |
| 2024/06 | 8.19.2 | 29.4 | | | X |
| 2024/03 | 8.19.1 | 29.3 | | | |
@@ -27,7 +29,7 @@
| 2023/06 | 8.17.1 | | | | |
| 2023/10 | | 29.1 | ubu 23 mantic mi | 2024/07 | |
| 2023/03 | 8.17.0 | | | | |
-| 2023/06 | | | deb 12 bookworm | 2026/06? | |
+| 2023/06 | | | deb 12 bookworm | 2026/06 | |
| 2023/04 | | | ubu 23 lun lobs | 2024/01 | |
| 2022/11 | 8.16.1 | | | | X |
| 2022/09 | 8.16.0 | 28.2 | | | |
diff --git a/ci/doc/currently-used-ci-coq-versions
b/ci/doc/currently-used-ci-coq-versions
index 372c01a00dc..18f8417c7ea 100644
--- a/ci/doc/currently-used-ci-coq-versions
+++ b/ci/doc/currently-used-ci-coq-versions
@@ -1,4 +1,3 @@
-coq-8.9.1
coq-8.10.2
coq-8.11.2
coq-8.12.2
@@ -11,3 +10,4 @@ coq-8.18.0
coq-8.19.2
coq-8.20.1
coq-9.0.0
+coq-9.1-rc1
diff --git a/ci/doc/currently-used-coq-emacs-versions
b/ci/doc/currently-used-coq-emacs-versions
index 47545105feb..7c4858e4ad6 100644
--- a/ci/doc/currently-used-coq-emacs-versions
+++ b/ci/doc/currently-used-coq-emacs-versions
@@ -1,35 +1,18 @@
-coq-8.9.1-emacs-26.2
coq-8.10.2-emacs-26.3
coq-8.11.2-emacs-26.3
-coq-8.11.2-emacs-30.1
-coq-8.12.2-emacs-26.3
coq-8.12.2-emacs-27.1
-coq-8.12.2-emacs-30.1
-coq-8.13.2-emacs-26.3
coq-8.13.2-emacs-27.2
-coq-8.13.2-emacs-30.1
-coq-8.14.1-emacs-26.3
coq-8.14.1-emacs-27.2
-coq-8.14.1-emacs-30.1
-coq-8.15.2-emacs-26.3
coq-8.15.2-emacs-27.1
coq-8.15.2-emacs-28.1
coq-8.15.2-emacs-30.1
-coq-8.16.1-emacs-26.3
coq-8.16.1-emacs-27.1
coq-8.16.1-emacs-28.2
coq-8.16.1-emacs-30.1
-coq-8.17.1-emacs-26.3
coq-8.17.1-emacs-27.1
-coq-8.17.1-emacs-27.2
-coq-8.17.1-emacs-28.1
coq-8.17.1-emacs-28.2
coq-8.17.1-emacs-29.1
-coq-8.17.1-emacs-29.2
-coq-8.17.1-emacs-29.3
-coq-8.17.1-emacs-29.4
coq-8.17.1-emacs-30.1
-coq-8.18.0-emacs-26.3
coq-8.18.0-emacs-27.1
coq-8.18.0-emacs-27.2
coq-8.18.0-emacs-28.1
@@ -39,7 +22,6 @@ coq-8.18.0-emacs-29.2
coq-8.18.0-emacs-29.3
coq-8.18.0-emacs-29.4
coq-8.18.0-emacs-30.1
-coq-8.19.2-emacs-26.3
coq-8.19.2-emacs-27.1
coq-8.19.2-emacs-27.2
coq-8.19.2-emacs-28.1
@@ -49,7 +31,6 @@ coq-8.19.2-emacs-29.2
coq-8.19.2-emacs-29.3
coq-8.19.2-emacs-29.4
coq-8.19.2-emacs-30.1
-coq-8.20.1-emacs-26.3
coq-8.20.1-emacs-27.1
coq-8.20.1-emacs-27.2
coq-8.20.1-emacs-28.1
@@ -59,7 +40,6 @@ coq-8.20.1-emacs-29.2
coq-8.20.1-emacs-29.3
coq-8.20.1-emacs-29.4
coq-8.20.1-emacs-30.1
-coq-9.0.0-emacs-26.3
coq-9.0.0-emacs-27.1
coq-9.0.0-emacs-27.2
coq-9.0.0-emacs-28.1
@@ -69,3 +49,12 @@ coq-9.0.0-emacs-29.2
coq-9.0.0-emacs-29.3
coq-9.0.0-emacs-29.4
coq-9.0.0-emacs-30.1
+coq-9.1-rc1-emacs-27.1
+coq-9.1-rc1-emacs-27.2
+coq-9.1-rc1-emacs-28.1
+coq-9.1-rc1-emacs-28.2
+coq-9.1-rc1-emacs-29.1
+coq-9.1-rc1-emacs-29.2
+coq-9.1-rc1-emacs-29.3
+coq-9.1-rc1-emacs-29.4
+coq-9.1-rc1-emacs-30.1
diff --git a/ci/simple-tests/coq-test-goals-present.el
b/ci/simple-tests/coq-test-goals-present.el
index 4e08ecbcc08..7faa37b02c5 100644
--- a/ci/simple-tests/coq-test-goals-present.el
+++ b/ci/simple-tests/coq-test-goals-present.el
@@ -27,15 +27,16 @@
(proof-ready-for-assistant 'coq)
(require 'coq-system)
-(defconst coq--post-v87 (not (coq--version< (coq-version t) "8.8"))
- "t if Coq is more recent than 8.7")
-
(defconst coq--between-v814-v815 (and (coq--post-v814) (coq--pre-v816))
"t if Coq is either 8.14 or 8.15")
+(defconst coq--post-8-20 (not (coq--version< (coq-version t) "9.0alpha"))
+ "t if Coq is 9.0 or higher")
+
+
(message (concat "goal/response present tests run with Coq version %s; \n\t"
- "post-v87: %s; between 8.14-8.15 %s")
- (coq-version t) coq--post-v87 coq--between-v814-v815)
+ "between 8.14-8.15 %s; post-8.20 %s")
+ (coq-version t) coq--between-v814-v815 coq--post-8-20)
;;; Coq source code for tests
@@ -152,12 +153,12 @@ Proof using.
"Coq source code for checking that goals are up-to-date after Check.")
(defconst coq-src-report-response-check
- "Require Import Arith.
+ "Definition x := 1.
-Lemma a : forall(a b : nat), a + b = b + a.
+Lemma y : forall(a b : nat), S (a + b) = a + S b.
Proof using.
intros a b.
- apply Nat.add_comm.
+ apply plus_n_Sm.
Qed.
"
"Coq source code for response buffer visibility tests.
@@ -176,34 +177,45 @@ Used in `check-response-present' for all
`response-buffer-visible-*' tests.")
"
"Coq source for ert-deftest's error-message-visible-at-qed-*")
-(defconst coq-src-queuemode-for-show
- "Require Export Coq.Lists.List.
-Export ListNotations.
+(defconst coq-src-queuemode-for-show-require
+ (if coq--post-8-20
+ "Require Export Lists.ListDef.\n"
+ "Require Export Coq.Lists.List.\n")
+ "Require command to use lists.
+Starting in 9.0 the standard library containing Coq.Lists.List is in a
+separate opam package, which might not be installed in the testing
+container. There use only stuff from the prelude, which is contained in
+packate rocq-core.")
+
+(defconst coq-src-queuemode-for-show-remainder
+ "Open Scope list_scope.
Inductive tree : Type :=
Subtrees : list tree -> tree.
Fixpoint list_create(n : nat)(t : tree) : list tree :=
match n with
- | 0 => []
+ | 0 => nil
| S n => t :: (list_create n t)
end.
Fixpoint build_tree(n m : nat) : tree :=
match n with
- | 0 => Subtrees []
+ | 0 => Subtrees nil
| S n => Subtrees (list_create m (build_tree n m))
end.
Lemma a :
- build_tree 6 6 = Subtrees [].
+ build_tree 6 6 = Subtrees nil.
Proof using. (* marker A *)
cbv.
trivial.
"
- "Coq source code for extend/retract tests during long running Show.
-When unfolded, the function build_tree generates big terms that take
-quite long to print.")
+ "Main Coq source code for extend/retract tests during long running Show.
+Main parte of Coq source code for extend/retract tests during long
+running Show without the first Require command, which is in
+`coq-src-queuemode-for-show-require'. When unfolded, the function
+build_tree generates big terms that take quite long to print.")
;;; utility functions
@@ -627,7 +639,7 @@ and calls QUERY-FUN. It then checks, according to RESPONSE,
that the
response buffer is either empty or contains the expected result. The
function further checks that the response buffer is visible in some
window."
- (let (buffer)
+ (let (buffer pos)
(unwind-protect
(progn
(find-file "goals.v")
@@ -635,8 +647,18 @@ window."
(insert coq-src-report-response-check)
(goto-char (point-min))
(forward-line (1- line))
+ (setq pos (point))
(proof-goto-point)
(wait-for-coq)
+ (message
+ "locked span: %s, locked until %s, point should be at %s, now at %s"
+ proof-locked-span
+ (and proof-locked-span (span-end proof-locked-span))
+ pos (point))
+ (should (eq pos (point)))
+ (should (and proof-locked-span
+ (span-end proof-locked-span)
+ (eq (1+ (span-end proof-locked-span)) (point))))
;; (record-buffer-content "*coq*")
;; (record-buffer-content "*goals*")
@@ -672,23 +694,23 @@ window."
(kill-buffer buffer)))))
(ert-deftest response-buffer-visible-coq-search-something-inside-proof ()
- "Check response for coq-Search on (0 <= 2) inside proof."
- (message "Check response for Search (0 <= 2) is shown inside proof")
- (check-response-present #'coq-Search 6 "(0 <= 2)" "Nat.le_0_2"))
+ "Check response for coq-Search on (S (_ + _)) inside proof."
+ (message "Check response for Search (S (_ + _)) is shown inside proof")
+ (check-response-present #'coq-Search 6 "(S (_ + _))" "^plus_Sn_m: forall"))
(ert-deftest response-buffer-visible-coq-search-something-proof-end ()
- "Check response for coq-Search on (0 <= 2) at proof end.
+ "Check response for coq-Search on (S (_ + _)) at proof end.
Skipped for 8.14 and 8.15, there Coq reacts with an error when searching
in proof mode with no more goals."
- (message "Check response for Search (0 <= 2) is shown at proof end")
+ (message "Check response for Search (S (_ + _)) is shown at proof end")
;; XXX change to skip-when when Emacs 29 is phased out
(skip-unless (not coq--between-v814-v815))
- (check-response-present #'coq-Search 7 "(0 <= 2)" "Nat.le_0_2"))
+ (check-response-present #'coq-Search 7 "(S (_ + _))" "^plus_Sn_m: forall"))
(ert-deftest response-buffer-visible-coq-search-something-outside-proof ()
- "Check response for coq-Search on (0 <= 2) outside any proof."
- (message "Check response for Search (0 <= 2) is shown outside proofs")
- (check-response-present #'coq-Search 3 "(0 <= 2)" "Nat.le_0_2"))
+ "Check response for coq-Search on (S (_ + _)) outside any proof."
+ (message "Check response for Search (S (_ + _)) is shown outside proofs")
+ (check-response-present #'coq-Search 2 "(S (_ + _))" "^plus_Sn_m: forall"))
(ert-deftest response-buffer-visible-coq-search-empty-inside-proof ()
"Check empty response for coq-Search on 42 inside proof"
@@ -707,28 +729,28 @@ in proof mode with no more goals."
(ert-deftest response-buffer-visible-coq-search-empty-outside-proof ()
"Check empty response for coq-Search on 42 outside proof"
(message "Check empty response for Search 42 is shown outside proof")
- (check-response-present #'coq-Search 3 "42" t))
+ (check-response-present #'coq-Search 2 "42" t))
(ert-deftest response-buffer-visible-coq-check-print-all-inside-poof ()
- "Check response for coq-Check on Nat.add_comm inside proof with printing
all."
+ "Check response for coq-Check on plus_n_Sm inside proof with printing all."
(message
- "Check response for Check Nat.add_comm inside proof with printing all")
+ "Check response for Check plus_n_Sm proof with printing all")
(check-response-present
- #'(lambda() (coq-Check t)) 6 "Nat.add_comm" "@eq nat (Nat.add n m)"))
+ #'(lambda() (coq-Check t)) 6 "plus_n_Sm" "@eq nat (S (Nat.add"))
(ert-deftest response-buffer-visible-coq-check-print-all-poof-end ()
- "Check response for coq-Check on Nat.add_comm at proof end with printing
all."
+ "Check response for coq-Check on plus_n_Sm at proof end with printing all."
(message
- "Check response for Check Nat.add_comm at proof end with printing all")
+ "Check response for Check plus_n_Sm at proof end with printing all")
(check-response-present
- #'(lambda() (coq-Check t)) 7 "Nat.add_comm" "@eq nat (Nat.add n m)"))
+ #'(lambda() (coq-Check t)) 7 "plus_n_Sm" "@eq nat (S (Nat.add"))
(ert-deftest response-buffer-visible-coq-check-print-all-outside-poof ()
- "Check response for coq-Check on Nat.add_comm outside proof with printing
all."
+ "Check response for coq-Check on plus_n_Sm outside proof with printing all."
(message
- "Check response for Check Nat.add_comm outside proof with printing all")
+ "Check response for Check plus_n_Sm outside proof with printing all")
(check-response-present
- #'(lambda() (coq-Check t)) 3 "Nat.add_comm" "@eq nat (Nat.add n m)"))
+ #'(lambda() (coq-Check t)) 2 "plus_n_Sm" "@eq nat (S (Nat.add"))
(defun user-action-during-long-running-show (extend)
@@ -752,24 +774,36 @@ Need to clear `debug-on-error', which is set in ERT in
Emacs 29 and
earlier. `debug-on-error' changes `cl-assert' such that it's error is
not handled by `unwind-protect'. Then the next test triggers the wrong
queuemode assertion again, because Coq was not killed in the handler."
- (let (buffer)
+ (let (buffer pos)
(unwind-protect
(progn
(find-file "goals.v")
(setq buffer (current-buffer))
- (insert coq-src-queuemode-for-show)
+ (insert coq-src-queuemode-for-show-require)
+ (insert coq-src-queuemode-for-show-remainder)
(goto-char (point-min))
+ ;; (record-buffer-content (current-buffer))
(should (re-search-forward "marker A" nil t))
(forward-line 1)
+ (setq pos (point))
(proof-goto-point)
(wait-for-coq)
+ (message
+ "locked span: %s, locked until %s, point should be at %s, now at %s"
+ proof-locked-span
+ (and proof-locked-span (span-end proof-locked-span))
+ pos (point))
+ (should (eq pos (point)))
+ (should (and proof-locked-span
+ (span-end proof-locked-span)
+ (eq (1+ (span-end proof-locked-span)) (point))))
(message "Start command with long running Show")
(forward-line 1)
(proof-goto-point)
(accept-process-output nil 0.1)
- ;;(record-buffer-content "*coq*")
+ ;; (record-buffer-content "*coq*")
(if (consp proof-action-list)
(progn
diff --git a/ci/simple-tests/coq-test-par-job-needs-compilation-quick.el
b/ci/simple-tests/coq-test-par-job-needs-compilation-quick.el
index 23018091ee1..cea7f0943ff 100644
--- a/ci/simple-tests/coq-test-par-job-needs-compilation-quick.el
+++ b/ci/simple-tests/coq-test-par-job-needs-compilation-quick.el
@@ -798,7 +798,7 @@ relative ages.")
This function creates the files in DIR, sets up a job with the
necessary fields, calls `coq--par-job-needs-compilation-tests' and
-test the result and side effects wth `assert'."
+test the result and side effects with `assert'."
(let ((id (format "%s: %s %s%s" counter (car variant) file-descr
(if dep-just-compiled " just" "")))
(job (make-symbol "coq-compile-job-symbol"))
@@ -842,12 +842,12 @@ test the result and side effects wth `assert'."
(mapcar (lambda (sym) (test-coq-par-sym-to-file dir sym))
same-descr))
;; (message "try %s files %s" same-descr file-list)
- (setq same-counter 5)
+ (setq same-counter 8)
(setq same-not-ok t)
(while same-not-ok
(setq same-counter (1- same-counter))
(cl-assert (> same-counter 0)
- nil "create files with same time stamp filed")
+ nil "create files with same time stamp failed")
(dolist (file file-list)
(with-temp-file file t))
;; check now that all the files in file-list have the same time stamp
diff --git a/ci/tools/cipg.ml b/ci/tools/cipg.ml
index b65a57c149a..b5eb211cffd 100644
--- a/ci/tools/cipg.ml
+++ b/ci/tools/cipg.ml
@@ -22,8 +22,10 @@ let readme_file = "ci/doc/README.md"
(* github yaml workflow file *)
let test_workflow_file = ".github/workflows/test.yml"
-(* directory in which the pg-ci-coq and pg-ci-emacs directories are *)
-let src_dir = ref "~/src/docker"
+(* directory in which the base, coq, and emacs directories containing
+ the Dockerfiles are
+ *)
+let src_dir = ref "~/src/docker/pg-ci"
(* file containing the currently needed ci-coq containers *)
let currently_used_coq_file = "ci/doc/currently-used-ci-coq-versions"
@@ -851,6 +853,9 @@ let yml_file_change_wrapper file marker print_fn =
*
*****************************************************************************)
+(* Convert [v] of type version to string. This uses "+" in RC
+ versions, which is an invalid character for docker tags.
+ *)
let version_to_string v =
Printf.sprintf "%d.%d%s%s"
v.major v.minor
@@ -859,24 +864,30 @@ let version_to_string v =
| Some p -> Printf.sprintf ".%d" p)
(match v.release_candidate with
| None -> ""
- | Some rc -> Printf.sprintf "-rc%d" rc)
+ | Some rc -> Printf.sprintf "+rc%d" rc)
(* convert version to string, ignoring the index *)
let indexed_version_to_string (v, _i) = version_to_string v
+(* Convert [v] of type version to string. This uses "-" in RC
+ versions, which makes the version wrong but can be used in docker
+ tags.
+ *)
+let version_to_tag_string v =
+ Printf.sprintf "%d.%d%s%s"
+ v.major v.minor
+ (match v.patch with
+ | None -> ""
+ | Some p -> Printf.sprintf ".%d" p)
+ (match v.release_candidate with
+ | None -> ""
+ | Some rc -> Printf.sprintf "-rc%d" rc)
+
(* print a float as time YYYY/mm *)
let date_to_string d =
let tm = Unix.localtime d in
Printf.sprintf "%d/%02d" (tm.U.tm_year + 1900) (tm.U.tm_mon + 1)
-(* convert LTS record to string *)
-let lts_to_string {lts_coq; lts_emacs; lts_name; eol_date} =
- Printf.sprintf "%s with Coq %s emacs %s end of live on %s"
- lts_name
- (version_to_string lts_coq)
- (version_to_string lts_emacs)
- (date_to_string eol_date)
-
(* String of type matrix_element for matrix printing. *)
let string_of_matrix_element = function
| Unused -> ""
@@ -899,15 +910,40 @@ let report_historic_pairs kind pairs =
(version_to_string em_v) (version_to_string coq_v))
pairs))
+(* Print LTS table of relevant Debian and Ubuntu releases to
+ outchannel oc. Uses for regular output as well as for README.md.
+ *)
+let print_debian_ubuntu_release_table lts_list oc =
+ (* get the longest LTS name for table formatting *)
+ let lts_name_cols =
+ List.fold_left
+ (fun max {lts_name; } ->
+ let len = String.length lts_name in
+ if len > max then len else max)
+ 0 lts_list
+ in
+ Printf.fprintf oc "| %-*s | Coq | Emacs | EOL |\n"
+ lts_name_cols "release";
+ Printf.fprintf oc "|-%s-|---------|-------|---------|\n"
+ (String.make lts_name_cols '-');
+ List.iter
+ (fun {lts_coq; lts_emacs; lts_name; eol_date} ->
+ Printf.fprintf oc "| %-*s | %7s | %4s | %s |\n"
+ lts_name_cols lts_name
+ (version_to_string lts_coq)
+ (version_to_string lts_emacs)
+ (date_to_string eol_date))
+ lts_list
+
(* Report all interesting and relevant information read from the
* Coq/Emacs/Debian/Ubuntu relase table.
*)
let report_table_results first_emacs first_coq first_full_range_coq
first_partial_range_coq lts passive_hist active_hist coqs emacses
latest_two_emacs_major =
- Printf.printf "LTS versions:\n %s\n"
- (String.concat "\n " (List.map lts_to_string lts));
- Printf.printf "Coq versions: %s\n"
+ Printf.printf "\nLTS versions which are still alive:\n";
+ print_debian_ubuntu_release_table lts stdout;
+ Printf.printf "\nCoq versions: %s\n"
(String.concat ", " (List.map indexed_version_to_string coqs));
Printf.printf "Emacs versions: %s\n"
(String.concat ", " (List.map indexed_version_to_string emacses));
@@ -1124,13 +1160,13 @@ let get_coq_emacs_containers () =
*
*****************************************************************************)
-(* Return the coq-emacs docker tag for version coq and emacs. *)
-let coq_tag coq = Printf.sprintf "coq-%s" (version_to_string coq)
+(* Return the coq-emacs docker tag for a coq version. *)
+let coq_tag coq = Printf.sprintf "coq-%s" (version_to_tag_string coq)
(* Return the coq-emacs docker tag for version coq and emacs. *)
let coq_emacs_tag coq emacs =
Printf.sprintf "coq-%s-emacs-%s"
- (version_to_string coq) (version_to_string emacs)
+ (version_to_tag_string coq) (version_to_tag_string emacs)
(* Read currently needed coq-nix containers from doc subdir. *)
let read_currently_used_coq_containers () =
@@ -1193,6 +1229,7 @@ let check_coq_containers coqs =
let not_needed = list_diff coq_containers coqs in
let del_now = list_diff not_needed now_in_use in
let del_soon = list_intersection not_needed now_in_use in
+ let pushdir_printed = ref `NO in
Printf.printf "now superfluous coq versions: %s\n"
(String.concat " " (List.map version_to_string del_now));
Printf.printf "soon superfluous coq versions: %s\n\n"
@@ -1204,23 +1241,46 @@ let check_coq_containers coqs =
Printf.printf "# build missing ci-coq containers\n";
print_endline
"####################################################################\n";
- Printf.printf "pushd %s/pg-ci-coq\n" !src_dir;
List.iter
(fun coqv ->
+ if !pushdir_printed = `NO ||
+ (!pushdir_printed = `RC && coqv.release_candidate = None) ||
+ (!pushdir_printed = `REGULAR && coqv.release_candidate <> None)
+ then
+ begin
+ if !pushdir_printed <> `NO
+ then
+ print_endline "popd";
+ if coqv.release_candidate = None
+ then
+ begin
+ Printf.printf "pushd %s/coq\n" !src_dir;
+ pushdir_printed := `REGULAR;
+ end
+ else
+ begin
+ Printf.printf "pushd %s/coq-rc\n" !src_dir;
+ pushdir_printed := `RC;
+ end;
+ end;
Printf.printf
("docker image build -t proofgeneral/ci-coq:%s \\\n"
+ (* XXX this should depend on the coq version *)
+ ^^ "\t--build-arg PGCI_BASE_TAG=debian-13-ocaml-5.3.0 \\\n"
^^ "\t--build-arg COQ_NAME=%s \\\n"
^^ "\t--build-arg COQ_VERSION=%s .\n")
(coq_tag coqv)
(if compare_versions coqv coq_9_version < 0
then "coq"
- else "rocq-prover")
+ else "rocq-core")
(version_to_string coqv);
Printf.printf "docker image push proofgeneral/ci-coq:%s\n\n"
(coq_tag coqv);
)
missing;
- print_endline "popd";
+ if !pushdir_printed <> `NO
+ then
+ print_endline "popd\n";
end;
del_now
@@ -1230,6 +1290,7 @@ let check_coq_containers coqs =
*)
let print_coq_emacs_build_command (coq, emacses) =
let coq_version = version_to_string coq in
+ let coq_version_tag = version_to_tag_string coq in
print_endline
"##############################################";
Printf.printf "# built Coq %s containers\n\n" coq_version;
@@ -1242,7 +1303,7 @@ let print_coq_emacs_build_command (coq, emacses) =
^^ "\t--build-arg COQ_VERSION=%s \\\n"
^^ "\t--build-arg EMACS_VERSION=%s .\n")
coq_emacs_tag
- coq_version
+ coq_version_tag
emacs_version;
Printf.printf
"docker image push proofgeneral/coq-emacs:%s\n\n" coq_emacs_tag;
@@ -1288,7 +1349,7 @@ let check_coq_emacs_containers coqs emacses conts =
print_endline "# build coq-emacs containers";
print_endline
"####################################################################\n";
- Printf.printf "pushd %s/pg-ci-emacs\n\n" !src_dir;
+ Printf.printf "pushd %s/emacs\n\n" !src_dir;
List.iter print_coq_emacs_build_command (pairs_to_keyed_list missing);
print_endline "popd"
end;
@@ -1425,18 +1486,19 @@ let delete_coq_containers token coqs =
(* Output Coq/Emacs versions on channel oc for
* .github/workflows/test.yml for those jobs that need Coq and Emacs.
* ci_pairs is the matrix for CI and coqs and emacses are the indexed
- * version lists of Coq and Emacs.
+ * version lists of Coq and Emacs. Note that we need to output the
+ * docker tags, which substitude - for +.
*)
let output_ci_coq_emacs_versions coqs emacses ci_pairs oc =
let last_coq_index = snd (list_last coqs) in
let last_emacs_index = snd (list_last emacses) in
for coq_i = 0 to last_coq_index do
- let coq_version = version_to_string (get_index_version coq_i coqs) in
+ let coq_version = version_to_tag_string (get_index_version coq_i coqs) in
for emacs_i = 0 to last_emacs_index do
if ci_pairs.(coq_i).(emacs_i) <> Unused
then
let emacs_version =
- version_to_string (get_index_version emacs_i emacses) in
+ version_to_tag_string (get_index_version emacs_i emacses) in
Printf.fprintf oc " - coq-%s-emacs-%s\n"
coq_version emacs_version;
done
@@ -1633,11 +1695,13 @@ let main() =
end;
if !do_pg_ci_update then
begin
- (* In README.md: update Coq/Emacs oldest activley supported
- * version, the number of containers, the container table, the
- * number of tested version pairs, and the tested version pair
- * table.
+ (* In README.md: update the LTS table, the Coq/Emacs oldest
+ * activley supported version, the number of containers, the
+ * container table, the number of tested version pairs, and the
+ * tested version pair table.
*)
+ md_file_change_wrapper readme_file "lts-versions"
+ (print_debian_ubuntu_release_table lts);
md_file_change_wrapper readme_file "coq-emacs-versions"
(print_actively_supported_coq_emacs_table
first_active_coq first_active_emacs);
