Skip to content

CI: update to Rocq 9.1+rc1 #839

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hendriktews merged 1 commit into from
Aug 11, 2025
Merged

CI: update to Rocq 9.1+rc1 #839

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
66 changes: 30 additions & 36 deletions .github/workflows/test.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion ci/compile-tests/002-require-no-dependencies/a.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,6 @@


(* This is line 21 *)
Require Coq.Bool.Bool.
Require Init.Datatypes.
Definition a : nat := 0.
(* This is line 24 *)
2 changes: 1 addition & 1 deletion ci/compile-tests/002-require-no-dependencies/b.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,6 @@


(* This is line 21 *)
Require Coq.Bool.Bool.
Require Init.Datatypes.
Require c.
(* This is line 24 *)
99 changes: 56 additions & 43 deletions ci/doc/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand All @@ -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
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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
Expand All @@ -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.

Expand Down
6 changes: 4 additions & 2 deletions ci/doc/coq-emacs-releases.org
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 | | | |
Expand All @@ -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 | | | |
Expand Down
2 changes: 1 addition & 1 deletion ci/doc/currently-used-ci-coq-versions
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
coq-8.9.1
coq-8.10.2
coq-8.11.2
coq-8.12.2
Expand All @@ -11,3 +10,4 @@ coq-8.18.0
coq-8.19.2
coq-8.20.1
coq-9.0.0
coq-9.1-rc1
Loading
Loading