branch: elpa/proof-general
commit f67da2d0aab7f0488750462e75a655a46f0e8d9d
Merge: d8a049f751 1776d18d7a
Author: Pierre Courtieu <[email protected]>
Commit: Pierre Courtieu <[email protected]>
Merge branch 'master' into fix-rocq-progname
---
.github/workflows/test.yml | 27 +++++++
Makefile | 6 +-
ci/coq-tests.el | 42 ++++++++++-
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/test-indent/indent-backslash-ops.v | 23 ++++++
ci/test-indent/indent-tac.v | 13 ++++
ci/test_error_loc_fst_cmd.v | 4 +
ci/tools/cipg.ml | 84 +++++++++++----------
coq/coq-db.el | 10 +--
coq/coq-indent.el | 7 +-
coq/coq-smie.el | 35 ++++++++-
coq/coq.el | 5 +-
generic/proof-script.el | 2 +-
17 files changed, 299 insertions(+), 128 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/Makefile b/Makefile
index 7a5df56023..b9b28aab5c 100644
--- a/Makefile
+++ b/Makefile
@@ -21,7 +21,7 @@
# Set this according to your version of Emacs.
# NB: this is also used to set default install path names below.
-EMACS=$(shell if [ -z "`which emacs`" ]; then echo "Emacs executable not
found"; exit 1; else echo emacs; fi)
+EMACS=$(shell if [ -z "`command -v emacs`" ]; then echo "Emacs executable not
found"; exit 1; else echo emacs; fi)
# We default to /usr rather than /usr/local because installs of
# desktop and doc files under /usr/local are unlikely to work with
@@ -273,7 +273,7 @@ scripts: bashscripts perlscripts
.PHONY: bashscripts
bashscripts:
- (bash="`which bash`"; \
+ (bash="`command -v bash`"; \
if [ -z "$$bash" ]; then \
echo "Could not find bash - bash paths not checked" >&2; \
exit 0; \
@@ -281,7 +281,7 @@ bashscripts:
.PHONY: perlscripts
perlscripts:
- (perl="`which perl`"; \
+ (perl="`command -v perl`"; \
if [ -z "$$perl" ]; then \
echo "Could not find perl - perl paths not checked" >&2; \
exit 0; \
diff --git a/ci/coq-tests.el b/ci/coq-tests.el
index 78e53dcf93..65bbdd9705 100644
--- a/ci/coq-tests.el
+++ b/ci/coq-tests.el
@@ -446,7 +446,47 @@ For example, COMMENT could be (*test-definition*)"
(coq-test-goto-before "(*proof*)")
(backward-char 3)
(should (span-at (point) 'proofusing))))))
-
+
+
+
+(ert-deftest 110_coq-test-regression_error_on_fst_cmd ()
+ "Test error highlghting in the first line."
+ (coq-fixture-on-file
+ (coq-test-full-path "test_error_loc_fst_cmd.v")
+ (lambda ()
+ (coq-test-goto-before " (*after-error*)")
+ ;; redefining this function locally so that self removing spans
+ ;; remain longer. Cf span.el
+ (cl-letf (((symbol-function 'span-make-self-removing-span)
+ (lambda (beg end &rest props)
+ (let ((ol (span-make beg end)))
+ (while props
+ (overlay-put ol (car props) (cadr props))
+ (setq props (cddr props)))
+ (add-timeout 10 'delete-overlay ol)
+ ol))))
+
+ (let ((proof-cmd-point (save-excursion
+ (coq-test-goto-before "(*after-error*)")
+ (re-search-backward "bar"))))
+ (coq-test-goto-after " (*after-error*)")
+ (proof-goto-point)
+ (proof-shell-wait)
+ (coq-should-buffer-string "Error: The reference bar was not found in
the current environment.")
+ ;; checking that there is an overlay with warning face
+ ;; exactly on "bar". WARNING: this overlay lasts only for 12
+ ;; secs (thx to the add-timeout above), if this test is done
+ ;; in a (very) slow virtual machine this may fail.
+ (should (equal (point) proof-cmd-point))
+ (let ((sp (span-at proof-cmd-point 'face)))
+ (should sp)
+ (should (equal (span-property sp 'face) 'proof-warning-face))
+ (should (equal (span-start sp) proof-cmd-point))
+ ;; coq-8.11 used to hace ending ps shifted by one
+ (should (or (equal (span-end sp) (+ proof-cmd-point (length "bar")))
+ (equal (span-end sp) (+ 1 proof-cmd-point (length
"bar")))))
+ )
+ (should (equal (proof-queue-or-locked-end) (point-min))))))))
(provide 'coq-tests)
;;; coq-tests.el ends here
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 17c10a3eb9..24cd169964 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 Rocq 9 and later
@@ -172,7 +174,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 (or (looking-at "\n<prompt>Coq <") (looking-at "\n<prompt>Rocq
<"))))
+ (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/test-indent/indent-backslash-ops.v
b/ci/test-indent/indent-backslash-ops.v
new file mode 100644
index 0000000000..5af1556458
--- /dev/null
+++ b/ci/test-indent/indent-backslash-ops.v
@@ -0,0 +1,23 @@
+Require Import mathcomp.ssreflect.ssrbool.
+
+Definition xx := nat.
+Module foo.
+ (* from PG issue #757 *)
+ Lemma test:
+ forall a : nat,
+ a \in [::] -> (* "\in" should be detected as one token *)
+ False.
+ Proof.
+ Abort.
+ Qed.
+
+ Lemma test2:
+ forall a : nat,
+ a \in (* "\in" should be detected as one token *)
+ [::] ->
+ False.
+ Proof.
+ Abort.
+ Qed.
+End foo.
+
diff --git a/ci/test-indent/indent-tac.v b/ci/test-indent/indent-tac.v
index 4a27e7038b..77a9987685 100644
--- a/ci/test-indent/indent-tac.v
+++ b/ci/test-indent/indent-tac.v
@@ -269,6 +269,19 @@ Module M1.
{ auto.
}
}
+ 1:{
+ destruct n.
+ 2:{ auto.
+ }
+ { auto. }
+ }
+ {
+ destruct n.
+ 2:{
+ auto. }
+ { auto.
+ }
+ }
Qed.
End M2.
End M1.
diff --git a/ci/test_error_loc_fst_cmd.v b/ci/test_error_loc_fst_cmd.v
new file mode 100644
index 0000000000..72c9541aa1
--- /dev/null
+++ b/ci/test_error_loc_fst_cmd.v
@@ -0,0 +1,4 @@
+Definition foo:= bar. (*after-error*)
+
+Definition foobar := nat.
+
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) -> ()
diff --git a/coq/coq-db.el b/coq/coq-db.el
index 6e79e95f3b..680292d161 100644
--- a/coq/coq-db.el
+++ b/coq/coq-db.el
@@ -65,7 +65,7 @@ menu but only in interactive completions.
Example of what could be in your emacs init file:
\(defvar coq-user-tactics-db
- '(
+ \\='(
(\"mytac\" \"mt\" \"mytac # #\" t \"mytac\")
(\"myassert by\" \"massb\" \"myassert ( # : # ) by #\" t \"assert\")
))
@@ -354,19 +354,19 @@ See `coq-syntax-db' for DB structure."
(defconst coq-solve-tactics-face 'coq-solve-tactics-face
"Expression that evaluates to a face.
-Required so that 'coq-solve-tactics-face is a proper facename")
+Required so that \\='coq-solve-tactics-face is a proper facename")
(defconst coq-cheat-face 'coq-cheat-face
"Expression that evaluates to a face.
-Required so that 'coq-cheat-face is a proper facename")
+Required so that \\='coq-cheat-face is a proper facename")
(defconst coq-symbol-binder-face 'coq-symbol-binder-face
"Expression that evaluates to a face.
-Required so that 'coq-symbol-binder-face is a proper facename")
+Required so that \\='coq-symbol-binder-face is a proper facename")
(defconst coq-symbol-face 'coq-symbol-face
"Expression that evaluates to a face.
-Required so that 'coq-symbol-binder-face is a proper facename")
+Required so that \\='coq-symbol-binder-face is a proper facename")
(defconst coq-question-mark-face 'coq-question-mark-face)
diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index b1e3e0425b..aab99837fa 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -208,7 +208,8 @@ position."
(while (coq-looking-at-comment) ;; we are looking for ". " so this is enough
(re-search-backward (concat "\\(?2:"
coq-simple-cmd-ender-prefix-regexp-backward "\\)\\.\\s-") (point-min) 'dummy))
;; unless we reached point-min, jump over the "."
- (when (match-end 2) (goto-char (match-end 2)) (forward-char 1))
+ (when (and (not (eq (point) (point-min))) (match-end 2))
+ (goto-char (match-end 2)) (forward-char 1))
(point))
(defun coq-find-start-of-cmd ()
@@ -216,10 +217,10 @@ position."
(coq-find-previous-endcmd)
(while (not something-found)
(forward-comment (point-max))
- (if (and (looking-at "\\({\\|}\\|\\++\\|\\*+\\|-+\\)")
+ (if (and (looking-at "\\(?1:{\\|}\\|\\++\\|\\*+\\|-+\\|[0-9]+\\s-*:{\\)")
(< (point) p) ;; if we are after the starting point then
anything is the start of the current command, even "#" or ".".
)
- (forward-char 1)
+ (goto-char (match-end 1))
(setq something-found t))))
(point))
diff --git a/coq/coq-smie.el b/coq/coq-smie.el
index d944e94958..5528c65586 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.el
@@ -266,14 +266,18 @@ the token of \".\" is simply \".\"."
;; A variant of smie-default-backward-token that recognize "." and ";"
-;; as single token even if glued at the end of another symbols.
-
+;; as single token even if glued at the end of another symbols. We
+;; glue "\" in front of a word though, to follow ssreflects
+;; ocnvention.
(defun coq-backward-token-fast-nogluing-dot-friends ()
(forward-comment (- (point)))
(let* ((pt (point))
(tok-punc (skip-syntax-backward "."))
(str-punc (buffer-substring-no-properties pt (point))))
- (if (zerop tok-punc) (skip-syntax-backward "w_'"))
+ ;; skip a regular word + one backslash
+ (when (zerop tok-punc)
+ (skip-syntax-backward "w_'")
+ (if (looking-back "\\s-\\\\") (forward-char -1)))
;; Special case: if the symbols found end by "." or ";",
;; then consider this last letter alone as a token
(when (and (not (zerop tok-punc)) (string-match "\\s.+[.;]" str-punc))
@@ -286,7 +290,9 @@ the token of \".\" is simply \".\"."
(let* ((pt (point))
(tok-punc (skip-syntax-forward "."))
(str-punc (buffer-substring-no-properties pt (point))))
- (if (zerop tok-punc) (skip-syntax-forward "w_'"))
+ (if (or (zerop tok-punc) (string-match "\\\\" str-punc)
+ )
+ (skip-syntax-forward "w_'"))
;; Special case: if the symbols found end by "." or ";",
;; then consider this last letter alone as a token
(when (and (not (zerop tok-punc)) (string-match "\\s.+[.;]" str-punc))
@@ -653,6 +659,27 @@ The point should be at the beginning of the command name."
(cdr res)))
(tok))))
+;; Modified from smie.el
+(defun smie-default-forward-token ()
+ (forward-comment (point-max))
+ (buffer-substring-no-properties
+ (point)
+ (let ((dist (skip-syntax-forward ".")))
+
+ (when (or (zerop dist)
+ (and (= 1 dist) (looking-back "\\\\")))
+ (skip-syntax-forward "w_'"))
+ (point))))
+
+(defun smie-default-backward-token ()
+ (forward-comment (- (point)))
+ (buffer-substring-no-properties
+ (point)
+ (progn (when (zerop (skip-syntax-backward "."))
+ (skip-syntax-backward "w_'")
+ (if (looking-back "\\s-\\\\") (forward-char -1)))
+ (point))))
+
(defun coq-smie-backward-token-aux ()
(let* ((tok (smie-default-backward-token)))
(cond
diff --git a/coq/coq.el b/coq/coq.el
index 2e4951f836..496fc2a538 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -2503,13 +2503,15 @@ tacitcs like destruct and induction reuse hypothesis
names by
default, which makes the detection of new hypothesis incorrect.
the hack consists in adding the \"!\" modifier on the argument
destructed, so that it is left in the goal and the name cannot be
-reused. We also had a \"clear\" at the end of the tactic so that
+reused. We also add a \"clear\" at the end of the tactic so that
the whole tactic behaves correctly.
Warning: this makes the error messages (and location) wrong.")
(defun coq-hack-cmd-for-infoH (s)
"return the tactic S hacked with infoH tactical."
(cond
+ ;; We cannot rebuild the sub-patterns from the final goal, so ';' is not
+ ;; supported. Only single tactics like destruct.
((string-match ";" s) s) ;; composed tactic cannot be treated
((string-match coq-auto-as-hack-hyp-name-regex s)
(concat "infoH " (match-string 1 s) " (" (match-string 2 s) ")."))
@@ -2710,6 +2712,7 @@ Used for automatic insertion of \"Proof using\"
annotations.")
(interactive)
(save-excursion
(goto-char (proof-unprocessed-begin))
+ (forward-char 1)
(coq-find-real-start)
(let* ((pt (point))
(_ (coq-script-parse-cmdend-forward))
diff --git a/generic/proof-script.el b/generic/proof-script.el
index afa2e50b63..d62f2ea54c 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2901,7 +2901,7 @@ with something different."
(eq typ 'proverproc)
(eq typ 'proof)
(and proof-ignore-for-undo-count cmd
- (proof-string-match proof-ignore-for-undo-count cmd))))
+ (proof-stringfn-match proof-ignore-for-undo-count cmd))))
;; some named element: use generic forget-id function; finish.
((setq name (span-property span 'name))
(setq ans (format proof-forget-id-command name))
