branch: elpa/proof-general
commit 1776d18d7aca8cfcf2b6b135bf6de2a4ca67139e
Merge: 85cde55a86 491857f378
Author: hendriktews <hend...@askra.de>
Commit: GitHub <nore...@github.com>
Merge pull request #810 from hendriktews/test-9
CI: add Coq 9.0+rc1
---
.github/workflows/test.yml | 27 +++++++
ci/doc/README.md | 28 ++++---
ci/doc/coq-emacs-releases.org | 123 ++++++++++++++++---------------
ci/doc/currently-used-coq-emacs-versions | 9 +++
ci/doc/currently-used-coq-nix-versions | 1 +
ci/simple-tests/coq-test-omit-proofs.el | 8 +-
ci/tools/cipg.ml | 84 +++++++++++----------
7 files changed, 170 insertions(+), 110 deletions(-)
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index a303453960..b025c07bef 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -142,6 +142,15 @@ jobs:
- coq-8.20.1-emacs-29.2
- coq-8.20.1-emacs-29.3
- coq-8.20.1-emacs-29.4
+ - coq-9.0-rc1-emacs-26.3
+ - coq-9.0-rc1-emacs-27.1
+ - coq-9.0-rc1-emacs-27.2
+ - coq-9.0-rc1-emacs-28.1
+ - coq-9.0-rc1-emacs-28.2
+ - coq-9.0-rc1-emacs-29.1
+ - coq-9.0-rc1-emacs-29.2
+ - coq-9.0-rc1-emacs-29.3
+ - coq-9.0-rc1-emacs-29.4
# CIPG change marker end
# don't cancel all in-progress jobs if one matrix job fails:
fail-fast: false
@@ -217,6 +226,15 @@ jobs:
- coq-8.20.1-emacs-29.2
- coq-8.20.1-emacs-29.3
- coq-8.20.1-emacs-29.4
+ - coq-9.0-rc1-emacs-26.3
+ - coq-9.0-rc1-emacs-27.1
+ - coq-9.0-rc1-emacs-27.2
+ - coq-9.0-rc1-emacs-28.1
+ - coq-9.0-rc1-emacs-28.2
+ - coq-9.0-rc1-emacs-29.1
+ - coq-9.0-rc1-emacs-29.2
+ - coq-9.0-rc1-emacs-29.3
+ - coq-9.0-rc1-emacs-29.4
# CIPG change marker end
# don't cancel all in-progress jobs if one matrix job fails:
fail-fast: false
@@ -288,6 +306,15 @@ jobs:
- coq-8.20.1-emacs-29.2
- coq-8.20.1-emacs-29.3
- coq-8.20.1-emacs-29.4
+ - coq-9.0-rc1-emacs-26.3
+ - coq-9.0-rc1-emacs-27.1
+ - coq-9.0-rc1-emacs-27.2
+ - coq-9.0-rc1-emacs-28.1
+ - coq-9.0-rc1-emacs-28.2
+ - coq-9.0-rc1-emacs-29.1
+ - coq-9.0-rc1-emacs-29.2
+ - coq-9.0-rc1-emacs-29.3
+ - coq-9.0-rc1-emacs-29.4
# CIPG change marker end
# don't cancel all in-progress jobs if one matrix job fails:
fail-fast: false
diff --git a/ci/doc/README.md b/ci/doc/README.md
index 2996c55d43..e312e613ef 100644
--- a/ci/doc/README.md
+++ b/ci/doc/README.md
@@ -153,7 +153,8 @@ of the following points is true for *cv* and *ev*.
This point is motivated by the compatibility of newest versions.
-#. The Coq version *cv* is a release candidate.
+#. The Coq version *cv* is a release candidate not superseded by a
+ later release candidate or a release.
This point is motivated by the compatibility of release candidates.
@@ -168,7 +169,7 @@ 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 -->
-57
+66
<!-- CIPG change marker end -->
containers.
@@ -189,6 +190,7 @@ containers.
| 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-rc1 | | RC | RC | RC | RC | RC | RC | RC | RC |
RC |
<!-- CIPG change marker end -->
In the table above,
@@ -274,7 +276,8 @@ following points is true for *cv* and *ev*.
This point is motivated by the compatibility of newest versions.
-#. The Coq version *cv* is a release candidate.
+#. The Coq version *cv* is a release candidate not superseded by a
+ later release candidate or a release.
This point is motivated by the compatibility of release candidates.
@@ -285,7 +288,7 @@ 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 -->
-34
+43
<!-- CIPG change marker end -->
version pairs for the Proof General interaction tests with Coq.
@@ -306,6 +309,7 @@ version pairs for the Proof General interaction tests with
Coq.
| 8.18.0 | | X | X | | | X | | | X | N
|
| 8.19.2 | | X | X | | | X | | | X | N
|
| 8.20.1 | | X | X | N | N | X | N | N | X | N
|
+| 9.0-rc1 | | RC | RC | RC | RC | RC | RC | RC | RC |
RC |
<!-- CIPG change marker end -->
See [Container build strategy](#contbuild) for an explanation of the
@@ -315,7 +319,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 -->
-131
+158
<!-- CIPG change marker end -->
github checks.
@@ -374,8 +378,13 @@ that `cipg` can process it.
: are specified with a date and an Emacs version.
Debian or Ubuntu releases
- : are specified with a date, a distribution name and an EOL date.
+ : are specified with a date, a distribution name, and an EOL date.
+ One line can be of several kinds: If a date, a Coq version, an
+ Emacs version, a Debian distribution name, and an EOL date is
+ present in a certain line, then this line specifies a Coq release,
+ an Emacs release, and a Debian release all together.
+
#. The Coq and Emacs versions of an Debian or Ubuntu release may be
omitted. If they are not present, they are taken from the last
preceding line containing the respective version (the table is
@@ -408,10 +417,9 @@ that `cipg` can process it.
YYYY/MM. Trailing non-digit characters are ignored. I use `?` to
indicate EOL dates that have not yet been fixed.
-#. Versions of release candidates must be of the form `8.10rc` or
- `8.10-rc`. `cipg` is not able to recognize outdated release
- candidates. The release candidate must therefore be deleted when
- the release happens.
+#. Versions of release candidates must be of the form
+ `8.10-rc1`. Outdated release candidates may be deleted from the
+ table.
## `cipg`
diff --git a/ci/doc/coq-emacs-releases.org b/ci/doc/coq-emacs-releases.org
index 80649c6887..67e86a6fbc 100644
--- a/ci/doc/coq-emacs-releases.org
+++ b/ci/doc/coq-emacs-releases.org
@@ -11,64 +11,65 @@
automatically, therefore please observe the requirements in Section
"Release table" in file README.md!
-| date | coq | emacs | distribution name | EOL | historic |
-|---------+--------+-------+-------------------+----------+----------|
-| 2025/01 | 8.20.1 | | | | |
-| 2024/09 | 8.20.0 | | | | |
-| 2024/06 | 8.19.2 | 29.4 | | | |
-| 2024/03 | 8.19.1 | 29.3 | | | |
-| 2024/01 | 8.19.0 | 29.2 | | | |
-| 2024/04 | | 29.3 | ubu 24 noble num | 2029/06 | |
-| 2023/09 | 8.18.0 | | | | |
-| 2023/07 | | 29.1 | | | X |
-| 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/04 | | | ubu 23 lun lobs | 2024/01 | |
-| 2022/11 | 8.16.1 | | | | X |
-| 2022/09 | 8.16.0 | 28.2 | | | |
-| 2022/05 | 8.15.2 | | | | |
-| 2022/04 | | 28.1 | | | X |
-| 2022/03 | 8.15.1 | | | | |
-| 2022/04 | | 27.1 | ubu 22 jammy jel | 2027/04 | |
-| 2022/01 | 8.15.0 | | | | |
-| 2021/12 | 8.14.1 | | | | X |
-| 2021/10 | 8.14.0 | | | | |
-| 2021/04 | 8.13.2 | | | | X |
-| 2021/03 | | 27.2 | | | |
-| 2021/02 | 8.13.1 | | | | |
-| 2021/01 | 8.13.0 | | | | |
-| 2020/12 | 8.12.2 | | | | X |
-| 2020/11 | 8.12.1 | | | | |
-| 2021/10 | | | ubu 21 impish | 2022/07 | |
-| 2021/08 | | | deb 11 bullseye | 2024/08 | |
-| 2020/08 | | 27.1 | | | |
-| 2020/07 | 8.12.0 | | | | |
-| 2020/06 | 8.11.2 | | | | |
-| 2020/04 | 8.11.1 | | | | X |
-| 2020/04 | | | ubu 20.4 focal | 2025/04 | |
-| 2020/01 | 8.11.0 | | | | |
-| 2019/11 | 8.10.2 | | | | |
-| 2019/10 | 8.10.1 | | | | X |
-| 2019/10 | 8.10.0 | | | | |
-| 2019/08 | | 26.3 | | | |
-| 2019/05 | 8.9.1 | | | | X |
-| 2019/07 | | | deb 10 buster | 2022/09 | |
-| 2019/04 | | 26.2 | | | |
-| 2019/01 | 8.9.0 | | | | |
-| 2018/09 | 8.8.2 | | | | X |
-| 2018/07 | 8.8.1 | | | | |
-| 2018/05 | | 26.1 | | | |
-| 2018/04 | 8.8.0 | | | | |
-| 2018/02 | 8.7.2 | | | | |
-| 2017/12 | 8.7.1 | | | | X |
-| 2017/10 | 8.7.0 | | | | |
-| 2017/09 | | 25.3 | | | |
-| 2017/07 | 8.6.1 | | | | X |
-| 2018/04 | | | ubu 18.04 bionic | 2023/04 | |
-| 2017/04 | | 25.2 | | | |
-| 2017/06 | | | deb 9 stretch | 2020/06 | |
-| 2016/12 | 8.6 | | | | |
-| 2016/10 | 8.5pl3 | | | | |
-| 2016/09 | | 25.1 | | | |
+| date | coq | emacs | distribution name | EOL | historic |
+|---------+---------+-------+-------------------+----------+----------|
+| 2025/01 | 9.0-rc1 | | | | |
+| 2025/01 | 8.20.1 | | | | |
+| 2024/09 | 8.20.0 | | | | |
+| 2024/06 | 8.19.2 | 29.4 | | | |
+| 2024/03 | 8.19.1 | 29.3 | | | |
+| 2024/01 | 8.19.0 | 29.2 | | | |
+| 2024/04 | | 29.3 | ubu 24 noble num | 2029/06 | |
+| 2023/09 | 8.18.0 | | | | |
+| 2023/07 | | 29.1 | | | X |
+| 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/04 | | | ubu 23 lun lobs | 2024/01 | |
+| 2022/11 | 8.16.1 | | | | X |
+| 2022/09 | 8.16.0 | 28.2 | | | |
+| 2022/05 | 8.15.2 | | | | |
+| 2022/04 | | 28.1 | | | X |
+| 2022/03 | 8.15.1 | | | | |
+| 2022/04 | | 27.1 | ubu 22 jammy jel | 2027/04 | |
+| 2022/01 | 8.15.0 | | | | |
+| 2021/12 | 8.14.1 | | | | X |
+| 2021/10 | 8.14.0 | | | | |
+| 2021/04 | 8.13.2 | | | | X |
+| 2021/03 | | 27.2 | | | |
+| 2021/02 | 8.13.1 | | | | |
+| 2021/01 | 8.13.0 | | | | |
+| 2020/12 | 8.12.2 | | | | X |
+| 2020/11 | 8.12.1 | | | | |
+| 2021/10 | | | ubu 21 impish | 2022/07 | |
+| 2021/08 | | | deb 11 bullseye | 2024/08 | |
+| 2020/08 | | 27.1 | | | |
+| 2020/07 | 8.12.0 | | | | |
+| 2020/06 | 8.11.2 | | | | |
+| 2020/04 | 8.11.1 | | | | X |
+| 2020/04 | | | ubu 20.4 focal | 2025/04 | |
+| 2020/01 | 8.11.0 | | | | |
+| 2019/11 | 8.10.2 | | | | |
+| 2019/10 | 8.10.1 | | | | X |
+| 2019/10 | 8.10.0 | | | | |
+| 2019/08 | | 26.3 | | | |
+| 2019/05 | 8.9.1 | | | | X |
+| 2019/07 | | | deb 10 buster | 2022/09 | |
+| 2019/04 | | 26.2 | | | |
+| 2019/01 | 8.9.0 | | | | |
+| 2018/09 | 8.8.2 | | | | X |
+| 2018/07 | 8.8.1 | | | | |
+| 2018/05 | | 26.1 | | | |
+| 2018/04 | 8.8.0 | | | | |
+| 2018/02 | 8.7.2 | | | | |
+| 2017/12 | 8.7.1 | | | | X |
+| 2017/10 | 8.7.0 | | | | |
+| 2017/09 | | 25.3 | | | |
+| 2017/07 | 8.6.1 | | | | X |
+| 2018/04 | | | ubu 18.04 bionic | 2023/04 | |
+| 2017/04 | | 25.2 | | | |
+| 2017/06 | | | deb 9 stretch | 2020/06 | |
+| 2016/12 | 8.6 | | | | |
+| 2016/10 | 8.5pl3 | | | | |
+| 2016/09 | | 25.1 | | | |
diff --git a/ci/doc/currently-used-coq-emacs-versions
b/ci/doc/currently-used-coq-emacs-versions
index 616c1ce485..2c7a467b6d 100644
--- a/ci/doc/currently-used-coq-emacs-versions
+++ b/ci/doc/currently-used-coq-emacs-versions
@@ -55,3 +55,12 @@ coq-8.20.1-emacs-29.1
coq-8.20.1-emacs-29.2
coq-8.20.1-emacs-29.3
coq-8.20.1-emacs-29.4
+coq-9.0-rc1-emacs-26.3
+coq-9.0-rc1-emacs-27.1
+coq-9.0-rc1-emacs-27.2
+coq-9.0-rc1-emacs-28.1
+coq-9.0-rc1-emacs-28.2
+coq-9.0-rc1-emacs-29.1
+coq-9.0-rc1-emacs-29.2
+coq-9.0-rc1-emacs-29.3
+coq-9.0-rc1-emacs-29.4
diff --git a/ci/doc/currently-used-coq-nix-versions
b/ci/doc/currently-used-coq-nix-versions
index d28d4f414f..fad04ae37c 100644
--- a/ci/doc/currently-used-coq-nix-versions
+++ b/ci/doc/currently-used-coq-nix-versions
@@ -10,3 +10,4 @@
8.18.0
8.19.2
8.20.1
+9.0-rc1
diff --git a/ci/simple-tests/coq-test-omit-proofs.el
b/ci/simple-tests/coq-test-omit-proofs.el
index 20a54b6e82..f2ec735eb2 100644
--- a/ci/simple-tests/coq-test-omit-proofs.el
+++ b/ci/simple-tests/coq-test-omit-proofs.el
@@ -132,6 +132,8 @@ In particular, test that with proof-omit-proofs-option
configured:
;; There should be a Qed with no error or message after it
(should
(or
+ ;; for Rocq 9.0
+ (looking-at "Qed\\.\n\n<prompt>Rocq <")
;; for Coq 8.11 and later
(looking-at "Qed\\.\n\n<prompt>Coq <")
;; for Coq 8.10 and earlier
@@ -170,7 +172,11 @@ In particular, test that with proof-omit-proofs-option
configured:
(should (search-forward "</infomsg>" nil t))
(forward-line 1))
;; no other messages or errors before the next prompt
- (should (looking-at "\n<prompt>Coq <")))
+ (should (or
+ ;; for Rocq
+ (looking-at "\n<prompt>Rocq <")
+ ;; for Coq
+ (looking-at "\n<prompt>Coq <"))))
;; Check 4: check proof-omitted-proof-face is active at marker 3
(message "4: check proof-omitted-proof-face is active at marker 3")
diff --git a/ci/tools/cipg.ml b/ci/tools/cipg.ml
index 600b0e22ff..d72304384d 100644
--- a/ci/tools/cipg.ml
+++ b/ci/tools/cipg.ml
@@ -95,11 +95,11 @@ type version = {
major : int;
minor : int;
patch : int option;
- release_candidate : bool;
+ release_candidate : int option;
}
let null_version = {major = 0; minor = 0; patch = None;
- release_candidate = false; }
+ release_candidate = None; }
(* record for lines of the Coq/Emacs/Debian/Ubuntu release table *)
type release_record = {
@@ -214,7 +214,9 @@ let today = U.time()
(* sort Debian/Ubuntu releases by their end-of-live date *)
let sort_lts = List.sort (fun a b -> compare a.eol_date b.eol_date)
-(* compare version records, taking the release_candidate field into account *)
+(* Compare version records, taking the release_candidate field into
+ account. Must return -1 if [a < b], 0 if [a = b], and 1 if [a > b].
+ *)
let compare_versions a b =
let x = compare a.major b.major in
if x = 0
@@ -225,16 +227,16 @@ let compare_versions a b =
match (a.patch, b.patch) with
| (Some pa, Some pb) -> compare pa pb
| (None, None) -> 0
- | (Some pa, None) -> compare pa 0
- | (None, Some pb) -> compare 0 pb
+ | (Some pa, None) -> 1 (* some patch is bigger than no patch or RC *)
+ | (None, Some pb) -> -1 (* some patch is smaller than no patch or RC
*)
in
if x = 0
then
match (a.release_candidate, b.release_candidate) with
- | (true, false) -> -1
- | (false, true) -> 1
- | (true, true)
- | (false, false) -> 0
+ | (Some rc1, Some rc2) -> compare rc1 rc2
+ | (None, None) -> 0
+ | (Some rc, None) -> -1
+ | (None, Some rc) -> 1
else x
else x
else x
@@ -306,11 +308,13 @@ let scan_year_month_date s =
else
Some (Scanf.sscanf s "%d/%d" norm_tm_date)
-(* Scan a version in string s in the form <major>.<minor>[rc], where
- the [rc] is optional, or <major>.<minor>[.<patch>], where the patch
- level is optional. Return a version option, where None is used when
- s is empty. Trailing characters after <minor> are ignored, but if
- there is a dot, a patch level must follow <minor>. *)
+(* Scan a version in string s in the form <major>.<minor>,
+ <major>.<minor>.<patch>, or <major>.<minor>-rc<n>. Return a version
+ option, where None is used when s is empty. Trailing characters
+ after <minor> are ignored, but if there is a dot, a patch level
+ must follow <minor> and if there is a plus or minus an rc version
+ must follow.
+ *)
let scan_version s =
if s = ""
then None
@@ -321,16 +325,16 @@ let scan_version s =
let (rc, patch) =
if i + 1 < String.length s
then
- if String.sub s i 2 = "rc"
- then (true, None)
- else
- Scanf.bscanf s_ch "%c"
- (function
- | '.' -> Scanf.bscanf s_ch "%d"
- (fun patch -> (false, Some patch))
- | _ -> (false, None)
- )
- else (false, None)
+ Scanf.bscanf s_ch "%c"
+ (function
+ | '.' -> Scanf.bscanf s_ch "%d"
+ (fun patch -> (None, Some patch))
+ | '+'
+ | '-' -> Scanf.bscanf s_ch "rc%d"
+ (fun rc -> (Some rc, None))
+ | _ -> (None, None)
+ )
+ else (None, None)
in
Some {major = ma; minor = mi;
patch = patch;
@@ -658,7 +662,7 @@ let select_newest first_emacs first_coq coqs emacses conts =
(* skip over coq RC versions *)
let newest_non_rc_coq =
snd (List.find
- (fun (coq_v, coq_i) -> coq_v.release_candidate = false)
+ (fun (coq_v, coq_i) -> coq_v.release_candidate = None)
(List.rev coqs))
in
for em_i = first_emacs to newest_emacs do
@@ -674,7 +678,7 @@ let select_coq_rc_version first_emacs coqs emacses conts =
let first_emacs = get_version_index first_emacs emacses in
let newest_emacs = snd (list_last emacses) in
let (coq_v, coq_i) = list_last coqs in
- if coq_v.release_candidate
+ if coq_v.release_candidate <> None
then
for em_i = first_emacs to newest_emacs do
conts.(coq_i).(em_i) <- RC
@@ -844,7 +848,9 @@ let version_to_string v =
(match v.patch with
| None -> ""
| Some p -> Printf.sprintf ".%d" p)
- (if v.release_candidate then "rc" else "")
+ (match v.release_candidate with
+ | None -> ""
+ | 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
@@ -1008,7 +1014,7 @@ let rec read_nix_containers inc nix_conts =
(match scan_version line with
| None -> assert false
| Some v ->
- if v.release_candidate || v.patch <> None
+ if v.release_candidate <> None || v.patch <> None
then read_nix_containers inc (v :: nix_conts)
else read_nix_containers inc nix_conts
)
@@ -1019,6 +1025,7 @@ let rec read_nix_containers inc nix_conts =
*)
let get_nix_containers () =
let inc = docker_tags_channel "coq-nix" in
+ (* let inc = U.open_process_in "cat coq-nix-tags-for-testing" in *)
let nix_conts = read_nix_containers inc [] in
(match U.close_process_in inc with
| WEXITED(0) -> ()
@@ -1044,15 +1051,15 @@ let read_coq_emacs_tag line =
| '-' -> None
| _ -> raise (Scanf.Scan_failure ". or - expected after coq minor")
in
- let (coq_rc, emacs_major, emacs_minor) =
- Scanf.bscanf sb "%[^-]"
+ let coq_rc =
+ Scanf.bscanf sb "%c"
(function
- | "emacs" -> Scanf.bscanf sb "-%d.%d" (fun a b -> (false, a, b))
- | "rc"
- | "rc1"
- | "rc2" -> Scanf.bscanf sb "-emacs-%d.%d" (fun a b -> (true, a, b))
- | _ -> raise (Scanf.Scan_failure "rc or emacs expected")
- )
+ | 'e' -> None
+ | 'r' -> Scanf.bscanf sb "c%d-e" (fun rc -> Some rc)
+ | _ -> raise (Scanf.Scan_failure "rc or emacs expected"))
+ in
+ let (emacs_major, emacs_minor) =
+ Scanf.bscanf sb "macs-%d.%d" (fun a b -> (a, b))
in
({major = coq_major;
minor = coq_minor;
@@ -1062,7 +1069,7 @@ let read_coq_emacs_tag line =
{major = emacs_major;
minor = emacs_minor;
patch = None;
- release_candidate = false;
+ release_candidate = None;
}
)
)
@@ -1076,7 +1083,7 @@ let rec read_all_coq_emacs_tags inc coq_emacs =
| line ->
let (coq_v, emacs_v) as vp = read_coq_emacs_tag line in
let coq_emacs =
- if coq_v.release_candidate || coq_v.patch <> None
+ if coq_v.release_candidate <> None || coq_v.patch <> None
then vp :: coq_emacs
else coq_emacs
in
@@ -1089,6 +1096,7 @@ let rec read_all_coq_emacs_tags inc coq_emacs =
*)
let get_coq_emacs_containers () =
let inc = docker_tags_channel "coq-emacs" in
+ (* let inc = U.open_process_in "cat coq-emacs-tags-for-testing" in *)
let coq_emacs = read_all_coq_emacs_tags inc [] in
(match U.close_process_in inc with
| WEXITED(0) -> ()
