branch: elpa/proof-general
commit dd9c8a2b6747acd6b774db63d02228bcfc3f740d
Merge: 084d783ff4 a967f22805
Author: Pierre Courtieu <pierre.court...@cnam.fr>
Commit: Pierre Courtieu <pierre.court...@cnam.fr>
Merge branch 'master' into fix-debug-mode
---
.github/workflows/test.yml | 108 ++---
CHANGES | 4 +
Makefile | 6 +-
ci/compile-tests/010-coqdep-errors/runtest.el | 10 +-
ci/compile-tests/011-current-buffer/Makefile | 36 ++
ci/compile-tests/011-current-buffer/a.v | 26 ++
ci/compile-tests/011-current-buffer/b.v | 15 +
ci/compile-tests/011-current-buffer/c.v | 25 ++
ci/compile-tests/011-current-buffer/d.v | 25 ++
ci/compile-tests/011-current-buffer/runtest.el | 266 ++++++++++++
ci/compile-tests/README.md | 3 +
ci/compile-tests/bin/coq-error | 11 +
ci/compile-tests/cct-lib.el | 2 +-
ci/coq-tests.el | 42 +-
ci/doc/README.md | 86 ++--
ci/doc/coq-emacs-releases.org | 121 +++---
ci/doc/currently-used-coq-emacs-versions | 35 +-
ci/doc/currently-used-coq-nix-versions | 4 +-
ci/simple-tests/coq-test-changes-in-comments.el | 518 ++++++++++++++++++++++++
ci/simple-tests/coq-test-goals-present.el | 2 +-
ci/simple-tests/coq-test-omit-proofs.el | 10 +-
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-abbrev.el | 4 +
coq/coq-db.el | 10 +-
coq/coq-indent.el | 7 +-
coq/coq-mode.el | 16 +-
coq/coq-par-compile.el | 348 ++++++++--------
coq/coq-smie.el | 35 +-
coq/coq-syntax.el | 1 +
coq/coq-system.el | 283 ++++++++-----
coq/coq.el | 14 +-
doc/ProofGeneral.texi | 38 +-
generic/proof-config.el | 2 +-
generic/proof-script.el | 2 +-
generic/proof-shell.el | 4 +-
38 files changed, 1727 insertions(+), 516 deletions(-)
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 3d0e4edaeb..b025c07bef 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -121,34 +121,36 @@ jobs:
- coq-8.15.2-emacs-29.4
- coq-8.16.1-emacs-28.2
- coq-8.16.1-emacs-29.4
- - coq-8.17.1-emacs-26.3
- - coq-8.17.1-emacs-27.1
- - coq-8.17.1-emacs-28.2
- coq-8.17.1-emacs-29.1
- coq-8.17.1-emacs-29.4
- coq-8.18.0-emacs-26.3
- coq-8.18.0-emacs-27.1
- coq-8.18.0-emacs-28.2
- - coq-8.18.0-emacs-29.1
+ - coq-8.18.0-emacs-29.3
- coq-8.18.0-emacs-29.4
- 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
- coq-8.19.2-emacs-28.2
- - coq-8.19.2-emacs-29.1
- - coq-8.19.2-emacs-29.2
- coq-8.19.2-emacs-29.3
- coq-8.19.2-emacs-29.4
- - coq-8.20-rc1-emacs-26.3
- - coq-8.20-rc1-emacs-27.1
- - coq-8.20-rc1-emacs-27.2
- - coq-8.20-rc1-emacs-28.1
- - coq-8.20-rc1-emacs-28.2
- - coq-8.20-rc1-emacs-29.1
- - coq-8.20-rc1-emacs-29.2
- - coq-8.20-rc1-emacs-29.3
- - coq-8.20-rc1-emacs-29.4
+ - 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
+ - coq-8.20.1-emacs-28.2
+ - 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
# CIPG change marker end
# don't cancel all in-progress jobs if one matrix job fails:
fail-fast: false
@@ -203,34 +205,36 @@ jobs:
- coq-8.15.2-emacs-29.4
- coq-8.16.1-emacs-28.2
- coq-8.16.1-emacs-29.4
- - coq-8.17.1-emacs-26.3
- - coq-8.17.1-emacs-27.1
- - coq-8.17.1-emacs-28.2
- coq-8.17.1-emacs-29.1
- coq-8.17.1-emacs-29.4
- coq-8.18.0-emacs-26.3
- coq-8.18.0-emacs-27.1
- coq-8.18.0-emacs-28.2
- - coq-8.18.0-emacs-29.1
+ - coq-8.18.0-emacs-29.3
- coq-8.18.0-emacs-29.4
- 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
- coq-8.19.2-emacs-28.2
- - coq-8.19.2-emacs-29.1
- - coq-8.19.2-emacs-29.2
- coq-8.19.2-emacs-29.3
- coq-8.19.2-emacs-29.4
- - coq-8.20-rc1-emacs-26.3
- - coq-8.20-rc1-emacs-27.1
- - coq-8.20-rc1-emacs-27.2
- - coq-8.20-rc1-emacs-28.1
- - coq-8.20-rc1-emacs-28.2
- - coq-8.20-rc1-emacs-29.1
- - coq-8.20-rc1-emacs-29.2
- - coq-8.20-rc1-emacs-29.3
- - coq-8.20-rc1-emacs-29.4
+ - 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
+ - coq-8.20.1-emacs-28.2
+ - 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
# CIPG change marker end
# don't cancel all in-progress jobs if one matrix job fails:
fail-fast: false
@@ -281,34 +285,36 @@ jobs:
- coq-8.15.2-emacs-29.4
- coq-8.16.1-emacs-28.2
- coq-8.16.1-emacs-29.4
- - coq-8.17.1-emacs-26.3
- - coq-8.17.1-emacs-27.1
- - coq-8.17.1-emacs-28.2
- coq-8.17.1-emacs-29.1
- coq-8.17.1-emacs-29.4
- coq-8.18.0-emacs-26.3
- coq-8.18.0-emacs-27.1
- coq-8.18.0-emacs-28.2
- - coq-8.18.0-emacs-29.1
+ - coq-8.18.0-emacs-29.3
- coq-8.18.0-emacs-29.4
- 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
- coq-8.19.2-emacs-28.2
- - coq-8.19.2-emacs-29.1
- - coq-8.19.2-emacs-29.2
- coq-8.19.2-emacs-29.3
- coq-8.19.2-emacs-29.4
- - coq-8.20-rc1-emacs-26.3
- - coq-8.20-rc1-emacs-27.1
- - coq-8.20-rc1-emacs-27.2
- - coq-8.20-rc1-emacs-28.1
- - coq-8.20-rc1-emacs-28.2
- - coq-8.20-rc1-emacs-29.1
- - coq-8.20-rc1-emacs-29.2
- - coq-8.20-rc1-emacs-29.3
- - coq-8.20-rc1-emacs-29.4
+ - 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
+ - coq-8.20.1-emacs-28.2
+ - 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
# CIPG change marker end
# don't cancel all in-progress jobs if one matrix job fails:
fail-fast: false
diff --git a/CHANGES b/CHANGES
index f277190604..8e77207399 100644
--- a/CHANGES
+++ b/CHANGES
@@ -40,6 +40,10 @@ the Git ChangeLog, the GitHub repo
https://github.com/ProofGeneral/PG
*** New command `proof-check-annotate' to annotate all failing proofs
with FAIL comments. Useful in the development process as described
above to ensure all currently failing proofs are marked as such.
+*** flag Printing Parentheses and Printing Notations can be set/unset
+ via menu and Coq keymap (C-c C-a C-9 and C-c C-a C-0 for
+ Parentheses (optimized for British and American keyboards); C-c
+ C-a n and C-c C-a N for Notations).
*** New options coq-compile-extra-coqc-arguments and
coq-compile-extra-coqdep-arguments to configure additional
command line arguments to calls of, respetively, coqc and coqdep
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/compile-tests/010-coqdep-errors/runtest.el
b/ci/compile-tests/010-coqdep-errors/runtest.el
index 73800a1b71..3e6f423b9d 100644
--- a/ci/compile-tests/010-coqdep-errors/runtest.el
+++ b/ci/compile-tests/010-coqdep-errors/runtest.el
@@ -33,6 +33,8 @@
;;; Define the tests
+(defvar cct-coqdep-error-prefix "^coqdep \\|^rocq dep ")
+
(ert-deftest cct-coqdep-fail-on-require ()
"coqdep error on missing library in a require command is detected."
;; (setq cct--debug-tests t)
@@ -47,7 +49,7 @@
(with-current-buffer coq--compile-response-buffer
;; (message "|%s|" (buffer-string))
(goto-char (1+ (length coq--compile-response-initial-content)))
- (setq coqdep-errror-in-response (looking-at "^coqdep "))
+ (setq coqdep-errror-in-response (looking-at cct-coqdep-error-prefix))
(setq missing-module-in-response (search-forward "X25XX" nil t)))
(with-current-buffer proof-shell-buffer
(goto-char (point-min))
@@ -78,7 +80,7 @@
(with-current-buffer coq--compile-response-buffer
;; (message "|%s|" (buffer-string))
(goto-char (1+ (length coq--compile-response-initial-content)))
- (setq coqdep-errror-in-response (looking-at "^coqdep "))
+ (setq coqdep-errror-in-response (looking-at cct-coqdep-error-prefix))
(setq syntax-error-in-response (search-forward "Syntax error" nil t)))
(with-current-buffer proof-shell-buffer
(goto-char (point-min))
@@ -90,6 +92,8 @@
(if coqdep-errror-in-response "DOES" "DOES NOT")
(if syntax-error-in-response "DOES" "DOES NOT")
(if dependency-in-coq "IS" "IS NOT"))
+ (message "coqdep-errror-in-response: %S" coqdep-errror-in-response)
+ (message "*** syntax-error-in-response: %S" syntax-error-in-response)
(should (and coqdep-errror-in-response
syntax-error-in-response
(not dependency-in-coq)))))
@@ -107,7 +111,7 @@
(with-current-buffer coq--compile-response-buffer
;; (message "|%s|" (buffer-string))
(goto-char (1+ (length coq--compile-response-initial-content)))
- (setq coqdep-errror-in-response (looking-at "^coqdep "))
+ (setq coqdep-errror-in-response (looking-at cct-coqdep-error-prefix))
(setq missing-module-in-response (search-forward "X25XX" nil t)))
(with-current-buffer proof-shell-buffer
(goto-char (point-min))
diff --git a/ci/compile-tests/011-current-buffer/Makefile
b/ci/compile-tests/011-current-buffer/Makefile
new file mode 100644
index 0000000000..6174b883cd
--- /dev/null
+++ b/ci/compile-tests/011-current-buffer/Makefile
@@ -0,0 +1,36 @@
+# This file is part of Proof General.
+#
+# © Copyright 2024 Hendrik Tews
+#
+# Authors: Hendrik Tews
+# Maintainer: Hendrik Tews <hend...@askra.de>
+#
+# SPDX-License-Identifier: GPL-3.0-or-later
+
+# This test uses ../bin/compile-test-start-delayed to start certain
+# commands with specified delays to check carfully constructed
+# internal states. compile-test-start-delayed outputs diagnostics on
+# file descriptor 9, which bypasses emacs and is joined with stderr of
+# the current make. Open file descriptor 9 here.
+#
+# To run not all tests, replace line
+#
+# -f ert-run-tests-batch-and-exit \
+#
+# with
+#
+# -eval '(ert-run-tests-batch-and-exit "pattern")' \
+#
+# where pattern should match the test names to run.
+
+.PHONY: test
+test:
+ $(MAKE) clean
+ emacs -batch -l ../../../generic/proof-site.el -l ../cct-lib.el \
+ -l runtest.el \
+ -f ert-run-tests-batch-and-exit \
+ 9>&1
+
+.PHONY: clean
+clean:
+ rm -f *.vo *.glob *.vio *.vos *.vok .*.aux
diff --git a/ci/compile-tests/011-current-buffer/a.v
b/ci/compile-tests/011-current-buffer/a.v
new file mode 100644
index 0000000000..0b35539fcd
--- /dev/null
+++ b/ci/compile-tests/011-current-buffer/a.v
@@ -0,0 +1,26 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2024 Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <hend...@askra.de>
+ *
+ * SPDX-License-Identifier: GPL-3.0-or-later
+ *
+ *
+ * This file is part of an automatic test case for parallel background
+ * compilation in coq-par-compile.el. See runtest.el in this directory.
+ *)
+
+(* The test script relies on absolute line numbers.
+ * DO NOT INSERT ANY LINE UNLESS YOU KNOW WHAT YOU ARE DOING.
+ *)
+
+(* The delay for coqdep is specified in comments with key coqdep-delay,
+ * see compile-test-start-delayed.
+ *)
+
+
+(* This is line 24 *)
+Require Export (* coqdep-delay 1 *) b.
+(* This is line 26 *)
diff --git a/ci/compile-tests/011-current-buffer/b.v
b/ci/compile-tests/011-current-buffer/b.v
new file mode 100644
index 0000000000..820e1449d2
--- /dev/null
+++ b/ci/compile-tests/011-current-buffer/b.v
@@ -0,0 +1,15 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2024 Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <hend...@askra.de>
+ *
+ * SPDX-License-Identifier: GPL-3.0-or-later
+ *
+ *
+ * This file is part of an automatic test case for parallel background
+ * compilation in coq-par-compile.el. See test.el in this directory.
+ *)
+
+Definition b : nat := 2.
diff --git a/ci/compile-tests/011-current-buffer/c.v
b/ci/compile-tests/011-current-buffer/c.v
new file mode 100644
index 0000000000..c29c827549
--- /dev/null
+++ b/ci/compile-tests/011-current-buffer/c.v
@@ -0,0 +1,25 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2024 Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <hend...@askra.de>
+ *
+ * SPDX-License-Identifier: GPL-3.0-or-later
+ *
+ *
+ * This file is part of an automatic test case for parallel background
+ * compilation in coq-par-compile.el. See test.el in this directory.
+ *)
+
+Definition c : nat := 2.
+
+(* Set `coq-compiler` and `coq-dependency-analyzer` as local variable
+ to something that definitely fails when the test (or the user)
+ visits this file in an ongoing background compilation and
+ background compilation picks up local variables from this file.
+ *)
+
+(*** Local Variables: ***)
+(*** coq-compiler: "coq-error" ***)
+(*** End: ***)
diff --git a/ci/compile-tests/011-current-buffer/d.v
b/ci/compile-tests/011-current-buffer/d.v
new file mode 100644
index 0000000000..2dffd4574d
--- /dev/null
+++ b/ci/compile-tests/011-current-buffer/d.v
@@ -0,0 +1,25 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2024 Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <hend...@askra.de>
+ *
+ * SPDX-License-Identifier: GPL-3.0-or-later
+ *
+ *
+ * This file is part of an automatic test case for parallel background
+ * compilation in coq-par-compile.el. See test.el in this directory.
+ *)
+
+Definition c : nat := 2.
+
+(* Set `coq-compiler` and `coq-dependency-analyzer` as local variable
+ to something that definitely fails when the test (or the user)
+ visits this file in an ongoing background compilation and
+ background compilation picks up local variables from this file.
+ *)
+
+(*** Local Variables: ***)
+(*** coq-dependency-analyzer: "coq-error" ***)
+(*** End: ***)
diff --git a/ci/compile-tests/011-current-buffer/runtest.el
b/ci/compile-tests/011-current-buffer/runtest.el
new file mode 100644
index 0000000000..0e72250099
--- /dev/null
+++ b/ci/compile-tests/011-current-buffer/runtest.el
@@ -0,0 +1,266 @@
+;; This file is part of Proof General. -*- lexical-binding: t; -*-
+;;
+;; © Copyright 2024 Hendrik Tews
+;;
+;; Authors: Hendrik Tews
+;; Maintainer: Hendrik Tews <hend...@askra.de>
+;;
+;; SPDX-License-Identifier: GPL-3.0-or-later
+
+;;; Commentary:
+;;
+;; Coq Compile Tests (cct) --
+;; ert tests for parallel background compilation for Coq
+;;
+;; Test that parallel background compilation is not confused by local
+;; variables in unrelated buffers.
+;;
+;; The dependencies in this test are:
+;;
+;; a c d
+;; |
+;; b
+;;
+;; Files c and d are completely independent of file a and file b and
+;; not processed by Coq. The idea is that files c or d come from a
+;; different project that uses a different `coq-compiler' or
+;; `coq-dependency-analyzer', see also PG issue #797. These different
+;; local settings should not confuse the ongoing background
+;; compilation of file b for processing file a in a script buffer.
+;; File c sets `coq-compiler' as local variable and file d sets
+;; `coq-dependency-analyzer' as local variable.
+
+
+;; require cct-lib for the elisp compilation, otherwise this is present already
+(require 'cct-lib "ci/compile-tests/cct-lib")
+
+;;; set configuration
+(cct-configure-proof-general)
+(configure-delayed-coq)
+
+(defvar switch-buffer-while-waiting nil
+ "Switch buffer in busy waiting hooks when t.
+Whether the hook functions `switch-to-other-buffer-while-waiting'
+and `switch-back-after-waiting' switch to some other buffer or
+not is controled by this variable. If t, switch to the buffer in
+`cdv-buffer' before starting busy waiting and switch back to the
+buffer in `av-buffer' after busy waiting.")
+
+(defvar av-buffer nil
+ "Buffer to switch back after busy waiting.
+See `switch-buffer-while-waiting'.")
+
+(defvar cdv-buffer nil
+ "Buffer to switch to before busy waiting.
+See `switch-buffer-while-waiting'.")
+
+(defun switch-to-other-buffer-while-waiting ()
+ "Hook to switch current buffer before busy waiting.
+Hook function for `cct-before-busy-waiting-hook'. Switches to
+`cdv-buffer' if `switch-buffer-while-waiting' is t."
+ (when (and switch-buffer-while-waiting cdv-buffer)
+ (message "Switch to buffer c.v while busy waiting")
+ (set-buffer cdv-buffer)))
+
+(defun switch-back-after-waiting ()
+ "Hook to switch current buffer back after busy waiting.
+Hook function for `cct-after-busy-waiting-hook'. Switches back to
+`av-buffer' if `switch-buffer-while-waiting' is t."
+ (when (and switch-buffer-while-waiting av-buffer)
+ (message "Switch back to buffer a.v after busy waiting")
+ (set-buffer av-buffer)))
+
+(add-hook 'cct-before-busy-waiting-hook #'switch-to-other-buffer-while-waiting)
+(add-hook 'cct-after-busy-waiting-hook #'switch-back-after-waiting)
+
+
+;;; The tests itself
+
+(ert-deftest test-current-buffer-vok ()
+ "Check that second stage compilation uses the right local variables.
+Second stage compilation (vok and vio2vo) should use the local
+variables from the original scripting buffer, see also PG issue
+#797."
+ (unwind-protect
+ (progn
+ (message "\nRun test-current-buffer-vok")
+
+ ;; configure 2nd stage
+ (if (coq--post-v811)
+ (setq coq-compile-vos 'vos-and-vok)
+ (setq coq-compile-quick 'quick-and-vio2vo))
+
+ ;; (setq cct--debug-tests t)
+ ;; (setq coq--debug-auto-compilation t)
+ (find-file "a.v")
+ (setq av-buffer (current-buffer))
+
+ (find-file "c.v")
+ (setq cdv-buffer (current-buffer))
+ (set-buffer av-buffer)
+
+ (message (concat "Settings in a.v:\n"
+ " coqdep: %s\n coqc: %s\n PATH %s\n"
+ " exec-path: %s\n detected coq version: %s")
+ coq-dependency-analyzer
+ coq-compiler
+ (getenv "PATH")
+ exec-path
+ coq-autodetected-version)
+
+ ;; Work around existing .vos and .vok files from other tests in
+ ;; this file.
+ (message "\ntouch dependency b.v to force complete (re-)compilation")
+ (should (set-file-times "b.v"))
+
+ (message "\nProcess a.v to end, including compilation of dependency
b.v")
+ (cct-process-to-line 27)
+ (cct-check-locked 26 'locked)
+
+ (with-current-buffer cdv-buffer
+ (message
+ (concat "\nWait for 2nd stage (vok/vio2vo) compilation "
+ "in buffer b.v with"
+ "\n coqdep: %s\n coqc: %s")
+ coq-dependency-analyzer
+ coq-compiler))
+
+ (setq switch-buffer-while-waiting t)
+
+ ;; This will temporarily switch to buffer c.v, which sets
+ ;; coq-compiler as local variable, see the hooks above
+ (cct-wait-for-second-stage)
+
+ (message "search for coq-error error message in compile-response
buffer")
+ (with-current-buffer coq--compile-response-buffer
+ (goto-char (point-min))
+ (should
+ (not
+ (re-search-forward "Error: coq-error has been executed" nil t)))))
+
+ ;; clean up
+ (dolist (buf (list av-buffer cdv-buffer))
+ (when buf
+ (with-current-buffer buf
+ (set-buffer-modified-p nil))
+ (kill-buffer buf)))
+ (setq switch-buffer-while-waiting nil)))
+
+(ert-deftest test-current-buffer-coqdep ()
+ "Check that dependency analysis uses the right local variables.
+Dependency analysis during parallel background compilation (i.e.,
+runing `coqdep` on dependencies) should use the local variables
+from the original scripting buffer, see also PG issue #797."
+ (unwind-protect
+ (progn
+ (message "\nRun test-current-buffer-coqdep")
+
+ ;; (setq cct--debug-tests t)
+ ;; (setq coq--debug-auto-compilation t)
+ (find-file "a.v")
+ (setq av-buffer (current-buffer))
+
+ (find-file "d.v")
+ (setq cdv-buffer (current-buffer))
+ (set-buffer av-buffer)
+
+ (message (concat "Settings in a.v:\n"
+ " coqdep: %s\n coqc: %s\n PATH %s\n"
+ " exec-path: %s\n detected coq version: %s")
+ coq-dependency-analyzer
+ coq-compiler
+ (getenv "PATH")
+ exec-path
+ coq-autodetected-version)
+
+ (with-current-buffer cdv-buffer
+ (message
+ (concat "\nProcess a.v to end while visiting d.v with"
+ "\n coqdep: %s\n coqc: %s")
+ coq-dependency-analyzer
+ coq-compiler))
+
+ (setq switch-buffer-while-waiting t)
+
+ ;; This will temporarily switch to buffer c.v, which sets
+ ;; coq-compiler as local variable, see the hooks above.
+ (cct-process-to-line 27)
+
+ ;; (with-current-buffer coq--compile-response-buffer
+ ;; (message "coq-compile-response:\n%s\n<<<End"
+ ;; (buffer-substring-no-properties (point-min)
(point-max))))
+
+ (cct-check-locked 26 'locked))
+
+ ;; clean up
+ (dolist (buf (list av-buffer cdv-buffer))
+ (when buf
+ (with-current-buffer buf
+ (set-buffer-modified-p nil))
+ (kill-buffer buf)))
+ (setq switch-buffer-while-waiting nil)))
+
+(ert-deftest test-current-buffer-coqc ()
+ "Check that compilation of dependencies uses the right local variables.
+Compilation of dependencies during parallel background
+compilation (i.e., runing `coqc` on dependencies) should use the
+local variables from the original scripting buffer, see also PG
+issue #797.
+
+To ensure we only see errors from running `coqc`, we temporarily
+switch to buffer c.v, which sets `coq-compiler' but leaves
+`coq-dependency-analyzer' alone."
+ (unwind-protect
+ (progn
+ (message "\nRun test-current-buffer-coqc")
+
+ ;; (setq cct--debug-tests t)
+ ;; (setq coq--debug-auto-compilation t)
+ (find-file "a.v")
+ (setq av-buffer (current-buffer))
+
+ (find-file "c.v")
+ (setq cdv-buffer (current-buffer))
+ (set-buffer av-buffer)
+
+ (message (concat "Settings in a.v:\n"
+ " coqdep: %s\n coqc: %s\n PATH %s\n"
+ " exec-path: %s\n detected coq version: %s")
+ coq-dependency-analyzer
+ coq-compiler
+ (getenv "PATH")
+ exec-path
+ coq-autodetected-version)
+
+ (with-current-buffer cdv-buffer
+ (message (concat "\nProcess a.v to end, "
+ "including compilation of dependency b.v\n"
+ " while temporarily visiting c.v with\n"
+ " coqdep: %s\n coqc: %s")
+ coq-dependency-analyzer
+ coq-compiler))
+
+ ;; Work around existing .vos and .vok files from other tests in
+ ;; this file.
+ (message "\ntouch dependency b.v to force complete (re-)compilation")
+ (should (set-file-times "b.v"))
+
+ (setq switch-buffer-while-waiting t)
+
+ ;; This will temporarily switch to buffer c.v, which sets
+ ;; coq-compiler as local variable, see the hooks above.
+ (cct-process-to-line 27)
+
+ ;; (with-current-buffer coq--compile-response-buffer
+ ;; (message "coq-compile-response:\n%s\n<<<End"
+ ;; (buffer-substring-no-properties (point-min)
(point-max))))
+
+ (cct-check-locked 26 'locked))
+
+ ;; clean up
+ (dolist (buf (list av-buffer cdv-buffer))
+ (when buf
+ (with-current-buffer buf
+ (set-buffer-modified-p nil))
+ (kill-buffer buf)))
+ (setq switch-buffer-while-waiting nil)))
diff --git a/ci/compile-tests/README.md b/ci/compile-tests/README.md
index 2e578c97d4..fe2ee2156b 100644
--- a/ci/compile-tests/README.md
+++ b/ci/compile-tests/README.md
@@ -39,6 +39,9 @@ All tests are for parallel background compilation.
dependee is still processing
010-coqdep-errors
: check that coqdep errors are reliably detected
+011-current-buffer
+: check that background compilation is not confused by local variables
+ in unrelated buffers
# Tests currently missing
diff --git a/ci/compile-tests/bin/coq-error b/ci/compile-tests/bin/coq-error
new file mode 100755
index 0000000000..2d75f8cabc
--- /dev/null
+++ b/ci/compile-tests/bin/coq-error
@@ -0,0 +1,11 @@
+#!/bin/bash
+
+# The purpose of this script is to always fail with a recognizable
+# error message. This is used in test ../011-current-buffer to check
+# that background compilation does not pick wrong values for
+# `coq-compiler' and `coq-dependency-analyzer' from local variables of
+# arbitrary files.
+
+echo "Error: coq-error has been executed" > /dev/stderr
+
+exit 1
diff --git a/ci/compile-tests/cct-lib.el b/ci/compile-tests/cct-lib.el
index 7a5a427c9a..76e9b25527 100644
--- a/ci/compile-tests/cct-lib.el
+++ b/ci/compile-tests/cct-lib.el
@@ -116,7 +116,7 @@ backward. Replace the word there with WORD."
(insert word))
(defun cct-process-to-line (line)
- "Assert/retract to line LINE and wait until processing completed.
+ "Assert/retract to start of line LINE and wait until processing completed.
Runs `cct-before-busy-waiting-hook' and
`cct-after-busy-waiting-hook' before and after busy waiting for
the prover. In many tests these hooks are not used."
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 eaa6c000da..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,28 +169,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 -->
-65
+66
<!-- 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.1 | 26.2 | 26.3 | 27.1 | 27.2 | 28.1 | 28.2 | 29.1 | 29.2 |
29.3 | 29.4 |
-|---------+------+------+------+------+------+------+------+------+------+------+------|
-| 8.8.2 | H | | | | | | | | |
| |
-| 8.9.1 | | H | | | | | | | |
| |
-| 8.10.2 | | | H | | | | | | |
| |
-| 8.11.2 | | | SUP | | | | | | |
| N |
-| 8.12.2 | | | SUP | SUP | | | | | |
| N |
-| 8.13.2 | | | SUP | SUP | H | | | | |
| N |
-| 8.14.1 | | | SUP | SUP | H | | | | |
| N |
-| 8.15.2 | | | SUP | SUP | | H | | | |
| N |
-| 8.16.1 | | | X | X | X | X | X | X | X | X
| X |
-| 8.17.1 | | | X | X | X | X | X | X | X | X
| X |
-| 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.20rc | | | RC | RC | RC | RC | RC | RC | RC |
RC | RC |
+| | 26.2 | 26.3 | 27.1 | 27.2 | 28.1 | 28.2 | 29.1 | 29.2 | 29.3 |
29.4 |
+|---------+------+------+------+------+------+------+------+------+------+------|
+| 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
|
+| 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,
@@ -275,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.
@@ -286,28 +288,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 -->
-41
+43
<!-- 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.1 | 26.2 | 26.3 | 27.1 | 27.2 | 28.1 | 28.2 | 29.1 | 29.2 |
29.3 | 29.4 |
-|---------+------+------+------+------+------+------+------+------+------+------+------|
-| 8.8.2 | | | | | | | | | |
| |
-| 8.9.1 | | | | | | | | | |
| |
-| 8.10.2 | | | | | | | | | |
| |
-| 8.11.2 | | | SUP | | | | | | |
| N |
-| 8.12.2 | | | | SUP | | | | | |
| 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 | | | X | X | | | X | X | |
| N |
-| 8.18.0 | | | X | X | | | X | X | |
| N |
-| 8.19.2 | | | X | X | N | N | X | X | N | N
| N |
-| 8.20rc | | | RC | RC | RC | RC | RC | RC | RC |
RC | RC |
+| | 26.2 | 26.3 | 27.1 | 27.2 | 28.1 | 28.2 | 29.1 | 29.2 | 29.3 |
29.4 |
+|---------+------+------+------+------+------+------+------+------+------+------|
+| 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 | | 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
@@ -317,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 -->
-152
+158
<!-- CIPG change marker end -->
github checks.
@@ -376,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
@@ -410,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 e313bb8b28..67e86a6fbc 100644
--- a/ci/doc/coq-emacs-releases.org
+++ b/ci/doc/coq-emacs-releases.org
@@ -11,62 +11,65 @@
automatically, therefore please observe the requirements in Section
"Release table" in file README.md!
-| date | coq | emacs | distribution name | EOL | historic |
-|---------+--------+-------+-------------------+----------+----------|
-| 2024/06 | 8.20rc | | | | |
-| 2024/06 | 8.19.2 | 29.4 | | | |
-| 2024/03 | 8.19.1 | 29.3 | | | |
-| 2024/01 | 8.19.0 | 29.2 | | | |
-| 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/07? | |
-| 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 96a336895d..2c7a467b6d 100644
--- a/ci/doc/currently-used-coq-emacs-versions
+++ b/ci/doc/currently-used-coq-emacs-versions
@@ -1,4 +1,3 @@
-coq-8.8.2-emacs-26.1
coq-8.9.1-emacs-26.2
coq-8.10.2-emacs-26.3
coq-8.11.2-emacs-26.3
@@ -7,11 +6,9 @@ coq-8.12.2-emacs-26.3
coq-8.12.2-emacs-27.1
coq-8.12.2-emacs-29.4
coq-8.13.2-emacs-26.3
-coq-8.13.2-emacs-27.1
coq-8.13.2-emacs-27.2
coq-8.13.2-emacs-29.4
coq-8.14.1-emacs-26.3
-coq-8.14.1-emacs-27.1
coq-8.14.1-emacs-27.2
coq-8.14.1-emacs-29.4
coq-8.15.2-emacs-26.3
@@ -20,12 +17,7 @@ coq-8.15.2-emacs-28.1
coq-8.15.2-emacs-29.4
coq-8.16.1-emacs-26.3
coq-8.16.1-emacs-27.1
-coq-8.16.1-emacs-27.2
-coq-8.16.1-emacs-28.1
coq-8.16.1-emacs-28.2
-coq-8.16.1-emacs-29.1
-coq-8.16.1-emacs-29.2
-coq-8.16.1-emacs-29.3
coq-8.16.1-emacs-29.4
coq-8.17.1-emacs-26.3
coq-8.17.1-emacs-27.1
@@ -54,12 +46,21 @@ coq-8.19.2-emacs-29.1
coq-8.19.2-emacs-29.2
coq-8.19.2-emacs-29.3
coq-8.19.2-emacs-29.4
-coq-8.20-rc1-emacs-26.3
-coq-8.20-rc1-emacs-27.1
-coq-8.20-rc1-emacs-27.2
-coq-8.20-rc1-emacs-28.1
-coq-8.20-rc1-emacs-28.2
-coq-8.20-rc1-emacs-29.1
-coq-8.20-rc1-emacs-29.2
-coq-8.20-rc1-emacs-29.3
-coq-8.20-rc1-emacs-29.4
+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
+coq-8.20.1-emacs-28.2
+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 125c320e9b..fad04ae37c 100644
--- a/ci/doc/currently-used-coq-nix-versions
+++ b/ci/doc/currently-used-coq-nix-versions
@@ -1,4 +1,3 @@
-8.8.2
8.9.1
8.10.2
8.11.2
@@ -10,4 +9,5 @@
8.17.1
8.18.0
8.19.2
-8.20rc
+8.20.1
+9.0-rc1
diff --git a/ci/simple-tests/coq-test-changes-in-comments.el
b/ci/simple-tests/coq-test-changes-in-comments.el
new file mode 100644
index 0000000000..aa093b3242
--- /dev/null
+++ b/ci/simple-tests/coq-test-changes-in-comments.el
@@ -0,0 +1,518 @@
+;; This file is part of Proof General.
+;;
+;; © Copyright 2025 Hendrik Tews
+;;
+;; Authors: Hendrik Tews
+;; Maintainer: Hendrik Tews <hend...@askra.de>
+;;
+;; License: GPL (GNU GENERAL PUBLIC LICENSE)
+
+;;; Commentary:
+;;
+;; Test that for various changes inside comments and spanning from one
+;; to the next comment the buffer is correctly retracted.
+
+
+;;; Coq source code for tests
+
+(defconst coq-src-comment
+ "(*
+ Comment 1
+ *)
+
+Definition aXXa := 1.
+
+(*
+ Comment 2
+
+ *)
+
+Definition bXXb := 2.
+"
+ "Coq source code for comment tests.")
+
+
+;;; utility functions
+
+(defun test-goto-line (line)
+ "Put point on start of line LINE.
+Very similar to `goto-line', but the documentation of `goto-line'
+says, programs should use this piece of code."
+ (goto-char (point-min))
+ (forward-line (1- line))
+ (cl-assert (eq (line-number-at-pos) line) nil
+ "point not at required line in test-goto-line"))
+
+(defun record-buffer-content (buf)
+ "Record buffer content of BUF via `message' for debugging.
+BUF should be a buffer as string or buffer object."
+ (with-current-buffer buf
+ (let ((content (buffer-substring-no-properties (point-min) (point-max))))
+ (message "%s buffer contains %d chars: %s" buf (length content)
content))))
+
+(defun wait-for-coq ()
+ "Wait until processing is complete."
+ (while (or proof-second-action-list-active
+ (consp proof-action-list))
+ ;; (message "wait for coq/compilation with %d items queued\n"
+ ;; (length proof-action-list))
+ ;;
+ ;; accept-process-output without timeout returns rather quickly,
+ ;; apparently most times without process output or any other event
+ ;; to process.
+ (accept-process-output nil 0.1)))
+
+(defun point-should-be-unlocked ()
+ "Check that point is unlocked.
+This is a simplified version of `cct-check-locked' that only
+works correctly when the `proof-locked-span' does exist in the
+current buffer."
+ (should (and proof-locked-span
+ (span-end proof-locked-span)
+ (< (span-end proof-locked-span) (point)))))
+
+
+;;; define the tests
+
+(ert-deftest insert-only-comment-end-in-processed-comment ()
+ :expected-result :failed
+ "Test inserting a comment end marker inside a processed comment."
+ (message "Check retract after inserting `*)' in a processed comment")
+
+ ;; Before Emacs 27 `self-insert-command' is lacking the optional
+ ;; character argument, making it too complicated to simulate typing.
+ ;; When done manually, this test also fails in Emacs 26.3.
+ (skip-unless (version<= "27" emacs-version))
+
+ (let (buffer)
+ (unwind-protect
+ (progn
+ (find-file "comments.v")
+ (setq buffer (current-buffer))
+ (insert coq-src-comment)
+
+ ;; process
+ (goto-char (point-max))
+ (proof-goto-point)
+ (wait-for-coq)
+
+ ;; check that Definition bXXb has been processed
+ ;; (record-buffer-content "*coq*")
+ (with-current-buffer proof-shell-buffer
+ (goto-char (point-max))
+ (should (search-backward "Definition bXXb" nil t)))
+
+ ;; insert comment end via keyboard simulation
+ (test-goto-line 9)
+ (self-insert-command 1 ?*)
+ (self-insert-command 1 41) ; ?) is 41, but ?) distorts indentation
+
+ ;; check that point is not in locked region
+ (forward-line 1)
+ ;; (record-buffer-content (current-buffer))
+ (point-should-be-unlocked))
+
+ ;; clean up
+ (when buffer
+ (with-current-buffer buffer
+ (set-buffer-modified-p nil))
+ (kill-buffer buffer)))))
+
+(ert-deftest insert-comment-end-and-char-in-processed-comment ()
+ "Insert a comment end marker and something else inside a processed comment."
+ (message "Check retract after inserting `*)a' in a processed comment")
+
+ ;; Before Emacs 27 `self-insert-command' is lacking the optional
+ ;; character argument, making it too complicated to simulate typing.
+ ;; When done manually, this test also succeeds in Emacs 26.3.
+ (skip-unless (version<= "27" emacs-version))
+
+ (let (buffer)
+ (unwind-protect
+ (progn
+ (find-file "comments.v")
+ (setq buffer (current-buffer))
+ (insert coq-src-comment)
+
+ ;; process
+ (goto-char (point-max))
+ (proof-goto-point)
+ (wait-for-coq)
+
+ ;; check that Definition bXXb has been processed
+ ;; (record-buffer-content "*coq*")
+ (with-current-buffer proof-shell-buffer
+ (goto-char (point-max))
+ (should (search-backward "Definition bXXb" nil t)))
+
+ ;; insert comment end via keyboard simulation
+ (test-goto-line 9)
+ (self-insert-command 1 ?*)
+ (self-insert-command 1 41) ; ?) is 41, but ?) distorts indentation
+ (self-insert-command 1 ?a)
+
+ ;; check that point is not in locked region
+ (forward-line 1)
+ ;; (record-buffer-content (current-buffer))
+ ;; (message "locked until %s, point at %s"
+ ;; (span-end proof-locked-span) (point))
+ (point-should-be-unlocked))
+
+ ;; clean up
+ (when buffer
+ (with-current-buffer buffer
+ (set-buffer-modified-p nil))
+ (kill-buffer buffer)))))
+
+(ert-deftest comment-definition-process-undo ()
+ :expected-result (if (version<= "27" emacs-version) :failed :passed)
+ "Comment a definition with `comment-dwim', process and then undo.
+Reproduces issue #800. The undo should cause a retract."
+ (message "Check undo of a comment region in a processed region")
+ (let (buffer
+ (saved-comment-style comment-style))
+ (unwind-protect
+ (progn
+ (find-file "comments.v")
+ (setq buffer (current-buffer))
+ (setq comment-style 'extra-line)
+ (transient-mark-mode 1)
+
+ ;; Insert `coq-src-comment' with many undo boundaries in
+ ;; between. If there are too few undo boundaries (or none)
+ ;; issue #800 cannot be reproduced.
+ (mapc
+ (lambda (s)
+ (insert s)
+ (insert "\n")
+ (undo-boundary))
+ (split-string coq-src-comment "\n"))
+
+ ;; Comment definition aXXa
+ (goto-char (point-min))
+ (should (search-forward "Definition aXXa" nil t))
+ (beginning-of-line)
+ (set-mark (point))
+ (end-of-line)
+ (comment-dwim nil)
+ (undo-boundary)
+ ;; (record-buffer-content (current-buffer))
+
+ ;; The mark seems to stay active - without deactivating it,
+ ;; the undo won't clear the comment.
+ (deactivate-mark t)
+
+ ;; process
+ (goto-char (point-max))
+ (proof-goto-point)
+ (wait-for-coq)
+ ;; (record-buffer-content (current-buffer))
+ ;; (message "locked until %s, point at %s"
+ ;; (span-end proof-locked-span) (point))
+
+ ;; check that Definition bXXb has been processed
+ ;; (record-buffer-content "*coq*")
+ (with-current-buffer proof-shell-buffer
+ (goto-char (point-max))
+ (should (search-backward "Definition bXXb" nil t)))
+
+ ;; undo
+ (pg-protected-undo nil)
+
+ ;; Definition aXXa should not be locked
+ (goto-char (point-min))
+ (should (search-forward "Definition aXXa" nil t))
+ (beginning-of-line)
+ (should (looking-at "Definition"))
+ ;; (record-buffer-content (current-buffer))
+ ;; (message "locked until %s, point at %s"
+ ;; (span-end proof-locked-span) (point))
+ (point-should-be-unlocked))
+
+ ;; clean up
+ (when buffer
+ (with-current-buffer buffer
+ (set-buffer-modified-p nil)
+ (setq comment-style saved-comment-style))
+ (kill-buffer buffer)))))
+
+(ert-deftest yank-comment-end-in-processed-comment ()
+ :expected-result :failed
+ "Insert a comment end marker inside a processed comment via yank."
+ (message "Check retract after yanking `*) XXX (*' in a processed comment")
+ (let (buffer)
+ (unwind-protect
+ (progn
+ (find-file "comments.v")
+ (setq buffer (current-buffer))
+ (insert coq-src-comment)
+
+ ;; process
+ (goto-char (point-max))
+ (proof-goto-point)
+ (wait-for-coq)
+
+ ;; check that Definition bXXb has been processed
+ ;; (record-buffer-content "*coq*")
+ (with-current-buffer proof-shell-buffer
+ (goto-char (point-max))
+ (should (search-backward "Definition bXXb" nil t)))
+
+ ;; insert comment end via keyboard simulation
+ (test-goto-line 9)
+ ;; fake some kill
+ (kill-new "*) XXX (*")
+ (yank)
+
+ ;; check that point is not in locked region
+ (forward-line 1)
+ ;; (record-buffer-content (current-buffer))
+ ;; (message "locked until %s, point at %s"
+ ;; (span-end proof-locked-span) (point))
+ (point-should-be-unlocked))
+
+ ;; clean up
+ (when buffer
+ (with-current-buffer buffer
+ (set-buffer-modified-p nil))
+ (kill-buffer buffer)))))
+
+(ert-deftest kill-from-comment-to-next-comment ()
+ :expected-result :failed
+ "Kill from comment to comment, including some non-commented material."
+ (message "Kill from comment to next comment")
+ (let (buffer start end)
+ (unwind-protect
+ (progn
+ (find-file "comments.v")
+ (setq buffer (current-buffer))
+ (insert coq-src-comment)
+
+ ;; process
+ (goto-char (point-max))
+ (proof-goto-point)
+ (wait-for-coq)
+
+ ;; check that Definition bXXb has been processed
+ ;; (record-buffer-content "*coq*")
+ (with-current-buffer proof-shell-buffer
+ (goto-char (point-max))
+ (should (search-backward "Definition bXXb" nil t)))
+
+ ;; Kill from comment one over aXXa to comment 2
+ (goto-char (point-min))
+ (should (search-forward "Comment 1" nil t))
+ (forward-line 1)
+ (setq start (point))
+ (should (search-forward "Comment 2" nil t))
+ (forward-line 1)
+ (setq end (point))
+ (kill-region start end)
+
+ ;; check that point is not in locked region
+ (forward-line 1)
+ ;; (record-buffer-content (current-buffer))
+ ;; (message "locked until %s, point at %s"
+ ;; (span-end proof-locked-span) (point))
+ (point-should-be-unlocked))
+
+ ;; clean up
+ (when buffer
+ (with-current-buffer buffer
+ (set-buffer-modified-p nil))
+ (kill-buffer buffer)))))
+
+(ert-deftest undo-breaks-up-nested-comment ()
+ :expected-result :failed
+ "Undo start and end of two nested comments to break up comment.
+Insert a comment start marker inside first comment and a comment
+end marker in second comment, such that there is one comment
+covering the definition of aXXa with two nested comments. Then,
+after processing, undo twice such that aXXa is outside any
+comment."
+ (message "Undo twice to break up comment with nested comments")
+ (let (buffer)
+ (unwind-protect
+ (progn
+ (find-file "comments.v")
+ (setq buffer (current-buffer))
+ (insert coq-src-comment)
+ (undo-boundary)
+
+ ;; insert comment start in first comment
+ (goto-char (point-min))
+ (should (search-forward "Comment 1" nil t))
+ (forward-line 1)
+ (insert "(* ")
+ (undo-boundary)
+
+ ;; insert comment end in second comment
+ (should (search-forward "Comment 2" nil t))
+ (forward-line -1)
+ (end-of-line)
+ (insert " *)")
+ (undo-boundary)
+
+ ;; process
+ (goto-char (point-max))
+ (proof-goto-point)
+ (wait-for-coq)
+ ;; (record-buffer-content (current-buffer))
+ ;; (message "locked until %s, point at %s"
+ ;; (span-end proof-locked-span) (point))
+
+ ;; check that Definition bXXb has been processed
+ ;; (record-buffer-content "*coq*")
+ (with-current-buffer proof-shell-buffer
+ (goto-char (point-max))
+ (should (search-backward "Definition bXXb" nil t)))
+
+ ;; undo twice
+ (pg-protected-undo nil)
+ (pg-protected-undo nil)
+
+ ;; check that bXXb is not in locked region
+ (should (search-backward "Definition aXXa" nil t))
+ (beginning-of-line)
+ ;; (record-buffer-content (current-buffer))
+ ;; (message "locked until %s, point at %s"
+ ;; (span-end proof-locked-span) (point))
+ (point-should-be-unlocked))
+
+ ;; clean up
+ (when buffer
+ (with-current-buffer buffer
+ (set-buffer-modified-p nil))
+ (kill-buffer buffer)))))
+
+(ert-deftest undo-comment-spanning-over-two-comments ()
+ :expected-result :failed
+ "Undo a comment such that some outer comment is broken up.
+Insert a new comment starting inside comment 1 and ending inside
+comment 2 such that the definition aXXa is inside a comment. Then
+process and undo. Requires `comment-style' to be set."
+ (message "Undo a comment such that some outer comment is broken up")
+ (let (buffer
+ (saved-comment-style comment-style))
+ (unwind-protect
+ (progn
+ (find-file "comments.v")
+ (setq buffer (current-buffer))
+ (setq comment-style 'extra-line)
+ (transient-mark-mode 1)
+
+ ;; Insert `coq-src-comment' with many undo boundaries in
+ ;; between.
+ (mapc
+ (lambda (s)
+ (insert s)
+ (insert "\n")
+ (undo-boundary))
+ (split-string coq-src-comment "\n"))
+
+ ;; insert a new comment from comment 1 to comment 2
+ (goto-char (point-min))
+ (should (search-forward "Comment 1" nil t))
+ (forward-line 1)
+ (set-mark (point))
+ (should (search-forward "Comment 2" nil t))
+ (forward-line 1)
+ (comment-dwim nil)
+ (undo-boundary)
+ (deactivate-mark t)
+
+ ;; delete last empty line
+ (goto-char (point-max))
+ (backward-delete-char 1)
+
+ ;; process
+ (proof-goto-point)
+ (wait-for-coq)
+ ;; (record-buffer-content (current-buffer))
+ ;; (message "locked until %s, point at %s"
+ ;; (span-end proof-locked-span) (point))
+
+ ;; check that Definition bXXb has been processed
+ ;; (record-buffer-content "*coq*")
+ (with-current-buffer proof-shell-buffer
+ (goto-char (point-max))
+ (should (search-backward "Definition bXXb" nil t)))
+
+ ;; undo twice
+ (pg-protected-undo nil)
+ (pg-protected-undo nil)
+
+ ;; check that bXXb is not in locked region
+ (should (search-backward "Definition aXXa" nil t))
+ (beginning-of-line)
+ ;; (record-buffer-content (current-buffer))
+ ;; (message "locked until %s, point at %s"
+ ;; (span-end proof-locked-span) (point))
+ (point-should-be-unlocked))
+
+ ;; clean up
+ (when buffer
+ (with-current-buffer buffer
+ (set-buffer-modified-p nil)
+ (setq comment-style saved-comment-style))
+ (kill-buffer buffer)))))
+
+(ert-deftest undo-kill-from-comment-to-comment ()
+ :expected-result :failed
+ "Kill from comment to next comment, including other material, then undo.
+Kill from inside comment 1 to inside comment 2 such that the
+definition aXXa is gone. Then process and undo. Requires
+`comment-style' to be set."
+ (message "Kill from comment to next comment, including material in between")
+ (let (buffer start
+ (saved-comment-style comment-style))
+ (unwind-protect
+ (progn
+ (find-file "comments.v")
+ (setq buffer (current-buffer))
+ (setq comment-style 'extra-line)
+ (transient-mark-mode 1)
+ (insert coq-src-comment)
+ (undo-boundary)
+
+ ;; kill from comment 1 to comment 2
+ (goto-char (point-min))
+ (should (search-forward "Comment 1" nil t))
+ (forward-line 1)
+ (setq start (point))
+ (should (search-forward "Comment 2" nil t))
+ (beginning-of-line)
+ (kill-region start (point))
+ (undo-boundary)
+
+ ;; process
+ (goto-char (point-max))
+ (proof-goto-point)
+ (wait-for-coq)
+ ;; (record-buffer-content (current-buffer))
+ ;; (message "locked until %s, point at %s"
+ ;; (span-end proof-locked-span) (point))
+
+ ;; check that Definition bXXb has been processed
+ ;; (record-buffer-content "*coq*")
+ (with-current-buffer proof-shell-buffer
+ (goto-char (point-max))
+ (should (search-backward "Definition bXXb" nil t)))
+
+ ;; undo kill-region
+ (pg-protected-undo nil)
+
+ ;; check that bXXb is not in locked region
+ (should (search-backward "Definition aXXa" nil t))
+ (beginning-of-line)
+ ;; (record-buffer-content (current-buffer))
+ ;; (message "locked until %s, point at %s"
+ ;; (span-end proof-locked-span) (point))
+ (point-should-be-unlocked))
+
+ ;; clean up
+ (when buffer
+ (with-current-buffer buffer
+ (set-buffer-modified-p nil)
+ (setq comment-style saved-comment-style))
+ (kill-buffer buffer)))))
diff --git a/ci/simple-tests/coq-test-goals-present.el
b/ci/simple-tests/coq-test-goals-present.el
index 6ba07db713..b3acfaf2db 100644
--- a/ci/simple-tests/coq-test-goals-present.el
+++ b/ci/simple-tests/coq-test-goals-present.el
@@ -141,7 +141,7 @@ Proof using.
(defun record-buffer-content (buf)
"Record buffer content of BUF via `message' for debugging.
-BUF should be a string."
+BUF should be a buffer as string or buffer object."
(with-current-buffer buf
(let ((content (buffer-substring-no-properties (point-min) (point-max))))
(message "%s buffer contains %d chars: %s" buf (length content)
content))))
diff --git a/ci/simple-tests/coq-test-omit-proofs.el
b/ci/simple-tests/coq-test-omit-proofs.el
index 20a54b6e82..24cd169964 100644
--- a/ci/simple-tests/coq-test-omit-proofs.el
+++ b/ci/simple-tests/coq-test-omit-proofs.el
@@ -132,8 +132,12 @@ 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
+ (looking-at "Qed\\.\n\n<prompt>Rocq <")
;; for Coq 8.10 and earlier
;; in 8.9 the message is on 1 line, in 8.10 on 3
(looking-at "Qed\\.\n<infomsg>\n?classic_excluded_middle is defined"))))
@@ -170,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 (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/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-abbrev.el b/coq/coq-abbrev.el
index 14658c51eb..3eefa60545 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -335,6 +335,10 @@
["Unset Printing All" coq-unset-printing-all t]
["Set Printing Implicit" coq-set-printing-implicit t]
["Unset Printing Implicit" coq-unset-printing-implicit t]
+ ["Set Printing Parentheses" coq-set-printing-parentheses t]
+ ["Unset Printing Parentheses" coq-unset-printing-parentheses t]
+ ["Set Printing Notations" coq-set-printing-notations t]
+ ["Unset Printing Notations" coq-unset-printing-notations t]
["Set Printing Coercions" coq-set-printing-coercions t]
["Unset Printing Coercions" coq-unset-printing-coercions t]
["Set Printing Compact Contexts" coq-set-printing-implicit t]
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-mode.el b/coq/coq-mode.el
index cdb0ef19ec..2bc1ec39e9 100644
--- a/coq/coq-mode.el
+++ b/coq/coq-mode.el
@@ -36,18 +36,24 @@
;; FIXME: this should probably be done like for smie above.
(defvar coq-may-use-prettify (fboundp 'prettify-symbols-mode))
-(defcustom coq-prog-name
- (or (if (executable-find "coqtop") "coqtop")
+(defun coq-detect-prog-gen (default &rest others)
+ (or (cl-find-if #'executable-find (cons default others))
(let ((exec-path (append exec-path '("C:/Program Files/Coq/bin"))))
- (executable-find "coqtop"))
- "coqtop")
+ (cl-find-if #'executable-find (cons default others)))
+ default))
+
+(defun coq-autodetect-progname ()
+ (coq-detect-prog-gen "coqtop" "rocq"))
+
+(defcustom coq-prog-name (coq-autodetect-progname)
"Name of program to run as Coq.
On Windows with latest Coq package you might need something like:
C:/Program Files/Coq/bin/coqtop.opt.exe
instead of just \"coqtop\".
This must be a single program name with no arguments. See option
`coq-prog-args' to manually adjust the arguments to the Coq process.
-See also `coq-prog-env' to adjust the environment."
+See also `coq-prog-env' to adjust the environment.
+With then 2025 new CLI 'rocq', this command only return 'rocq'."
:type 'string
:group 'coq
:group 'coq-mode)
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index 2ee58c049d..e0f0bf488f 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -84,7 +84,7 @@
;; 4- using -quick and the handling of .vo/.vio prerequisites for Coq < 8.11
;; 5- using -vos for Coq >= 8.11
;; 6- running vio2vo or -vok to check proofs
-;; 7- default-directory / current directory
+;; 7- default-directory / current directory and buffer local variables
;;
;;
;; For 1- where to put the Require command and the items that follow it:
@@ -116,13 +116,15 @@
;; dependency). At that time the 'lock-state property of the job is
;; set to 'locked. When a require job is retired, all ancestors with
;; 'lock-state property 'locked are collected by following the
-;; downward links. When the require job was successful, the collected
-;; jobs are stored in the 'coq-locked-ancestors property of the span
-;; belonging to that require command (in the 'require-span property).
-;; Furhter, the 'lock-state is set to 'asserted, such that another
-;; collection from a following require job ignores these jobs. A span
-;; delete action will unlock all uncestors in the
-;; 'coq-locked-ancestors property.
+;; downward links in a depth-first recursion. (Previous versions that
+;; collected ancestors upwards during dependant kickoff suffered from
+;; exponential blowup, see issues #499 and #572.) When the require job
+;; was successful, the collected jobs are stored in the
+;; 'coq-locked-ancestors property of the span belonging to that
+;; require command (in the 'require-span property). Furhter, the
+;; 'lock-state is set to 'asserted, such that another collection from
+;; a following require job ignores these jobs. A span delete action
+;; will unlock all uncestors in the 'coq-locked-ancestors property.
;;
;; When the require job was unsuccessful, all collected jobs are
;; unlocked.
@@ -137,19 +139,20 @@
;; retracts the queue region and resets all internal data.
;;
;; For `coq-compile-keep-going', the failing job, all ordinary
-;; dependants and all queue dependants are marked with 'failed. All
-;; ancestors that have already been registered in such a failed job
-;; are treated in the following way: If the ancestor is (via a
-;; different dependency path) an ancestor of a job that is still being
-;; compiled, then the ancestor is kept locked. Otherwise the ancestor
-;; is unlocked. Failed jobs continue with their normal state
-;; transition, but omit certain steps (eg., running coqc). If a coqc
-;; compilation finishes and all dependants are marked as failed, the
-;; ancestors are also treated in the way described before. If a failed
-;; require job is retired, nothing is done (especially its span is not
-;; asserted), unless it is the last compilation job. If the last
-;; compilation job is marked as failed when it is retired, then the
-;; whole queue region is retracted.
+;; dependants and all queue dependants are marked with 'failed.
+;; Therefore, if any job failed, the last require job is also marked
+;; as failed. Ancestors of failing require jobs are unlocked only when
+;; this last require is retired. At that time any ancestors of any
+;; preceeding successful require jobs have already been asserted.
+;; Failed jobs continue with their normal state transition, but omit
+;; certain steps (eg., running coqc). If the last compilation job is
+;; marked as failed at the time it is retired, then the whole queue
+;; region is retracted and all ancestors of this and all preceeding
+;; failed require jobs are unlocked. The ancestors to unlock are those
+;; with 'lock-state 'asserted and they are collected from the
+;; dependency tree just before unlocking. (Previous versions that
+;; collected ancestors upwards during dependant kickoff suffered from
+;; exponential blowup, see issues #499 and #572.)
;;
;; When a failing require command follows a bunch of commands that
;; take a while to process, it may happen, that the last failing
@@ -231,19 +234,21 @@
;; current value when the callback is executed.
;;
;;
-;; For 7- default-directory / current directory
+;; For 7- default-directory / current directory and buffer local variables
;;
-;; `default-directory' determines the current directory for background
-;; processes. In a sentinel or process filter, default-directory is
-;; taken from the current buffer, which is basically random. Starting
-;; with a wrong current directory will cause compilation failures.
-;; Therefore all entry points of this library must set
-;; default-directory. Entry points are coq-par-process-sentinel, the
-;; functions started from timer and those started from an empty entry
-;; in `proof-action-list'. To set default-directory in these cases, I
-;; record default-directory in 'current-dir inside
-;; `coq-par-preprocess-require-commands' and then pass it on to all
-;; jobs created.
+;; Sentinels and timer functions inherit local variables and the
+;; current directory (`default-directory') from the basically random
+;; buffer that is current when they are invoked. Users may have
+;; configured `coq-compiler' or other variables that influence
+;; background compilation, see issue #797. Therefore all entry points
+;; of this library must temporarily switch to the scripting buffer
+;; that caused the compilation, thereby implicitely also setting
+;; `default-directory' to the correct value. Such entry points are
+;; coq-par-process-sentinel, the functions started from timer and
+;; those started from an empty entry in `proof-action-list'. To set
+;; the current buffer in these cases, I record it in 'script-buf inside
+;; `coq-par-handle-require-list' and then pass it on to all jobs
+;; created.
;;
;;
;; Properties of compilation jobs
@@ -315,11 +320,13 @@
;; 'failed - t if coqdep or coqc for the job or one dependee failed.
;; 'visited - used in the dependency cycle detection to mark
;; visited jobs
-;; 'current-dir - current directory or default-directory of the buffer
-;; that contained the require command. Passed recursively
-;; to all jobs. Used to set default-directory in the
-;; sentinel and other functions, because it can otherwise
-;; be more or less random.
+;; 'script-buf - Buffer that cause the background compilation, i.e.,
+;; that contained a require command. This buffer
+;; is propagate to all dependencies and used as
+;; current buffer in all asynchronous functions
+;; (sentinels, timer functions, etc). This
+;; ensures that local variables and
+;; `default-directory' have correct values.
;; 'temp-require-file - temporary file name just containing the require
;; command of a require job for determining the files
;; needed for that require. Must be deleted after
@@ -761,22 +768,21 @@ earlier than 8.19."
Argument CLPATH must be `coq-load-path' from the buffer
that triggered the compilation, in order to provide correct
load-path options to coqdep."
- (nconc (copy-sequence coq-compile-extra-coqdep-arguments) ; copy for nconc
- (coq-par-coqdep-warning-arguments)
- (coq-coqdep-prog-args clpath
- (file-name-directory lib-src-file)
- (coq--pre-v85))
- (list lib-src-file)))
+ (nconc
+ (coq-coqdep-prog-args clpath (file-name-directory lib-src-file)
(coq--pre-v85))
+ (copy-sequence coq-compile-extra-coqdep-arguments) ; copy for nconc
+ (coq-par-coqdep-warning-arguments)
+ (list lib-src-file)))
(defun coq-par-coqc-arguments (lib-src-file clpath)
"Compute the command line arguments for invoking coqc on LIB-SRC-FILE.
Argument CLPATH must be `coq-load-path' from the buffer
that triggered the compilation, in order to provide correct
load-path options to coqdep."
- (nconc (copy-sequence coq-compile-extra-coqc-arguments) ; copy for nconc
- (coq-coqc-prog-args clpath
+ (nconc (coq-coqc-prog-args clpath
(file-name-directory lib-src-file)
(coq--pre-v85))
+ (copy-sequence coq-compile-extra-coqc-arguments) ; copy for nconc
(list lib-src-file)))
(defun coq-par-analyse-coq-dep-exit (status output command)
@@ -962,7 +968,8 @@ file to be deleted when the process does not finish
successfully."
(when coq--debug-auto-compilation
(message "%s %s: start %s %s in %s"
(get job 'name) process-name
- command (mapconcat #'identity arguments " ")
+ command
+ (mapconcat (lambda (a) (concat "\"" a "\"")) arguments " ")
default-directory))
(condition-case err
;; If the command is wrong, start-process aborts with an
@@ -999,15 +1006,17 @@ Runs when process PROCESS terminated because of EVENT. It
determines the exit status and calls the continuation function
that has been registered with that process. Normal compilation
errors are reported with an error message inside the callback.
-Starts as many queued jobs as possible. Second stage compilation
-jobs that have been killed, possibly because the user triggered a
-next first stage compilation, are put back into
-`coq--par-second-stage-queue'. If, at the end, no job is
-running in the background but compilation has not been finished,
-then, either second stage compilation finished (which is reported),
-or there must be a cycle in the dependencies, which is found
-and reported here. The cycle detection is skipped, if the
-retirement of the last compilation job has been delayed per
+Starts as many queued jobs as possible. The callback and queued
+jobs are done with the 'script-buf as current buffer, such that
+local variables and `default-directory' have correct values.
+Second stage compilation jobs that have been killed, possibly
+because the user triggered a next first stage compilation, are
+put back into `coq--par-second-stage-queue'. If, at the end, no
+job is running in the background but compilation has not been
+finished, then, either second stage compilation finished (which
+is reported), or there must be a cycle in the dependencies, which
+is found and reported here. The cycle detection is skipped, if
+the retirement of the last compilation job has been delayed per
`coq--par-delayed-last-job'. All signals are caught inside this
function and reported appropriately."
(condition-case err
@@ -1035,43 +1044,45 @@ function and reported appropriately."
(coq-par-second-stage-enqueue
(process-get process 'coq-compilation-job))))
;; process was not killed explicitly by us
- (let (exit-status
- (default-directory
- (get (process-get process 'coq-compilation-job) 'current-dir)))
- (when coq--debug-auto-compilation
- (message
- (concat "%s %s: TTT process status changed to %s "
- "command: %s\n default-dir: %s curr buf %s")
- (get (process-get process 'coq-compilation-job) 'name)
- (process-name process)
- event
- (mapconcat 'identity (process-get process 'coq-process-command) "
")
- default-directory
- (buffer-name)))
- (cond
- ((eq (process-status process) 'exit)
- (setq exit-status (process-exit-status process)))
- (t (setq exit-status "abnormal termination")))
- (setq coq--current-background-jobs
- (max 0 (1- coq--current-background-jobs)))
- (funcall (process-get process 'coq-process-continuation)
- process exit-status)
- (coq-par-start-jobs-until-full)
- (when (and coq--par-second-stage-in-progress
- (eq coq--current-background-jobs 0))
- (setq coq--par-second-stage-in-progress nil)
- (if (coq--post-v811)
- (message "vok compilation finished")
- (message "vio2vo compilation finished")))
- (when (and
- (not coq--par-delayed-last-job)
- (eq coq--current-background-jobs 0)
- coq--last-compilation-job)
- (let ((cycle (coq-par-find-dependency-circle)))
- (if cycle
- (signal 'coq-compile-error-circular-dep
- (mapconcat #'identity cycle " -> "))
- (error "Deadlock in parallel compilation"))))))
+ (with-current-buffer
+ (get (process-get process 'coq-compilation-job) 'script-buf)
+ (let (exit-status)
+ (when coq--debug-auto-compilation
+ (message
+ (concat "%s %s: TTT process status changed to %s "
+ "command: %s\n default-dir: %s curr buf %s")
+ (get (process-get process 'coq-compilation-job) 'name)
+ (process-name process)
+ event
+ (mapconcat 'identity
+ (process-get process 'coq-process-command)
+ " ")
+ default-directory
+ (buffer-name)))
+ (cond
+ ((eq (process-status process) 'exit)
+ (setq exit-status (process-exit-status process)))
+ (t (setq exit-status "abnormal termination")))
+ (setq coq--current-background-jobs
+ (max 0 (1- coq--current-background-jobs)))
+ (funcall (process-get process 'coq-process-continuation)
+ process exit-status)
+ (coq-par-start-jobs-until-full)
+ (when (and coq--par-second-stage-in-progress
+ (eq coq--current-background-jobs 0))
+ (setq coq--par-second-stage-in-progress nil)
+ (if (coq--post-v811)
+ (message "vok compilation finished")
+ (message "vio2vo compilation finished")))
+ (when (and
+ (not coq--par-delayed-last-job)
+ (eq coq--current-background-jobs 0)
+ coq--last-compilation-job)
+ (let ((cycle (coq-par-find-dependency-circle)))
+ (if cycle
+ (signal 'coq-compile-error-circular-dep
+ (mapconcat #'identity cycle " -> "))
+ (error "Deadlock in parallel compilation")))))))
;; coq-compile-error-start can be signaled inside the continuation
;; function, if that tries to start new jobs
;; XXX catch this error also in coq-par-preprocess-require-commands
@@ -1094,9 +1105,9 @@ function and reported appropriately."
(defun coq-par-run-second-stage-queue ()
"Start delayed second stage compilation (vio2vo or vok).
-Set `default-directory' from the 'current-dir property of the
-head of the second stage queue, such that processes started here
-run with the right current directory."
+Use the buffer stored in the 'script-buf property as current
+buffer for starting processes, such that local variables and, in
+particular, `default-directory' have the correct values."
;; when the user starts another compilation, the timer for second
;; stage is canceled
(cl-assert (not coq--last-compilation-job)
@@ -1105,12 +1116,11 @@ run with the right current directory."
(when coq--debug-auto-compilation
(message "Start second stage processing for %d jobs"
(coq-par-second-stage-queue-length)))
- (let ((head (coq-par-second-stage-head))
- default-directory)
+ (let ((head (coq-par-second-stage-head)))
(when head
- (setq default-directory (get head 'current-dir))
- (setq coq--par-second-stage-in-progress t)
- (coq-par-start-jobs-until-full))))
+ (with-current-buffer (get head 'script-buf)
+ (setq coq--par-second-stage-in-progress t)
+ (coq-par-start-jobs-until-full)))))
(defun coq-par-require-processed (race-counter)
"Callback for `proof-action-list' to signal completion of the last Require.
@@ -1484,9 +1494,12 @@ should be cleared before the next collection run."
Return all not yet asserted ancestors for successful jobs JOB as
well as for failed jobs JOB. For successful jobs, the not yet
asserted ancestors of preceeding require jobs have been collected
-in a previous collection run. For failed jobs, this is not the
-case, therefore, for failed jobs, this function recureses into
-the preceeding require job, if it exists."
+in a previous collection run and have been asserted back then.
+For failed jobs, this is not the case and, moreover, ancestor
+unlocking can only be done when the last failing reqire job is
+retired. Therefore, for failed jobs, this function recureses into
+the preceeding require job, if it exists and is also marked as
+failed."
(let ((this-anc (coq-par-collect-locked-ancestors-dependees job))
(q-dep (get job 'queue-dependee))
prev-anc)
@@ -1497,12 +1510,14 @@ the preceeding require job, if it exists."
(defun coq-par-collect-locked-require-ancestors (job)
"Top-level ancestor collection function - collects not asserted ancestors.
Return all not yet asserted ancestors for successful jobs JOB as
-well as for failed jobs JOB. For failed require jobs JOB, this
-entails visiting the preceeding require job. The recursion
-internally uses property 'collect-visited to mark already visited
-jobs in order to avoid an exponential blowup in graphs that are
-not trees. This property is reset here after collection, such
-that its use stays internal."
+well as for failed jobs JOB. For failed require jobs JOB,
+additionally collect all asserted ancestors of all preceeding
+failed require jobs. This is necessary, because for failed jobs,
+unlocking only happens when the last require job is retired. The
+recursion internally uses property 'collect-visited to mark
+already visited jobs in order to avoid an exponential blowup in
+graphs that are not trees. This property is reset here after
+collection, such that its use stays internal."
(let ((ancs (coq-par-collect-locked-require-ancestors-rec job)))
(mapc (lambda (job) (put job 'collect-visited nil)) ancs)
(when coq--debug-auto-compilation
@@ -1570,10 +1585,12 @@ jobs when they transition from 'waiting-queue to 'ready:
(defun coq-par-kickoff-queue-from-action-list (job)
"Trigger `coq-par-kickoff-queue-maybe' from action list.
-Simple wrapper around `coq-par-kickoff-queue-maybe' to set
-`default-directory' when entering background compilation
-functions from `proof-action-list'."
- (let ((default-directory (get job 'current-dir)))
+Simple wrapper around `coq-par-kickoff-queue-maybe' to ensure the
+right scripting buffer is the current buffer and local variables
+and `default-directory' are taken from there. This function is
+used to enter background compilation functions from
+`proof-action-list'."
+ (with-current-buffer (get job 'script-buf)
(when coq--debug-auto-compilation
(message "%s: TTT retry queue kickoff after processing action list"
(get job 'name)))
@@ -1837,17 +1854,20 @@ This function may be called asynchronously, if the
require job
was queued."
;; get coq-load-path from job
;; check that this really includes the current dir in the arguments
- (let ((load-path
- ;; For coq < 8.5 coqdep needs the current working directory
- ;; in the load path. This differs from the directory containing
- ;; 'temp-require-file. Therefore we add it here and tweek
- ;; coq-load-path-include-current such that coq-coqdep-prog-args
- ;; does not add the directory containing 'temp-require-file to
- ;; load-path.
- (if (and coq-load-path-include-current (coq--pre-v85))
- (cons (get job 'current-dir) (get job 'load-path))
- (get job 'load-path)))
- (coq-load-path-include-current nil)
+ (let (
+ ;; passively supported coq versions start now with >= 8.9.1 --
+ ;; do not maintain 8.4 compatibility
+ ;; (load-path
+ ;; ;; For coq < 8.5 coqdep needs the current working directory
+ ;; ;; in the load path. This differs from the directory containing
+ ;; ;; 'temp-require-file. Therefore we add it here and tweek
+ ;; ;; coq-load-path-include-current such that coq-coqdep-prog-args
+ ;; ;; does not add the directory containing 'temp-require-file to
+ ;; ;; load-path.
+ ;; (if (and coq-load-path-include-current (coq--pre-v85))
+ ;; (cons (get job 'current-dir) (get job 'load-path))
+ ;; (get job 'load-path)))
+ ;; (coq-load-path-include-current nil)
(require-command
(mapconcat #'identity (nth 1 (car (get job 'queueitems))) " "))
(temp-file (make-temp-file "ProofGeneral-coq" nil ".v")))
@@ -1859,7 +1879,7 @@ was queued."
(get job 'temp-require-file)))
(coq-par-start-process
coq-dependency-analyzer
- (coq-par-coqdep-arguments (get job 'temp-require-file) load-path)
+ (coq-par-coqdep-arguments (get job 'temp-require-file) (get job
'load-path))
'coq-par-process-coqdep-result
job
(get job 'temp-require-file))))
@@ -1877,6 +1897,8 @@ Lock the source file and start the coqdep background
process."
(message "%s: TTT start coqdep for file job for file %s"
(get job 'name)
(get job 'src-file)))
+ (if coq--debug-auto-compilation
+ (message "%s: UUU start %s" (get job 'name) (cons
coq-dependency-analyzer (coq-par-coqdep-arguments (get job 'src-file) (get job
'load-path)))))
(coq-par-start-process
coq-dependency-analyzer
(coq-par-coqdep-arguments (get job 'src-file) (get job 'load-path))
@@ -1897,13 +1919,15 @@ used."
(let ((arguments
(coq-par-coqc-arguments (get job 'src-file) (get job 'load-path))))
(cond
- ((eq (get job 'use-quick) 'vos) (push "-vos" arguments))
- ((eq (get job 'use-quick) 'vio) (push "-quick" arguments))
+ ((eq (get job 'use-quick) 'vos) (nconc arguments (list "-vos")))
+ ((eq (get job 'use-quick) 'vio) (nconc arguments (list "-quick")))
(t t))
(when coq--debug-auto-compilation
(message "%s: TTT start coqc compile for file job for file %s"
(get job 'name)
(get job 'src-file)))
+ (if coq--debug-auto-compilation
+ (message "%s: VVV start %S %S" (get job 'name) coq-compiler arguments))
(coq-par-start-process
coq-compiler
arguments
@@ -1924,7 +1948,9 @@ used."
(get job 'src-file)))
(let ((arguments
(coq-par-coqc-arguments (get job 'src-file) (get job 'load-path))))
- (push "-vok" arguments)
+ (nconc arguments (list "-vok"))
+ (if coq--debug-auto-compilation
+ (message "%s: WWW start %S %S" (get job 'name) coq-compiler arguments))
(coq-par-start-process
coq-compiler
arguments
@@ -1998,18 +2024,19 @@ synchronously or asynchronously."
(coq-par-start-task new-job)
(coq-par-job-enqueue new-job)))
-(defun coq-par-job-init-common (clpath type current-dir)
+(defun coq-par-job-init-common (clpath type script-buf)
"Common initialization for 'require and 'file jobs.
Create a new job of type TYPE and initialize all common fields of
require and file jobs that need an initialization different from
-nil."
+nil. Argument SCRIPT-BUF must be the script buffer that caused
+the background compilation."
(let ((new-job (make-symbol "coq-compile-job-symbol")))
(put new-job 'name (format "job-%d" coq--par-next-id))
(setq coq--par-next-id (1+ coq--par-next-id))
(put new-job 'coqc-dependency-count 0)
(put new-job 'type type)
(put new-job 'state 'enqueued-coqdep)
- (put new-job 'current-dir current-dir)
+ (put new-job 'script-buf script-buf)
;; The ancestor modification time is not really needed in require
;; jobs, however, if the field is present, we can treat require
;; and file jobs more uniformely.
@@ -2017,26 +2044,25 @@ nil."
(put new-job 'load-path clpath)
new-job))
-(defun coq-par-create-require-job (clpath require-items require-span
- current-dir)
+(defun coq-par-create-require-job (clpath require-items require-span
script-buf)
"Create a new require job for REQUIRE-SPAN.
-Create a new require job and initialize its fields. CLPATH
-is the load path configured for the current scripting buffer,
-that is passed down to all dependencies and used in all
-compilations. REQUIRE-ITEMS are the non-require commands
-following the REQUIRE-SPAN, they are temporarily stored in the
-new require job outside of `proof-action-list'.
-
-The current directory (from `default-directory') is stored in
-property 'current-dir and propagated to all dependend jobs. This
-is used to set `default-directory' when entering background
-compilation from a sentinel or elsewhere.
+Create a new require job and initialize its fields. CLPATH is the
+load path configured for the current scripting buffer, that is
+passed down to all dependencies and used in all compilations.
+REQUIRE-ITEMS are the non-require commands following the
+REQUIRE-SPAN, they are temporarily stored in the new require job
+outside of `proof-action-list'. SCRIPT-BUF must be the script
+buffer that caused the background compilation. It is stored in
+property 'script-buf and propagated to all dependent jobs. This
+buffer is made current in all sentinels and other asynchronously
+called functions to ensure local variables and, in particular,
+`default-directory' are correct.
This function is called synchronously when asserting. The new
require job is neither started nor enqueued here - the caller
must do this."
(let* ((coq-load-path clpath)
- (new-job (coq-par-job-init-common clpath 'require current-dir)))
+ (new-job (coq-par-job-init-common clpath 'require script-buf)))
(put new-job 'require-span require-span)
(put new-job 'queueitems require-items)
(when coq--debug-auto-compilation
@@ -2050,14 +2076,15 @@ must do this."
;; there was some error and it was not used anywhere back then, but
;; job is now needed as a dependency of some other file?
;; XXX what happens if the job exists and is failed?
-(defun coq-par-create-file-job (module-vo-file clpath dep-src-file
- current-dir)
+(defun coq-par-create-file-job (module-vo-file clpath dep-src-file script-buf)
"Create a new file job for MODULE-VO-FILE.
DEP-SRC-FILE is the source file whose coqdep output we are just
processing and which depends on MODULE-VO-FILE. This argument is
only used in the error message, when MODULE-VO-FILE happens to
coincide with the current scripting buffer (which means we
-detected a dependency cycle).
+detected a dependency cycle). SCRIPT-BUF must be the current
+scripting buffer and CLPATH must be the load path configured in
+there, see also `coq-par-create-require-job'.
If there is a file job for MODULE-VO-FILE, just return this.
Otherwise, create a new file job and initialize its fields. In
@@ -2069,7 +2096,7 @@ If a new job is created it is started or enqueued right
away."
((gethash module-vo-file coq--compilation-object-hash))
(t
(let* ((coq-load-path clpath)
- (new-job (coq-par-job-init-common clpath 'file current-dir)))
+ (new-job (coq-par-job-init-common clpath 'file script-buf)))
;; fields 'required-obj-file and obj-mod-time are implicitely set to nil
(put new-job 'vo-file module-vo-file)
(put new-job 'src-file (coq-library-src-of-vo-file module-vo-file))
@@ -2129,12 +2156,12 @@ error, the job is marked as failed or compilation is
aborted via
a signal (depending on `coq-compile-keep-going'). If there was no
coqdep error, the following actions are taken.
- temp-require-file for require jobs is deleted
-- the job that started PROCESS is put into sate 'waiting-dep
-- a new job is created for every dependency. If this new job is
- not immediately ready, a dependency is registered from the
- new job to the current job. For dependencies that are 'ready
+- the job that started PROCESS is put into state 'waiting-dep
+- a new job is created for every dependency and registered in the
+ dependency tree of all jobs. For dependencies that are 'ready
already, the most recent ancestor modification time is
- propagated.
+ propagated. If a dependency is marked as failed the current job
+ is also marked as failed.
- if there are no dependencies (especially if coqdep failed) or
all dependencies are ready already, the next transition is
triggered. For file jobs the next transition goes to
@@ -2175,7 +2202,7 @@ is directly passed to `coq-par-analyse-coq-dep-exit'."
(let* ((dep-job (coq-par-create-file-job dep-vo-file
(get job 'load-path)
(get job 'src-file)
- (get job 'current-dir)))
+ (get job 'script-buf)))
(dep-time (get dep-job 'youngest-coqc-dependency)))
(when (get dep-job 'failed)
(setq dependee-failed t))
@@ -2291,19 +2318,24 @@ the compilation as current, otherwise a wrong
`coq-load-path'
might be used.
This function is called synchronously when asserting."
+ ;; need a current proof script buffer where we can switch to in a
+ ;; sentinel or in a timer function
+ (cl-assert (bufferp proof-script-buffer) nil
+ "no current proof script buffer when handling require commands")
(let ((span (caar require-items))
new-job)
(when coq--debug-auto-compilation
(let* ((require-item (car require-items))
(require-command (mapconcat 'identity (nth 1 require-item) " ")))
- (message "handle require command \"%s\"" require-command)))
+ (message "handle require command \"%s\"\nin script buffer %s"
+ require-command proof-script-buffer)))
(span-add-delete-action
span
(lambda () (coq-unlock-all-ancestors-of-span span)))
;; create a new require job and maintain coq--last-compilation-job
(setq new-job
(coq-par-create-require-job coq-load-path require-items span
- default-directory))
+ proof-script-buffer))
(when coq--last-compilation-job
(coq-par-add-queue-dependency coq--last-compilation-job new-job))
(setq coq--last-compilation-job new-job)
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-syntax.el b/coq/coq-syntax.el
index 7d3251d6f2..c66b8107a9 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -641,6 +641,7 @@ They deserve a separate menu for sending them to Coq
without insertion.")
("From" nil "From #." nil "From")
("Generalizable Variables" nil "Generalizable Variables #." t
"Generalizable\\s-+Variables")
("Generalizable All Variables" nil "Generalizable All Variables." t
"Generalizable\\s-+All\\s-+Variables")
+ ("Guarded" nil "Guarded." t "Guarded")
("Identity Coercion" nil "Identity Coercion #." t "Identity\\s-+Coercion")
("Implicit Arguments Off" nil "Implicit Arguments Off." t
"Implicit\\s-+Arguments\\s-+Off")
("Implicit Arguments On" nil "Implicit Arguments On." t
"Implicit\\s-+Arguments\\s-+On")
diff --git a/coq/coq-system.el b/coq/coq-system.el
index ad65cc4bc2..6ca50e2c45 100644
--- a/coq/coq-system.el
+++ b/coq/coq-system.el
@@ -29,6 +29,14 @@
(defvar coq-prog-args)
(defvar coq-debug)
+;; Regular files should be of the form "valid_modulename.v" coq
+;; accepts lots of things as letter, this is probably much stricter.
+;; In practice it should be OK though, except maybe for non latin
+;; characters.
+(defun coq-regular-filename-p (s)
+ (let ((noext (file-name-base s)))
+ (string-match-p "\\`[[:alpha:]_][[:alnum:]_]*\\'" noext)))
+
;; Arbitrary arguments can already be passed through _CoqProject.
;; However this is not true for all assistants, so we don't modify the
;; (defpgcustom prog-args) declaration.
@@ -38,24 +46,44 @@
(put 'coq-prog-args 'safe-local-variable #'coq--string-list-p)
+;; DEAD CODE?
(defcustom coq-prog-env nil
"List of environment settings to pass to Coq process.
On Windows you might need something like:
(setq coq-prog-env '(\"HOME=C:\\Program Files\\Coq\\\"))"
:group 'coq)
-(defcustom coq-dependency-analyzer
- (if (executable-find "coqdep") "coqdep"
- (proof-locate-executable "coqdep" t '("C:/Program Files/Coq/bin")))
+;; We just call "rocq" and look the error message that should mention
+;; subcommands
+(defun coq-detect-rocq-cli ()
+ "return non nil if the detected coq/rocq executable obeys the rocq CLI."
+ (let* ((coq-command (or proof-prog-name (coq-autodetect-progname))))
+ (condition-case nil
+ (with-temp-buffer
+ (apply 'process-file (list coq-command nil t))
+ (string-match "Supported subcommands:" (buffer-string)))
+ (error nil))))
+
+(defun coq-detect-coqdep ()
+ (if (coq-detect-rocq-cli) (coq-detect-prog-gen "rocq")
+ (coq-detect-prog-gen "coqdep")))
+(defun coq-detect-coqc ()
+ (if (coq-detect-rocq-cli) (coq-detect-prog-gen "rocq")
+ (coq-detect-prog-gen "coqc")))
+
+;; We return the executable coqtop or rocq. But not the rocq option
+;; (dep, c, top)) triggering the particular tool.
+(defcustom coq-dependency-analyzer (coq-detect-coqdep)
"Command to invoke coqdep."
:type 'string
+ :safe 'stringp
:group 'coq)
-(defcustom coq-compiler
- (if (executable-find "coqc") "coqc"
- (proof-locate-executable "coqc" t '("C:/Program Files/Coq/bin")))
+(defcustom coq-compiler (coq-detect-coqc)
+ ;FIXME
"Command to invoke the coq compiler."
:type 'string
+ :safe 'stringp
:group 'coq)
(defcustom coq-pinned-version nil
@@ -112,16 +140,16 @@ The given option should make coqtop return immediately.
Optionally check the return code and return nil if the check
fails. Return also nil on other kinds of errors (e.g., `coq-prog-name'
not found).
-This function supports calling coqtop via tramp."
- (let ((coq-command (or coq-prog-name "coqtop"))
- retv)
+This function supports calling coqtop via tramp.
+This function must not rely on coq-autodetect-version, it would be a cycle."
+ (let* ((coq-command (or proof-prog-name coq-prog-name
(coq-autodetect-progname)))
+ (coq-args (if (coq-detect-rocq-cli) (list "top" option) (list
option)))
+ (process-args (append (list coq-command nil t nil) coq-args))
+ retv)
(condition-case nil
(with-temp-buffer
- (setq retv (if option
- (process-file coq-command nil t nil option)
- (process-file coq-command nil t nil)))
- (if (or (not expectedretv) (equal retv expectedretv))
- (buffer-string)))
+ (setq retv (apply 'process-file process-args))
+ (if (or (not expectedretv) (equal retv expectedretv))
(buffer-string)))
(error nil))))
(defun coq-autodetect-version (&optional interactive-p)
@@ -142,7 +170,6 @@ Interactively (with INTERACTIVE-P), show that number."
(let ((coq-output (coq-callcoq "-help")))
(setq coq-autodetected-help (or coq-output ""))))
-
(defun coq--version< (v1 v2)
"Compare Coq versions V1 and V2."
;; -snapshot is only supported by Emacs 24.5, not 24.3
@@ -441,65 +468,76 @@ options of a few coq-project files does the right thing."
(coq--options-test-roundtrip "-R /test Test")
(coq--options-test-roundtrip "-I /test")))
-(defun coq-coqdep-prog-args (loadpath &optional current-directory pre-v85)
+;; it is better to inform coqtop of the name of the current module
+;; using the -topfile option, so that coqtop understands references
+;; to it. But don't insist if this would fail (because of wrong
+;; file name): Some people want to script .v files without ever
+;; compiling them.
+(defun coq-topfile-prog-arg ()
+ (when (and (coq--supports-topfile) buffer-file-name)
+ (if (coq-regular-filename-p buffer-file-name)
+ (cons "-topfile" (cons buffer-file-name nil))
+ (message "Warning: buffer %s seems not compilable," buffer-file-name)
+ (message "probably because of its name, no -topfile option set.")
+ nil)))
+
+
+(defun coq-include-prog-args (loadpath &optional current-directory pre-v85)
"Build a list of options for coqdep.
LOADPATH, CURRENT-DIRECTORY, PRE-V85: see `coq-include-options'."
(coq-include-options loadpath current-directory pre-v85))
(defun coq--clean-prog-args (args)
- "Return ARGS without the entries added by `coq-coqtop-prog-args'.
+ "Return ARGS without the entries added by `coq-coqtop-prog-args' and such.
Such entries are currently -emacs and -topfile."
(pcase args
- ((or `("-emacs" . ,rest)
+ ((or `("-emacs" . ,rest) `("top" . ,rest) `("c" . ,rest) `("dep" . ,rest)
`("-topfile" . (,(pred (apply-partially #'equal buffer-file-name)) .
,rest)))
(coq--clean-prog-args rest))
(`(,car . ,cdr)
(cons car (coq--clean-prog-args cdr)))
(_ args)))
+
+(defun coq-common-prog-args (loadpath &optional current-directory pre-v85)
+ "Build a list of options common for coqc and coqtop and coqdep.
+LOADPATH, CURRENT-DIRECTORY, PRE-V85: see `coq-include-options'."
+;; coqtop always adds the current directory to the LoadPath, so don't
+ ;; include it in the -Q options.
+ (append (coq--clean-prog-args coq-prog-args)
+ (let* ((coq-load-path-include-current nil)
+ (cmd (coq-include-prog-args loadpath current-directory
pre-v85)))
+ cmd)))
+
+(defun coq-coqdep-prog-args (loadpath &optional current-directory pre-v85)
+ "Build a list of option for coqdep."
+ (append
+ (if (coq-detect-rocq-cli) (list "dep") nil)
+ (coq-include-prog-args loadpath current-directory pre-v85)))
+
(defun coq-coqc-prog-args (loadpath &optional current-directory pre-v85)
"Build a list of options for coqc.
LOADPATH, CURRENT-DIRECTORY, PRE-V85: see `coq-include-options'."
;; coqtop always adds the current directory to the LoadPath, so don't
;; include it in the -Q options.
- (append (coq--clean-prog-args coq-prog-args)
- (let ((coq-load-path-include-current nil)) ; Not needed in >=8.5beta3
- (coq-coqdep-prog-args loadpath current-directory pre-v85))))
+ (append (if (coq-detect-rocq-cli) (list "c") nil)
+ (coq-common-prog-args loadpath current-directory pre-v85)))
-;;XXXXXXXXXXXXXX
;; coq-coqtop-prog-args is the user-set list of arguments to pass to
;; Coq process, see 'defpacustom prog-args' in pg-custom.el for
;; documentation.
-;; Regular files should be of the form "valid_modulename.v" coq
-;; accepts lots of things as letter, this is probably much stricter.
-;; In practice it should be OK though, except maybe for non latin
-;; characters.
-(defun coq-regular-filename-p (s)
- (let ((noext (file-name-base s)))
- (string-match-p "\\`[[:alpha:]_][[:alnum:]_]*\\'" noext)))
-
(defun coq-coqtop-prog-args (loadpath &optional current-directory pre-v85)
;; coqtop always adds the current directory to the LoadPath, so don't
;; include it in the -Q options. This is not true for coqdep.
"Build a list of options for coqc.
LOADPATH, CURRENT-DIRECTORY, PRE-V85: see `coq-coqc-prog-args'."
- (let ((topfile-supported (coq--supports-topfile)))
- (append
- ;; it is better to inform coqtop of the name of the current module
- ;; using the -topfile option, so that coqtop understands references
- ;; to it. But don't insist if this would fail (because of wrong
- ;; file name): Some people want to script .v files without ever
- ;; compiling them.
- (if (and topfile-supported buffer-file-name
- (coq-regular-filename-p buffer-file-name))
- (cons "-topfile" (cons buffer-file-name nil))
- (if (and topfile-supported buffer-file-name)
- (message "Warning: this Coq buffer is probably not compilable \
-because of its name, no -topfile option set."))
- nil)
- (cons "-emacs" (coq-coqc-prog-args loadpath current-directory pre-v85)))))
+ (append
+ (if (coq-detect-rocq-cli) (list "top") nil)
+ (list "-emacs")
+ (coq-topfile-prog-arg)
+ (coq-common-prog-args loadpath current-directory pre-v85)))
(defun coq-prog-args ()
"Recompute `coq-load-path' before calling `coq-coqtop-prog-args'."
@@ -520,29 +558,71 @@ path (including the -R lib options) (see
`coq-load-path')."
:safe 'booleanp
:group 'coq)
-(defcustom coq-project-filename "_CoqProject"
- "The name of coq project file.
-The coq project file of a coq development (cf. Coq documentation on
-\"makefile generation\") should contain the arguments given to
-coq_makefile. In particular it contains the -I and -R
-options (preferably one per line). If `coq-use-coqproject' is
-t (default) the content of this file will be used by Proof General to
-infer the `coq-load-path' and the `coq-prog-args' variables that set
-the coqtop invocation by Proof General. This is now the recommended
-way of configuring the coqtop invocation. Local file variables may
-still be used to override the coq project file's configuration.
-.dir-locals.el files also work and override project file settings."
+;; FIXME: should we add "Make" as a valid project name? Maybe only if
+;; _xxProject is not present? And/Or if its content seems ok?
+;; \\` and \\' avoid matching "_CoqProject~" and such
+(defcustom coq-project-file-regexp "\\`\\(_coqproject\\|_rocqproject\\)\\'"
+ "The regexp matching file names which PG detects as coq/rocq project files.
+
+It is used by `coq--default-project-find-file' in a case insensistive way."
:type 'string
:safe 'stringp
:group 'coq)
+
+(defun coq--default-project-find-file (dir)
+ "Default function for `coq-project-filename'.
+
+If DIR contains an acceptable coq/rocq project file, return it. Return
+nil otherwise. See `coq-project-filename'."
+ (when (file-directory-p dir)
+ (let* ((case-fold-search t) (files (directory-files dir)))
+ (cl-find-if (lambda (s) (string-match coq-project-file-regexp s nil))
files))))
+
+(defcustom coq-project-filename 'coq--default-project-find-file
+ "Variable containing the function detecting a project file.
+
+See its default value `coq--default-project-find-file' for an example.
+
+The function takes one argument, the name of a directory, and returns
+the name of a coq/rocq project file it contains if there is one. Return
+nil otherwise.
+
+This is used to detect the coq project file (using
+`locate-dominating-file'). By default we accept _CoqProject and
+_RocqProject (and any case-variant of these) without checking coq/rocq
+version. If you want something smarter please redefine
+`coq-project-filename' directly by using:
+
+(setq coq-project-filename #'my-own-predicate)
+
+About the coq/rocq project file (cf. Coq documentation on project files
+and \"makefile generation\"):
+
+The coq project file of a coq development should contain the arguments
+given to coq_makefile. In particular it contains the -I and -R
+options (preferably one per line). If `coq-use-coqproject' is
+t (default) the content of this file will be used by Proof General to
+infer the `coq-load-path' and the `coq-prog-args' variables that set the
+coqtop invocation by Proof General. This is now the recommended way of
+configuring the coqtop invocation. Local file variables may still be
+used to override the coq project file's configuration. .dir-locals.el
+files also work and override project file settings.
+"
+ :type 'function
+ :group 'coq)
+
(defun coq-find-project-file ()
"Return '(buf alreadyopen) where buf is the buffer visiting coq project file.
alreadyopen is t if buffer already existed."
(when buffer-file-name
- (let* ((projectfiledir (locate-dominating-file buffer-file-name
coq-project-filename)))
+ (let* ((projectfiledir
+ (locate-dominating-file
+ buffer-file-name
+ (lambda (f) (funcall coq-project-filename f)))))
(when projectfiledir
- (let* ((projectfile (expand-file-name coq-project-filename
projectfiledir))
+ (let* ((projectfilel (funcall coq-project-filename projectfiledir))
+ (projectfile (expand-file-name projectfilel projectfiledir))
;; we store this intermediate result to know if we have to kill
;; the coq project buffer at the end
(projectbufferalreadyopen (find-buffer-visiting projectfile))
@@ -601,7 +681,7 @@ coqtop. But -arg \"'a b'\" means to pass a and b together."
(setq args
(append args
(split-string-and-unquote concatenated-args
coq--project-file-separator)))))))
- (cons "-emacs" args)))
+ args))
(defun coq--extract-load-path-1 (option base-directory)
"Convert one _CoqProject OPTION, relative to BASE-DIRECTORY."
@@ -684,6 +764,11 @@ Does nothing if `coq-use-project-file' is nil."
;; avoid adding for other modes , the setting is performed inside
;; coq-mode-hook. This is described in www.emacswiki.org/emacs/LocalVariables
+;; NOTE: the coq-prog-arg variable is local to the buffer, and it is
+;; re-populated each time coq is launched on this buffer. In other
+;; words: this hook is useful for coq files on which coq will not be
+;; run.
+
;; TODO: also read COQBIN somewhere?
;; Note: this does not need to be at a particular place in the hook, but we
;; need to make this hook local.
@@ -694,14 +779,38 @@ Does nothing if `coq-use-project-file' is nil."
#'coq-load-project-file
nil t)))
-; detecting coqtop args should happen at the last moment before
-; calling the process. In particular it should ahppen after that
-; proof-prog-name-ask is performed, this hook is at the right place.
+;; Detecting coqtop or rocq args should happen at the last moment
+;; before calling the process. In particular it should happen after
+;; that proof-prog-name-ask is performed. This hook is exactly called
+;; after querying proof-prog-name (if proof-prog-name-ask is t). This
+;; way the options can be elaborated correctly (coqtop and rocq have
+;; different options). We first detect executables (taking
+;; proof-prog-name-ask into account), then elaborate the
+;; proof-prog-args. Note: we don't support proof-prog-name-guess
(add-hook 'proof-shell-before-process-hook
(lambda ()
- ;; It seems coq-prog-name and proof-prog-name are not correctly
linked
- ;; so let us make sure they are the same before computing options
+ ;; detect executables unless explicitely set by hand. In
+ ;; this case we try to find coqdep and coqc in the same
+ ;; directory
+ (if (and proof-prog-name-ask proof-prog-name)
+ ;; let us find other executables in the exact same
+ ;; place. TODO: go back to default exec-path if not found?
+ (let ((exec-path (list (file-name-directory proof-prog-name))))
+ (setq coq-compiler (executable-find (coq-detect-coqc)))
+ (setq coq-dependency-analyzer (executable-find
(coq-detect-coqdep))))
+ ;; default: detect everything from the current exec-path
+ (setq proof-prog-name (coq-autodetect-progname))
+ (setq coq-compiler (coq-detect-coqc))
+ (setq coq-dependency-analyzer (coq-detect-coqdep)))
+ (when coq-debug
+ (message "coq-proof-prog-name: %S" proof-prog-name)
+ (message "coq-dependency-analyzer: %S" coq-dependency-analyzer)
+ (message "coq-compiler: %S" coq-compiler))
+ ;; in principe coq-prog-name is only used to set up
+ ;; proof-prog-name, but it may sometimes be used by itself
+ ;; so let us sync them
(setq coq-prog-name proof-prog-name)
+ ;; now elaborate args
(setq coq-prog-args (coq-prog-args))))
;; smie's parenthesis blinking is too slow, let us have the default one back
@@ -727,48 +836,4 @@ Does nothing if `coq-use-project-file' is nil."
(provide 'coq-system)
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; To guess the command line options ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; OBSOLETE, should take _CoqProject into account.
-(defun coq-guess-command-line (filename)
- "Guess the right command line options to compile FILENAME using `make -n'.
-This function is obsolete, the recommended way of setting the coqtop
-options is to use a _Coqproject file as described in coq
-documentation. ProofGeneral reads this file and sets compilation
-options according to its contents. See `coq-project-filename'. Per
-file configuration may then be set using local file variables."
- (if (local-variable-p 'coq-prog-name (current-buffer))
- coq-prog-name
- (let* ((dir (or (file-name-directory filename) "."))
- (makedir
- (cond
- ((file-exists-p (concat dir "Makefile")) ".")
- ;; ((file-exists-p (concat dir "../Makefile")) "..")
- ;; ((file-exists-p (concat dir "../../Makefile")) "../..")
- (t nil))))
- (if (and coq-use-makefile makedir)
- (let*
- ;;TODO, add dir name when makefile is in .. or ../..
- ;;
- ;; da: FIXME: this code causes problems if the make
- ;; command fails. It should not be used by default
- ;; and should be made more robust.
- ;;
- ((compiled-file (concat (substring
- filename 0
- (string-match ".v$" filename)) ".vo"))
- (command (shell-command-to-string
- (concat "cd " dir ";"
- "make -n -W " filename " " compiled-file
- "| sed s/coqc/coqtop/"))))
- (message command)
- (setq coq-prog-args nil)
- (concat
- (substring command 0 (string-match " [^ ]*$" command))
- "-emacs"))
- coq-prog-name))))
-
;;; coq-system.el ends here
diff --git a/coq/coq.el b/coq/coq.el
index 98291f1137..d12382d4a2 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1771,6 +1771,10 @@ See `coq-fold-hyp'."
(proof-definvisible coq-unset-printing-implicit "Unset Printing Implicit.")
(proof-definvisible coq-set-printing-all "Set Printing All.")
(proof-definvisible coq-unset-printing-all "Unset Printing All.")
+(proof-definvisible coq-set-printing-parentheses "Set Printing Parentheses.")
+(proof-definvisible coq-unset-printing-parentheses "Unset Printing
Parentheses.")
+(proof-definvisible coq-set-printing-notations "Set Printing Notations.")
+(proof-definvisible coq-unset-printing-notations "Unset Printing Notations.")
(proof-definvisible coq-set-printing-synth "Set Printing Synth.")
(proof-definvisible coq-unset-printing-synth "Unset Printing Synth.")
(proof-definvisible coq-set-printing-coercions "Set Printing Coercions.")
@@ -1901,7 +1905,6 @@ at `proof-assistant-settings-cmds' evaluation time.")
(setq proof-assistant-home-page coq-www-home-page)
(setq proof-prog-name coq-prog-name)
- (setq proof-guess-command-line #'coq-guess-command-line)
(setq proof-prog-name-guess t)
;; We manage file saveing via coq-compile-auto-save and for coq
@@ -2508,13 +2511,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) ")."))
@@ -2715,6 +2720,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))
@@ -2869,6 +2875,10 @@ Completion is on a quasi-exhaustive list of Coq
tacticals."
(define-key coq-keymap [(control ?l)] #'coq-LocateConstant)
(define-key coq-keymap [(control ?n)] #'coq-LocateNotation)
(define-key coq-keymap [(control ?w)] #'coq-ask-adapt-printing-width-and-show)
+(define-key coq-keymap [(control ?9)] #'coq-set-printing-parentheses)
+(define-key coq-keymap [(control ?0)] #'coq-unset-printing-parentheses)
+(define-key coq-keymap [(?N)] #'coq-set-printing-notations)
+(define-key coq-keymap [(?n)] #'coq-unset-printing-notations)
;(proof-eval-when-ready-for-assistant
; (define-key ??? [(control c) (control a)] (proof-ass keymap)))
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index acaed36176..d7e2cc910e 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -4521,17 +4521,35 @@ Documentation of the user option
@code{coq-project-filename}:
@c TEXI DOCSTRING MAGIC: coq-project-filename
@defvar coq-project-filename
-The name of coq project file.@*
-The coq project file of a coq development (cf. Coq documentation on
-"makefile generation") should contain the arguments given to
-coq_makefile. In particular it contains the -I and -R
-options (preferably one per line). If @samp{coq-use-coqproject} is
+Variable containing the function detecting a project file.
+
+See its default value @samp{@code{coq--default-project-find-file}} for an
example.
+
+The function takes one argument, the name of a directory, and returns
+the name of a coq/rocq project file it contains if there is one. Return
+nil otherwise.
+
+This is used to detect the coq project file (using
+@samp{@code{locate-dominating-file}}). By default we accept _CoqProject and
+_RocqProject (and any case-variant of these) without checking coq/rocq
+version. If you want something smarter please redefine
+@samp{@code{coq-project-filename}} directly by using:
+
+(setq @code{coq-project-filename} #'my-own-predicate)
+
+About the coq/rocq project file (cf. Coq documentation on project files
+and "makefile generation"):
+
+The coq project file of a coq development should contain the arguments
+given to coq_makefile. In particular it contains the -I and -R
+options (preferably one per line). If @samp{coq-use-coqproject} is
t (default) the content of this file will be used by Proof General to
-infer the @samp{@code{coq-load-path}} and the @samp{@code{coq-prog-args}}
variables that set
-the coqtop invocation by Proof General. This is now the recommended
-way of configuring the coqtop invocation. Local file variables may
-still be used to override the coq project file's configuration.
-.dir-locals.el files also work and override project file settings.
+infer the @samp{@code{coq-load-path}} and the @samp{@code{coq-prog-args}}
variables that set the
+coqtop invocation by Proof General. This is now the recommended way of
+configuring the coqtop invocation. Local file variables may still be
+used to override the coq project file's configuration. .dir-locals.el
+files also work and override project file settings.
+
@end defvar
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 07e338599a..ed0703c106 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -107,7 +107,7 @@
The function could take a filename as argument, run `make -n' to see
how to compile the file non-interactively, then translate the result
into an interactive invocation of the proof assistant with the same
-command line options. For an example, see coq/coq.el."
+command line options."
:type 'function
:group 'prover-config)
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))
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 14e1ede318..159711b912 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -400,7 +400,9 @@ process command."
(append (split-string proof-rsh-command)
prog-name-list1)
prog-name-list1))
- (prog-command-line (mapconcat 'identity prog-name-list " "))
+ (prog-command-line
+ (mapconcat (lambda (arg) (concat "\"" arg "\""))
+ prog-name-list " "))
(process-connection-type
proof-shell-process-connection-type)
