Skip to content

CI: update for Coq 8.19+rc1 #718

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
merged 2 commits into from
Jan 2, 2024
Merged

CI: update for Coq 8.19+rc1 #718

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
13d731a
ci/coq-tests: Disable tests test_wholefile.v tests
hendriktews Dec 26, 2023
10cb65c
CI: update for Coq 8.19+rc1
hendriktews Dec 26, 2023
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
30 changes: 24 additions & 6 deletions .github/workflows/test.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -97,10 +97,8 @@ jobs:
- coq-8.13-emacs-29.1
- coq-8.14-emacs-27.2
- coq-8.14-emacs-29.1
- coq-8.15-emacs-26.3
- coq-8.15-emacs-27.1
- coq-8.15-emacs-28.1
- coq-8.15-emacs-28.2
- coq-8.15-emacs-29.1
- coq-8.16-emacs-26.3
- coq-8.16-emacs-27.1
Expand All @@ -116,6 +114,14 @@ jobs:
- coq-8.18-emacs-28.1
- coq-8.18-emacs-28.2
- coq-8.18-emacs-29.1
- coq-8.19-rc-emacs-26.1
- coq-8.19-rc-emacs-26.2
- coq-8.19-rc-emacs-26.3
- coq-8.19-rc-emacs-27.1
- coq-8.19-rc-emacs-27.2
- coq-8.19-rc-emacs-28.1
- coq-8.19-rc-emacs-28.2
- coq-8.19-rc-emacs-29.1
# at most 20 concurrent jobs per free account
# cf. https://help.github.com/en/actions/reference/workflow-syntax-for-github-actions#usage-limit
max-parallel: 6
Expand Down Expand Up @@ -164,10 +170,8 @@ jobs:
- coq-8.13-emacs-29.1
- coq-8.14-emacs-27.2
- coq-8.14-emacs-29.1
- coq-8.15-emacs-26.3
- coq-8.15-emacs-27.1
- coq-8.15-emacs-28.1
- coq-8.15-emacs-28.2
- coq-8.15-emacs-29.1
- coq-8.16-emacs-26.3
- coq-8.16-emacs-27.1
Expand All @@ -183,6 +187,14 @@ jobs:
- coq-8.18-emacs-28.1
- coq-8.18-emacs-28.2
- coq-8.18-emacs-29.1
- coq-8.19-rc-emacs-26.1
- coq-8.19-rc-emacs-26.2
- coq-8.19-rc-emacs-26.3
- coq-8.19-rc-emacs-27.1
- coq-8.19-rc-emacs-27.2
- coq-8.19-rc-emacs-28.1
- coq-8.19-rc-emacs-28.2
- coq-8.19-rc-emacs-29.1
# don't cancel all in-progress jobs if one matrix job fails:
fail-fast: false
steps:
Expand Down Expand Up @@ -224,10 +236,8 @@ jobs:
- coq-8.13-emacs-29.1
- coq-8.14-emacs-27.2
- coq-8.14-emacs-29.1
- coq-8.15-emacs-26.3
- coq-8.15-emacs-27.1
- coq-8.15-emacs-28.1
- coq-8.15-emacs-28.2
- coq-8.15-emacs-29.1
- coq-8.16-emacs-26.3
- coq-8.16-emacs-27.1
Expand All @@ -243,6 +253,14 @@ jobs:
- coq-8.18-emacs-28.1
- coq-8.18-emacs-28.2
- coq-8.18-emacs-29.1
- coq-8.19-rc-emacs-26.1
- coq-8.19-rc-emacs-26.2
- coq-8.19-rc-emacs-26.3
- coq-8.19-rc-emacs-27.1
- coq-8.19-rc-emacs-27.2
- coq-8.19-rc-emacs-28.1
- coq-8.19-rc-emacs-28.2
- coq-8.19-rc-emacs-29.1
# don't cancel all in-progress jobs if one matrix job fails:
fail-fast: false

Expand Down
55 changes: 30 additions & 25 deletions ci/coq-tests.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -258,31 +258,36 @@ For example, COMMENT could be (*test-definition*)"
(should (equal (proof-queue-or-locked-end) proof-point))))))


(ert-deftest 060_coq-test-wholefile ()
;; test_wholefile.v triggers a fatal warning in 8.17, see also #698
:expected-result (if (coq--is-v817) :failed :passed)
"Test `proof-process-buffer'."
(coq-fixture-on-file
(coq-test-full-path "test_wholefile.v")
(lambda ()
(let ((proof-point (save-excursion
(coq-test-goto-before "Theorem")
(search-forward "Qed."))))
(proof-process-buffer)
(proof-shell-wait)
(should (equal (proof-queue-or-locked-end) proof-point))))))


(ert-deftest 070_coq-test-regression-wholefile-no-proof ()
"Regression test for no proof bug"
(coq-fixture-on-file
(coq-test-full-path "test_wholefile.v")
(lambda ()
(proof-process-buffer)
(proof-shell-wait)
(goto-char (point-min))
(insert "(*.*)")
(should (equal (proof-queue-or-locked-end) (point-min))))))
;; Disable tests that use test_wholefile.v. The file is outdated, uses
;; deprecated features, is prone to caues Coq errors and therefore
;; causes the tests to fail. See #698 and commit
;; bd3615b442974f1e1c3fca0252e081a05525d26b.
;;
;; (ert-deftest 060_coq-test-wholefile ()
;; ;; test_wholefile.v triggers a fatal warning in 8.17, see also #698
;; :expected-result (if (coq--is-v817) :failed :passed)
;; "Test `proof-process-buffer'."
;; (coq-fixture-on-file
;; (coq-test-full-path "test_wholefile.v")
;; (lambda ()
;; (let ((proof-point (save-excursion
;; (coq-test-goto-before "Theorem")
;; (search-forward "Qed."))))
;; (proof-process-buffer)
;; (proof-shell-wait)
;; (should (equal (proof-queue-or-locked-end) proof-point))))))
;;
;;
;; (ert-deftest 070_coq-test-regression-wholefile-no-proof ()
;; "Regression test for no proof bug"
;; (coq-fixture-on-file
;; (coq-test-full-path "test_wholefile.v")
;; (lambda ()
;; (proof-process-buffer)
;; (proof-shell-wait)
;; (goto-char (point-min))
;; (insert "(*.*)")
;; (should (equal (proof-queue-or-locked-end) (point-min))))))

(ert-deftest 080_coq-test-regression-show-proof-stepwise()
"Regression test for the \"Show Proof\" option"
Expand Down
64 changes: 32 additions & 32 deletions ci/doc/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -137,22 +137,22 @@ we build containers for the historic pairs of the last 6 years as
passively supported versions.


This results in 43 containers.

| | 25.3 | 26.1 | 26.2 | 26.3 | 27.1 | 27.2 | 28.1 | 28.2 | 29.1 |
|---------+------+------+------+------+------+------+------+------+------|
| 8.7 | H | | | | | | | | |
| 8.8 | | H | | | | | | | |
| 8.9 | | | H | | | | | | |
| 8.10 | | | | H | | | | | |
| 8.11 | | | | SUP | | | | | N |
| 8.12 | | | | SUP | SUP | | | | N |
| 8.13 | | | | SUP | SUP | H | | | N |
| 8.14 | | | | X | X | X | X | X | X |
| 8.15 | | | | X | X | X | X | X | X |
| 8.16 | | | | X | X | X | X | X | X |
| 8.17 | | | | X | X | X | X | X | X |
| 8.18 | | | | X | X | X | X | X | X |
This results in 48 containers.

| | 26.1 | 26.2 | 26.3 | 27.1 | 27.2 | 28.1 | 28.2 | 29.1 |
|---------+------+------+------+------+------+------+------+------|
| 8.8 | H | | | | | | | |
| 8.9 | | H | | | | | | |
| 8.10 | | | H | | | | | |
| 8.11 | | | SUP | | | | | N |
| 8.12 | | | SUP | SUP | | | | N |
| 8.13 | | | SUP | SUP | H | | | N |
| 8.14 | | | SUP | SUP | H | | | N |
| 8.15 | | | X | X | X | X | X | X |
| 8.16 | | | X | X | X | X | X | X |
| 8.17 | | | X | X | X | X | X | X |
| 8.18 | | | X | X | X | X | X | X |
| 8.19-rc | RC | RC | RC | RC | RC | RC | RC | RC |

In the table above,

Expand Down Expand Up @@ -245,23 +245,23 @@ following points is true for *cv* and *ev*.
Running Proof General interaction tests with Coq for passively
supported versions is work in progress.

This results in 26 version pairs for the Proof General interaction
This results in 33 version pairs for the Proof General interaction
tests with Coq.

| | 25.3 | 26.1 | 26.2 | 26.3 | 27.1 | 27.2 | 28.1 | 28.2 | 29.1 |
|---------+------+------+------+------+------+------+------+------+------|
| 8.7 | | | | | | | | | |
| 8.8 | | | | | | | | | |
| 8.9 | | | | | | | | | |
| 8.10 | | | | | | | | | |
| 8.11 | | | | SUP | | | | | N |
| 8.12 | | | | | SUP | | | | N |
| 8.13 | | | | | | H | | | N |
| 8.14 | | | | | | H | | | N |
| 8.15 | | | | X | X | | H | | N |
| 8.16 | | | | X | X | | | SUP | N |
| 8.17 | | | | X | X | | | X | SUP |
| 8.18 | | | | X | X | N | N | X | X |
| | 26.1 | 26.2 | 26.3 | 27.1 | 27.2 | 28.1 | 28.2 | 29.1 |
|---------+------+------+------+------+------+------+------+------|
| 8.8 | | | | | | | | |
| 8.9 | | | | | | | | |
| 8.10 | | | | | | | | |
| 8.11 | | | SUP | | | | | N |
| 8.12 | | | | SUP | | | | N |
| 8.13 | | | | | H | | | N |
| 8.14 | | | | | H | | | N |
| 8.15 | | | | SUP | | H | | N |
| 8.16 | | | X | X | | | X | N |
| 8.17 | | | X | X | | | X | SUP |
| 8.18 | | | X | X | N | N | X | X |
| 8.19-rc | RC | RC | RC | RC | RC | RC | RC | RC |

See [Container build strategy](#contbuild) for an explanation of the
symbols in the table.
Expand Down Expand Up @@ -363,6 +363,6 @@ that `cipg` can process it.

<!--
!-- Local Variables:
!-- compile-command: "pandoc -N README.md -o README.pdf"
!-- compile-command: "pandoc -N --pdf-engine=lualatex README.md -o README.pdf"
!-- End:
-->
Binary file modified ci/doc/README.pdf
View file
Open in desktop
Binary file not shown.
1 change: 1 addition & 0 deletions ci/doc/coq-emacs-releases.org
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@

| date | coq | emacs | distribution name | EOL | historic |
|---------+--------+-------+-------------------+----------+----------|
| 2023/12 | 8.19rc | | | | |
| 2023/09 | 8.18.0 | | | | |
| 2023/07 | | 29.1 | | | |
| 2023/06 | 8.17.1 | | | | |
Expand Down