From 8985fa996de0f81e9af08b3472cbb78f3bd03089 Mon Sep 17 00:00:00 2001 From: Stefan Monnier Date: Tue, 20 Sep 2022 22:52:11 -0400 Subject: [PATCH 1/4] ci/*.el: Fix compilation problems using the ELPA scripts Compilation typically failed because the files required some coq*.el file when the `coq` subdir wasn't yet in `load-path`. While at it, enable lexical-binding where still missing, and fix some warnings. * ci/simple-tests/test-prelude-correct.el: * ci/simple-tests/test-coq-par-job-needs-compilation-quick.el: * ci/compile-tests/cct-lib.el: * ci/coq-tests.el: Eval `proof-ready-for-assistant` also during compilation so that (require 'coq*) doesn't error out. * ci/coq-tests.el (coq-fixture-on-file): Avoid `not-modified` which is "interactive only". * ci/init-tests.el: Don't fail compilation if `ert-async` is absent. * ci/compile-tests/cct-lib.el: Fix compile warnings about quotes in docstrings. Prefer #' to quote function names. * ci/simple-tests/test-coq-par-job-needs-compilation-quick.el (test-coq-par-test-data-invarint): Remove unused vars `test-id` and `req-obj-result`. --- ci/compile-tests/cct-lib.el | 14 +++++++------- ci/coq-tests.el | 6 ++++-- ci/init-tests.el | 8 +++++++- .../test-coq-par-job-needs-compilation-quick.el | 13 +++++++------ ci/simple-tests/test-prelude-correct.el | 4 ++-- 5 files changed, 27 insertions(+), 18 deletions(-) diff --git a/ci/compile-tests/cct-lib.el b/ci/compile-tests/cct-lib.el index 7a5a427c9..65b295045 100644 --- a/ci/compile-tests/cct-lib.el +++ b/ci/compile-tests/cct-lib.el @@ -1,4 +1,4 @@ -;; This file is part of Proof General. +;; This file is part of Proof General. -*- lexical-binding: t; -*- ;; ;; © Copyright 2020 - 2021 Hendrik Tews ;; @@ -30,7 +30,7 @@ ;; require proof-site, otherwise proof-ready-for-assistant won't be ;; defined. (require 'proof-site) -(proof-ready-for-assistant 'coq) +(eval-and-compile (proof-ready-for-assistant 'coq)) (require 'coq-compile-common) (require 'ert) @@ -90,7 +90,7 @@ cannot be accessed." "Return an assoc list of FILES with their modification times. The modification time is an emacs time value, it's nil if file cannot be accessed." - (mapcar 'cct-record-change-time files)) + (mapcar #'cct-record-change-time files)) (defun cct-split-change-times (file-change-times files) "Split assoc list FILE-CHANGE-TIMES. @@ -162,7 +162,7 @@ Runs `cct-before-busy-waiting-hook' and PG uses a number of overlapping and non-overlapping spans (read overlays) in the asserted and queue region of the proof buffer, see the comments in generic/proof-script.el. Spans of type -vanilla (stored at 'type in the span property list) are created +vanilla (stored at `type' in the span property list) are created for real commands (not for comments). They hold various information that is used, among others, for backtracking. @@ -185,7 +185,7 @@ and `current-message' does not return anything." (defun cct-check-locked (line locked-state) "Check that line LINE has locked state LOCKED-STATE -LOCKED-STATE must be 'locked or 'unlocked. This function checks +LOCKED-STATE must be `locked' or `unlocked'. This function checks whether line LINE is inside or outside the asserted (locked) region of the buffer and signals a test failure if not." (let ((locked (eq locked-state 'locked))) @@ -216,7 +216,7 @@ region of the buffer and signals a test failure if not." (defun cct-check-files-locked (line lock-state files) "Check that all FILES at line number LINE have lock state LOCK-STATE. -LOCK-STATE must be either 'locked or 'unlocked. FILES must be +LOCK-STATE must be either `locked' or `unlocked'. FILES must be list of file names." (when cct--debug-tests (message "check files %s at line %d: %s" @@ -233,7 +233,7 @@ list of file names." The comparison treats ANCESTORS as set but the file names must be `equal' as strings. -Ancestors are recoreded in the 'coq-locked-ancestors property of +Ancestors are recoreded in the `coq-locked-ancestors' property of the vanilla spans of require commands, see the in-file documentation of coq/coq-par-compile.el." (let ((locked-ancestors diff --git a/ci/coq-tests.el b/ci/coq-tests.el index 774cc989f..38d9f5eac 100644 --- a/ci/coq-tests.el +++ b/ci/coq-tests.el @@ -12,6 +12,8 @@ (setq coq-test-dir (file-name-directory buffer-file-name)) (error "You should set 'coq-test-dir, or run coq-test.el from a file buffer."))) +;; FIXME: Merely loading a file should not have such side effects. +;; We should move that code into a function. (setq debug-on-error t) ; open the debugger on error -- may be commented-out (setq ert-batch-backtrace-right-margin 79) @@ -20,7 +22,7 @@ ;;(setq ert-async-timeout 2) ;; Load Coq instance of Proof General now. -(proof-ready-for-assistant 'coq) +(eval-and-compile (proof-ready-for-assistant 'coq)) (require 'coq) ;;; Code: @@ -155,7 +157,7 @@ then evaluate the BODY function and finally tear-down (exit Coq)." (coq-mock body)))) (coq-test-exit) (coq-set-flags nil flags) - (not-modified nil) ; Clear modification + (set-buffer-modified-p nil) ; Clear modification (kill-buffer buffer) (when rmfile (message "Removing file %s ..." rmfile)) (ignore-errors (delete-file rmfile))))) diff --git a/ci/init-tests.el b/ci/init-tests.el index ade70cce3..5a73cf108 100644 --- a/ci/init-tests.el +++ b/ci/init-tests.el @@ -7,6 +7,9 @@ ;;; Code: +;; FIXME: Merely loading a file should not have such side effects. +;; We should move all of that code into a function. + ;; Setup MELPA (require 'package) (setq gnutls-algorithm-priority "NORMAL:-VERS-TLS1.3") @@ -24,7 +27,10 @@ (unless (package-installed-p 'ert-async) (package-refresh-contents) (package-install 'ert-async)) + (eval-when-compile - (require 'ert-async)) + ;; FIXME: Why do we have this `require' and why is it within + ;; an `eval-when-compile'? + (require 'ert-async nil t)) ;;; init-tests.el ends here diff --git a/ci/simple-tests/test-coq-par-job-needs-compilation-quick.el b/ci/simple-tests/test-coq-par-job-needs-compilation-quick.el index 23018091e..d7037f73f 100644 --- a/ci/simple-tests/test-coq-par-job-needs-compilation-quick.el +++ b/ci/simple-tests/test-coq-par-job-needs-compilation-quick.el @@ -1,9 +1,9 @@ -;;; test-coq-par-job-needs-compilation-quick.el --- test compilation internals +;;; test-coq-par-job-needs-compilation-quick.el --- test compilation internals -*- lexical-binding: t; -*- ;; This file is part of Proof General. ;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh -;; Portions © Copyright 2003-2018 Free Software Foundation, Inc. +;; Portions © Copyright 2003-2022 Free Software Foundation, Inc. ;; Portions © Copyright 2001-2017 Pierre Courtieu ;; Portions © Copyright 2010, 2016 Erik Martin-Dorel ;; Portions © Copyright 2011-2013, 2016-2017 2021 Hendrik Tews @@ -33,7 +33,7 @@ ;;; Code: (require 'proof-site) -(proof-ready-for-assistant 'coq) +(eval-and-compile (proof-ready-for-assistant 'coq)) (require 'coq-par-compile) (eval-when-compile (require 'cl-lib)) @@ -756,7 +756,7 @@ relative ages.") "Wellformedness check for the test specifications." (mapc (lambda (test) - (let ((test-id (format "%s" (car test)))) + ;; (let ((test-id (format "%s" (car test)))) ;; a test is a list of 4 elements and the first element is a list itself (should (and @@ -770,7 +770,8 @@ relative ages.") (quick-mode (car variant)) (compilation-result (nth 1 variant)) (delete-result (nth 2 variant)) - (req-obj-result (nth 3 variant))) + ;; (req-obj-result (nth 3 variant)) + ) ;; the delete field, when set, must be a member of the files list (should (or (not delete-result) (member delete-result files))) @@ -780,7 +781,7 @@ relative ages.") (should (not delete-result)) (should (eq compilation-result (not (eq (car (last (car test))) 'vo))))))) - (cdr test)))) + (cdr test))) ;; ) coq--par-job-needs-compilation-tests)) (defun test-coq-par-sym-to-file (dir sym) diff --git a/ci/simple-tests/test-prelude-correct.el b/ci/simple-tests/test-prelude-correct.el index 77676d205..eb38c97f2 100644 --- a/ci/simple-tests/test-prelude-correct.el +++ b/ci/simple-tests/test-prelude-correct.el @@ -1,4 +1,4 @@ -;; This file is part of Proof General. +;; This file is part of Proof General. -*- lexical-binding: t; -*- ;; ;; © Copyright 2021 Hendrik Tews ;; @@ -21,7 +21,7 @@ ;; ;; Load stuff for `coq--version<' (require 'proof-site) -(proof-ready-for-assistant 'coq) +(eval-and-compile (proof-ready-for-assistant 'coq)) (require 'coq-system) (defconst coq--post-v810 (coq--post-v810) From d58636b4d6204992f2d7a46fb9a29d972adf27d2 Mon Sep 17 00:00:00 2001 From: Stefan Monnier Date: Tue, 20 Sep 2022 23:07:46 -0400 Subject: [PATCH 2/4] Use the new advice facility Replace all uses of `defadvice` with `advice-add`. * coq/coq.el: Remove coding cookie since .el files default to utf-8. (coq--unset-double-hit-advice): New function extracted from advice. (proof-electric-terminator-enable): Use `advice-add` instead of `defadvice`. * generic/pg-autotest.el (proof--debug-to-log): New function extracted from advice. (proof-debug): Advice with `advice-add` rather than `defadvice`. * generic/proof-syntax.el: * lib/bufhist.el: Update comments to refer to `advice-add` rather than `defadvice`. --- coq/coq.el | 9 +++++---- generic/pg-autotest.el | 11 ++++++----- generic/proof-script.el | 4 ++-- generic/proof-syntax.el | 8 ++++---- lib/bufhist.el | 14 +++++++------- 5 files changed, 24 insertions(+), 22 deletions(-) diff --git a/coq/coq.el b/coq/coq.el index 5a85bf7b9..f3dbde275 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -1,9 +1,9 @@ -;;; coq.el --- Major mode for Coq proof assistant -*- coding: utf-8; lexical-binding: t; -*- +;;; coq.el --- Major mode for Coq proof assistant -*- lexical-binding: t; -*- ;; This file is part of Proof General. ;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh -;; Portions © Copyright 2003-2021 Free Software Foundation, Inc. +;; Portions © Copyright 2003-2022 Free Software Foundation, Inc. ;; Portions © Copyright 2001-2017 Pierre Courtieu ;; Portions © Copyright 2010, 2016 Erik Martin-Dorel ;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews @@ -3363,14 +3363,15 @@ This function is called by `proof-set-value' on `coq-double-hit-enable'." (proof-deftoggle coq-double-hit-enable coq-double-hit-toggle) -(defadvice proof-electric-terminator-enable (after coq-unset-double-hit-advice) +(defun coq--unset-double-hit-advice (&rest _) "Disable double hit terminator since electric terminator is a replacement. This is an advice to pg `proof-electric-terminator-enable' function." (when (and coq-double-hit-enable proof-electric-terminator-enable) (coq-double-hit-toggle 0) (message "Hit M-1 . to enter a real \".\"."))) -(ad-activate 'proof-electric-terminator-enable) +(advice-add 'proof-electric-terminator-enable + :after #'coq--unset-double-hit-advice) (defvar coq-double-hit-delay 0.25 "The maximum delay between the two hit of a double hit in coq/proofgeneral.") diff --git a/generic/pg-autotest.el b/generic/pg-autotest.el index 2bb1d05bd..b3dc3bfd1 100644 --- a/generic/pg-autotest.el +++ b/generic/pg-autotest.el @@ -3,7 +3,7 @@ ;; This file is part of Proof General. ;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh -;; Portions © Copyright 2003-2018 Free Software Foundation, Inc. +;; Portions © Copyright 2003-2022 Free Software Foundation, Inc. ;; Portions © Copyright 2001-2017 Pierre Courtieu ;; Portions © Copyright 2010, 2016 Erik Martin-Dorel ;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews @@ -141,10 +141,11 @@ (setq debug-on-error t) ; enable in case a test goes wrong (setq proof-general-debug t) ; debug messages from PG - (defadvice proof-debug (before proof-debug-to-log (msg &rest args)) - "Output the debug message to the test log." - (apply 'pg-autotest-message msg args)) - (ad-activate 'proof-debug))) + (advice-add 'proof-debug :before #'proof--debug-to-log))) + +(defun proof--debug-to-log (msg &rest args) + "Output the debug message to the test log." + (apply #'pg-autotest-message msg args)) (defun pg-autotest-exit () "Exit Emacs returning Unix success 0 if all tests succeeded." diff --git a/generic/proof-script.el b/generic/proof-script.el index 654b9796f..c333aeb6e 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -3,7 +3,7 @@ ;; This file is part of Proof General. ;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh -;; Portions © Copyright 2003-2021 Free Software Foundation, Inc. +;; Portions © Copyright 2003-2022 Free Software Foundation, Inc. ;; Portions © Copyright 2001-2017 Pierre Courtieu ;; Portions © Copyright 2010, 2016 Erik Martin-Dorel ;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews @@ -2605,7 +2605,7 @@ assistant." (when proof-script-font-lock-keywords (setq font-lock-defaults (list '(proof-script-font-lock-keywords) - ;; see defadvice in proof-syntax + ;; see advice in proof-syntax (fboundp (proof-ass-sym font-lock-fontify-syntactically-region))))) ;; Has buffer already been processed? diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el index 51601715e..3882e709e 100644 --- a/generic/proof-syntax.el +++ b/generic/proof-syntax.el @@ -3,7 +3,7 @@ ;; This file is part of Proof General. ;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh -;; Portions © Copyright 2003-2018 Free Software Foundation, Inc. +;; Portions © Copyright 2003-2022 Free Software Foundation, Inc. ;; Portions © Copyright 2001-2017 Pierre Courtieu ;; Portions © Copyright 2010, 2016 Erik Martin-Dorel ;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews @@ -221,15 +221,15 @@ this were even more bogus...." ;; fontification function. ;; -;; (defadvice font-lock-fontify-keywords-region -;; (before font-lock-fontify-keywords-advice (beg end &optional loudly)) +;; (advice-add 'font-lock-fontify-keywords-region :before +;; #'proof--font-lock-fontify-keywords-region) +;; (defun proof--font-lock-fontify-keywords-region (beg end &optional loudly) ;; "Call proof assistant specific syntactic region fontify. ;; If it's bound, we call -font-lock-fontify-syntactically-region." ;; (when (and proof-buffer-type ;; (fboundp (proof-ass-sym font-lock-fontify-syntactically-region))) ;; (funcall (proof-ass-sym font-lock-fontify-syntactically-region) ;; beg end loudly))) -;; (ad-activate 'font-lock-fontify-keywords-region) ;; ;; Functions for doing something like "format" but with customizable diff --git a/lib/bufhist.el b/lib/bufhist.el index d7cce2d4f..485ab8e4f 100644 --- a/lib/bufhist.el +++ b/lib/bufhist.el @@ -3,7 +3,7 @@ ;; This file is part of Proof General. ;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh -;; Portions © Copyright 2003-2021 Free Software Foundation, Inc. +;; Portions © Copyright 2003-2022 Free Software Foundation, Inc. ;; Portions © Copyright 2001-2017 Pierre Courtieu ;; Portions © Copyright 2010, 2016 Erik Martin-Dorel ;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews @@ -327,11 +327,11 @@ If RINGSIZE is omitted or nil, the size defaults to ‘bufhist-ring-size’." (progn (setq before-change-functions (remq 'bufhist-before-change-function before-change-functions))) -; (ad-disable-advice 'erase-buffer 'before 'bufhist-last-advice))) +; (advice-remove 'erase-buffer #'bufhist--last))) ;; readonly history: switch to latest contents (setq before-change-functions (cons 'bufhist-before-change-function before-change-functions)))) -; (ad-enable-advice 'erase-buffer 'before 'bufhist-last-advice)))) +; (advice-add 'erase-buffer :before #'bufhist--last)))) ;; Restore the latest buffer contents before changes from elsewhere. @@ -340,10 +340,10 @@ If RINGSIZE is omitted or nil, the size defaults to ‘bufhist-ring-size’." (bufhist-switch-to-index 0)) ;; Unfortunately, erase-buffer does not call before-change-function -; (defadvice erase-buffer (before bufhist-last-advice activate) -; (if (and bufhist-mode bufhist-read-only-history) -; (bufhist-last))) -; (ad-activate-on 'erase-buffer))) +;; (advice-add 'erase-buffer :before #'bufhist--last) +;; (defun bufhist--last (&rest _) +;; (if (and bufhist-mode bufhist-read-only-history) +;; (bufhist-last))) ;;; ;;; Buttons From 6ee5a18e037d2b0b1428fe102ddc0105714d09cf Mon Sep 17 00:00:00 2001 From: Stefan Monnier Date: Tue, 20 Sep 2022 23:19:21 -0400 Subject: [PATCH 3/4] Various cosmetic changes and fix some warnings Enable `lexical-binding` when missing in the files recently modified. Fix compile warnings about quotes in docstrings. Prefer #' to quote function names. * coq/coq.el: Require `proof-syntax`, `proof-useropts`, and `proof-utils` to silence some compiler warnings. (action, string): Move dynbound declaration to a smaller scope in `coq-preprocessing`. (coq-set-state-infos, coq-grab-punctuation-left): Fit docstring within 80 columns. (coq-diffs--setter, coq-diffs): Move `coq-diffs` var before first use. (coq-shell-theorem-dependency-list-regexp) (coq-dependency-menu-system-specific) (coq-dependencies-system-specific): Move vars before their first use. (coq-proof-tree-insert-evar-command): Simplify with `or`. (coq-preprocessing): Declare `action` and `string` locally to be dynbound. (coq-highlight-span-dependencies): Remove unused var `proof-pos`. : Remove second coding cookie since .el files default to utf-8. * generic/pg-autotest.el: Use `lexical-binding`. (pg-autotest-test-script-randomjumps): Remove unused var `random-edit`. (pg-autotest-test-eval): Use lexical binding. * generic/proof-script.el (proof-colour-locked, proof-setup-imenu) (proof-colour-locked-span, proof-script-delete-spans) (proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window): Fit docstring within 80 columns. * generic/proof-syntax.el: Use `lexical-binding`. (proof-replace-regexp-in-string, proof-re-search-forward) (proof-re-search-backward, proof-re-search-forward-safe): Fit docstring within 80 columns. (proof-format): Use lexical binding. * doc/PG-adapting.texi: (Auto)Update accordingly. --- coq/coq.el | 144 +++++++++++++++++++++------------------- doc/PG-adapting.texi | 4 +- generic/pg-autotest.el | 12 ++-- generic/proof-script.el | 61 +++++++++-------- generic/proof-syntax.el | 14 ++-- 5 files changed, 122 insertions(+), 113 deletions(-) diff --git a/coq/coq.el b/coq/coq.el index f3dbde275..5b378606b 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -32,15 +32,17 @@ (require 'cl-lib) (require 'span) +(require 'proof-syntax) +(require 'proof-useropts) +(require 'proof-utils) (eval-when-compile (require 'proof-utils) (require 'span) (require 'outline) (require 'newcomment) (require 'etags)) + (defvar proof-info) ; dynamic scope in proof-tree-urgent-action -(defvar action) ; dynamic scope in coq-insert-as stuff -(defvar string) ; dynamic scope in coq-insert-as stuff (defvar old-proof-marker) (defvar coq-keymap) (defvar coq-one-command-per-line) @@ -177,7 +179,7 @@ It is mostly useful in three window mode, see also `proof-three-window-mode-policy' for details." :type 'boolean - :safe 'booleanp + :safe #'booleanp :group 'coq-auto-compile) ;; @@ -591,11 +593,11 @@ and read by function `coq-empty-action-list-command'.") (span-set-property span 'statenum val)) (defsubst coq-get-span-goalcmd (span) - "Return the 'goalcmd flag of the SPAN." + "Return the `goalcmd' flag of the SPAN." (span-property span 'goalcmd)) (defsubst coq-set-span-goalcmd (span val) - "Set the 'goalcmd flag of the SPAN to VAL." + "Set the `goalcmd' flag of the SPAN to VAL." (span-set-property span 'goalcmd val)) (defsubst coq-set-span-proofnum (span val) @@ -625,7 +627,7 @@ and read by function `coq-empty-action-list-command'.") (defun coq-set-state-infos () "Set the last locked span's state number to the number found last time. -This number is in the *last but one* prompt (variable `coq-last-but-one-statenum'). +This number is in the *last but one* prompt (var `coq-last-but-one-statenum'). If locked span already has a state number, then do nothing. Also updates `coq-last-but-one-statenum' to the last state number for next time." (if proof-shell-last-prompt @@ -815,7 +817,7 @@ If C is nil, return nil." (or (equal (char-syntax c) ?\.) (equal (char-syntax c) ?\_)))) (defun coq-grab-punctuation-left (pos) - "Return a string made of punctuations chars found immediately before position POS." + "Return the punctuation chars found immediately before position POS." (let ((res nil) (currpos pos)) (while (coq-is-symbol-or-punct (char-before currpos)) @@ -931,7 +933,7 @@ Otherwise propose identifier at point if any." (defun coq-command-with-set-unset (setcmd cmd unsetcmd &optional postformatcmd testcmd) "Play commands SETCMD then CMD and then silently UNSETCMD. -The last UNSETCMD is performed with tag 'empty-action-list so that it +The last UNSETCMD is performed with tag `empty-action-list' so that it does not trigger ‘proof-shell-empty-action’ (which does \"Show\" at the time of writing this documentation)." (let* ((postform (if (eq postformatcmd nil) 'identity postformatcmd)) @@ -1119,7 +1121,7 @@ With flag Printing All if some prefix arg is given (C-u)." (coq-ask-do-show-all "Check" "Check")) (defun coq-get-response-string-at (&optional pt) - "Go forward from PT until reaching a 'response property, and return it. + "Go forward from PT until reaching a `response' property, and return it. Response span only starts at first non space character of a command, so we may have to go forward to find it. Starts from (point) if pt is nil. Precondition: pt (or point if nil) @@ -1183,6 +1185,27 @@ Printing All set." (add-hook 'proof-assert-command-hook #'coq-adapt-printing-width) (add-hook 'proof-retract-command-hook #'coq-reset-printing-width) +(defun coq-diffs--setter (symbol new-value) + ":set function fo `coq-diffs'. +Set Diffs setting if Coq is running and has a version >= 8.10." + (set symbol new-value) + (if (proof-shell-available-p) + (let ((cmd (coq-diffs))) + (if (equal cmd "") + (message "Ignore coq-diffs setting %s for Coq before 8.10" + (symbol-name coq-diffs)) + (proof-shell-invisible-command cmd))))) + +(defcustom coq-diffs 'off + "Controls Coq Diffs option" + :type '(radio + (const :tag "Don't show diffs" off) + (const :tag "Show diffs: only added" on) + (const :tag "Show diffs: added and removed" removed)) + :safe (lambda (v) (member v '(off on removed))) + :set #'coq-diffs--setter + :group 'coq) + (defun coq--show-proof-stepwise-cmds () (when coq-show-proof-stepwise (if (coq--post-v811) @@ -1202,7 +1225,7 @@ Printing All set." (defun coq-empty-action-list-command (cmd) "Return the list of commands to send to Coq after CMD if it is the last command of the action list. -If CMD is tagged with 'empty-action-list then this function won't +If CMD is tagged with `empty-action-list' then this function won't be called and no command will be sent to Coq. Note: the last command added if `coq-show-proof-stepwise' is set should match the `coq-show-proof-diffs-regexp'." @@ -1959,6 +1982,41 @@ at `proof-assistant-settings-cmds' evaluation time.") (proof-config-done) ) +;; This variable is used by generic pg code. Every time this is detected in the +;; output, it sets the `proof-last-theorem-dependencies' variable. Substring 1 +;; should contain the name of the theorem, and substring 2 should contain its +;; dependencies. The content of `proof-last-theorem-dependencies' is then used +;; by pg generic code to trigger `proof-depends-process-dependencies', which +;; itself sets the 'dependencies property of the span, and calls +;; `proof-dependencies-system-specific'. The latter is bound to +;; `coq-dependencies-system-specific' below. +(defconst coq-shell-theorem-dependency-list-regexp + "\n?The proof of \\(?1:[^ \n]+\\)\\(?: \\|\n\\)should start with one of the following commands:\\(?: \\|\n\\)Proof using\\(?2:[^.]*\\)\\.") + + +;; the additional menu for "proof using". highlights the "Proof." command, and +;; have a entry to insert the annotation and remove the highlight. +(defvar coq-dependency-menu-system-specific + (lambda (span) + (let* ((deps (span-property-safe span 'dependencies)) + (specialspans (spans-at-region-prop (span-start span) (span-end span) 'proofusing)) + (specialspan (and specialspans (not (cdr specialspans)) (car specialspans))) + (suggested (mapconcat #'identity deps " ")) + (suggested (coq-hack-proofusing-suggestion suggested)) + (name (concat " insert \"proof using " suggested "\"")) + (fn (lambda (sp) + (coq-insert-proof-using-suggestion sp t) + (and specialspan (span-delete specialspan))))) + (list "-------------" (vector name `(,fn ,span) t)))) + "Coq specific additional menu entry for \"Proof using\". +annotation. See `proof-dependency-menu-system-specific'." ) + +(defvar coq-dependencies-system-specific + (lambda (span) + (coq-insert-proof-using-suggestion span)) + "Coq specific dependency mechanism. +Used for automatic insertion of \"Proof using\" annotations.") + (defun coq-shell-mode-config () (setq proof-shell-cd-cmd coq-shell-cd @@ -2113,27 +2171,6 @@ Return the empty string if the version of Coq < 8.10." (format "Set Diffs \"%s\". " (symbol-name coq-diffs)) "")) -(defun coq-diffs--setter (symbol new-value) - ":set function fo `coq-diffs'. -Set Diffs setting if Coq is running and has a version >= 8.10." - (set symbol new-value) - (if (proof-shell-available-p) - (let ((cmd (coq-diffs))) - (if (equal cmd "") - (message "Ignore coq-diffs setting %s for Coq before 8.10" - (symbol-name coq-diffs)) - (proof-shell-invisible-command cmd))))) - -(defcustom coq-diffs 'off - "Controls Coq Diffs option" - :type '(radio - (const :tag "Don't show diffs" off) - (const :tag "Show diffs: only added" on) - (const :tag "Show diffs: added and removed" removed)) - :safe (lambda (v) (member v '(off on removed))) - :set #'coq-diffs--setter - :group 'coq) - ;; Obsolete: ;;(defpacustom undo-depth coq-default-undo-limit ;; "Depth of undo history. Undo behaviour will break beyond this size." @@ -2217,7 +2254,7 @@ Show commands before the next real proof command. The ID's of the open goals are checked with `proof-tree-sequent-hash' in order to find out if they are new. For any new goal an appropriate Show Goal command with a -'proof-tree-show-subgoal flag is inserted into +`proof-tree-show-subgoal' flag is inserted into `proof-action-list'. Then, in the normal delayed output processing, the sequent text is send to prooftree as a sequent update (see `proof-tree-update-sequent') and the ID of the @@ -2336,7 +2373,7 @@ fact in `coq--proof-tree-must-disable-evars'." "Insert an evar printing command at the head of `proof-action-list'." (push (proof-shell-action-list-item (concat cmd " Printing Dependent Evars Line.") - (if callback callback 'proof-done-invisible) + (or callback #'proof-done-invisible) (list 'invisible)) proof-action-list)) @@ -2406,8 +2443,10 @@ result of `coq-proof-tree-get-proof-info'." (defun coq-bullet-p (s) (string-match coq-bullet-regexp-nospace s)) -;; Remark: `action' and `string' are known by `proof-shell-insert-hook' (defun coq-preprocessing () + ;; Remark: `action' and `string' are known by `proof-shell-insert-hook' + (defvar action) ; dynamic scope in coq-insert-as stuff + (defvar string) ; dynamic scope in coq-insert-as stuff (when coq-time-commands (with-no-warnings ;; NB: dynamic scoping of `string' and `action' ;; Don't add the prefix if this is a command sent internally @@ -2620,17 +2659,6 @@ Warning: this makes the error messages (and location) wrong.") ;; already performed.). -;; This variable is used by generic pg code. Every time this is detected in the -;; output, it sets the `proof-last-theorem-dependencies' variable. Substring 1 -;; should contain the name of the theorem, and substring 2 should contain its -;; dependencies. The content of `proof-last-theorem-dependencies' is then used -;; by pg generic code to trigger `proof-depends-process-dependencies', which -;; itself sets the 'dependencies property of the span, and calls -;; `proof-dependencies-system-specific'. The latter is bound to -;; `coq-dependencies-system-specific' below. -(defconst coq-shell-theorem-dependency-list-regexp - "\n?The proof of \\(?1:[^ \n]+\\)\\(?: \\|\n\\)should start with one of the following commands:\\(?: \\|\n\\)Proof using\\(?2:[^.]*\\)\\.") - (defcustom coq-accept-proof-using-suggestion 'highlight "Whether and how proofgeneral should insert \"Proof using\" suggestions. Suggestions are emitted by Coq at Qed time. The possible values @@ -2674,23 +2702,6 @@ Remarks and limitations: (defun coq-hack-proofusing-suggestion (suggested) (if (string-equal "" suggested) "Type" suggested)) -;; the additional menu for "proof using". highlights the "Proof." command, and -;; have a entry to insert the annotation and remove the highlight. -(defvar coq-dependency-menu-system-specific - (lambda (span) - (let* ((deps (span-property-safe span 'dependencies)) - (specialspans (spans-at-region-prop (span-start span) (span-end span) 'proofusing)) - (specialspan (and specialspans (not (cdr specialspans)) (car specialspans))) - (suggested (mapconcat #'identity deps " ")) - (suggested (coq-hack-proofusing-suggestion suggested)) - (name (concat " insert \"proof using " suggested "\"")) - (fn (lambda (sp) - (coq-insert-proof-using-suggestion sp t) - (and specialspan (span-delete specialspan))))) - (list "-------------" (vector name `(,fn ,span) t)))) - "Coq specific additional menu entry for \"Proof using\". -annotation. See `proof-dependency-menu-system-specific'." ) - (defconst coq-proof-using-regexp "\\_ if that is defined, otherwise it calls @samp{@code{proof-looking-at-syntactic-context}}. @end defun @@ -3665,7 +3665,7 @@ user option @samp{@code{proof-auto-action-when-deactivating-scripting}}. If @samp{@code{proof-no-fully-processed-buffer}} is t there is only the choice to fully retract the active scripting buffer. In this case the active scripting buffer is retracted even if it was fully processed. -Setting @samp{@code{proof-auto-action-when-deactivating-scripting}} to @code{'process} +Setting @samp{@code{proof-auto-action-when-deactivating-scripting}} to @samp{process} is ignored in this case. If the scripting buffer is (or has become) fully processed, and it is diff --git a/generic/pg-autotest.el b/generic/pg-autotest.el index b3dc3bfd1..b4c47c4aa 100644 --- a/generic/pg-autotest.el +++ b/generic/pg-autotest.el @@ -1,4 +1,4 @@ -;;; pg-autotest.el --- Simple testing framework for Proof General +;;; pg-autotest.el --- Simple testing framework for Proof General -*- lexical-binding: t; -*- ;; This file is part of Proof General. @@ -39,7 +39,7 @@ "Flag indicating overall successful state of tests.") (defvar pg-autotest-log t - "Value for 'standard-output' during tests.") + "Value for `standard-output' during tests.") ;;; Some utilities @@ -106,7 +106,7 @@ (defun pg-autotest-message (msg &rest args) "Give message MSG (formatted using ARGS) in log file output and on display." - (let ((fmsg (if args (apply 'format msg args) msg))) + (let ((fmsg (if args (apply #'format msg args) msg))) (proof-with-current-buffer-if-exists pg-autotest-log (insert fmsg "\n")) @@ -117,7 +117,7 @@ (pg-autotest-message "\n\nREMARK: %s\n" msg)) (defun pg-autotest-timestart (&optional clockname) - "Make a note of current time, named 'local or CLOCKNAME." + "Make a note of current time, named `local' or CLOCKNAME." (put 'pg-autotest-time (or clockname 'local) (current-time))) @@ -208,7 +208,7 @@ completely processing the buffer as the last step." (pg-autotest-find-file-restart file) (while (> jumps 0) (let* ((random-point (random (point-max))) - (random-edit nil) ; (< 20 (random 100))) + ;; (random-edit nil) ; (< 20 (random 100))) (random-thing (random 10))) (cond ((and (eq random-thing 0) @@ -277,7 +277,7 @@ completely processing the buffer as the last step." (defun pg-autotest-test-eval (body) "Evaluate given expression for side effect." - (eval body)) + (eval body t)) (defun pg-autotest-test-quit-prover () "Exit prover process." diff --git a/generic/proof-script.el b/generic/proof-script.el index c333aeb6e..6600b9060 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -315,14 +315,16 @@ Also clear list of script portions." ;;;###autoload (defun proof-colour-locked () - "Alter the colour of all locked regions according to variable `proof-colour-locked'." + "Alter the colour of all locked regions. +Obeys the variable `proof-colour-locked'." (interactive) (proof-map-buffers (proof-buffers-in-mode proof-mode-for-script) (and (span-live-p proof-locked-span) (proof-colour-locked-span)))) (defun proof-colour-locked-span () - "Alter the colour of the locked region according to variable `proof-colour-locked'." + "Alter the colour of the locked region. +Obeys the variable `proof-colour-locked'." (if proof-colour-locked (span-set-property proof-locked-span 'face 'proof-locked-face) (span-set-property proof-locked-span 'face nil))) @@ -381,7 +383,7 @@ value of proof-locked span." "Remove the queue span from buffer, cleaning spans no longer queued. If BADSPAN is non-nil, assume that this was the span whose command caused the error. Go to the start of it if `proof-follow-mode' is -'locked. +`locked'. If INTERRUPTP is non-nil, do not consider BADSPAN itself as faulty. @@ -404,14 +406,15 @@ This is a subroutine used in proof-shell-handle-{error,interrupt}." (proof-script-delete-spans start end))) (defun proof-script-delete-spans (beg end) - "Delete primary spans between BEG and END. Secondary 'pghelp spans are left." + "Delete primary spans between BEG and END. +Secondary `pghelp' spans are left." (span-delete-spans beg end 'type) (span-delete-spans beg end 'idiom) (span-delete-spans beg end 'pg-span) ) (defun proof-script-delete-secondary-spans (beg end) - "Delete secondary spans between BEG and END (currently, 'pghelp spans)." + "Delete secondary spans between BEG and END (currently, `pghelp' spans)." (span-delete-spans beg end 'pghelp)) @@ -515,7 +518,7 @@ If called interactively, a mark is set at the current location with `push-mark'" "If the end of the locked region is not visible, jump to the end of it. A possible hook function for `proof-shell-handle-error-or-interrupt-hook'. Does nothing if there is no active scripting buffer, or if -`proof-follow-mode' is set to 'ignore." +`proof-follow-mode' is set to `ignore'." (interactive) (if (and proof-script-buffer (not (eq proof-follow-mode 'ignore))) @@ -523,7 +526,8 @@ Does nothing if there is no active scripting buffer, or if (proof-goto-end-of-locked t)))) (defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window () - "As `proof-goto-end-of-locked-if-pos-not-visible-in-window', but not for interrupts. + "As `proof-goto-end-of-locked-if-pos-not-visible-in-window', +but not for interrupts. Intended as a hook function for `proof-shell-handle-error-or-interrupt-hook'." (interactive) (unless (eq proof-follow-mode 'ignore) @@ -595,7 +599,7 @@ will be recorded as a textual name used instead of ID for users; NAME does not need to be unique. NAME is a name that comes from the proof script or prover output. -It is recorded in the span with the 'rawname property." +It is recorded in the span with the `rawname' property." (cl-assert (symbolp idiomsym)) (cl-assert (stringp id)) (if name (cl-assert (stringp name))) @@ -633,12 +637,12 @@ It is recorded in the span with the 'rawname property." (defun pg-invisible-prop (idiom) "Return an invisibility symbol for the given IDIOM. -This is a value for the overlay 'invisible property." +This is a value for the overlay `invisible' property." (intern (concat "pg-" (symbol-name (or idiom 'other))))) (defun pg-set-element-span-invisible (span invisiblep) "Function to adjust visibility of SPAN to INVISIBLEP. -We use list values of the 'invisible property which contain +We use list values of the `invisible' property which contain private symbols, that should play well with other conforming modes and `buffer-invisibility-spec'." (let* ((invisible-prop (pg-invisible-prop (span-property span 'idiom))) @@ -712,13 +716,13 @@ IDIOMSYM is a symbol and ID is a strings." "Return a user-level name for SPAN. This is based on its name and type. -Each span has a 'type property, one of: +Each span has a `type' property, one of: - 'goalsave A goal..savegoal region in the buffer, a completed proof. - 'vanilla Initialised in proof-semis-to-vanillas, for - 'comment A comment outside a command. - 'proverproc A region closed by the prover, processed outwith PG - 'pbp A PBP command inserted automatically into the script." + `goalsave' A goal..savegoal region in the buffer, a completed proof. + `vanilla' Initialised in proof-semis-to-vanillas, for + `comment' A comment outside a command. + `proverproc' A region closed by the prover, processed outwith PG + `pbp' A PBP command inserted automatically into the script." (let ((type (span-property span 'type)) (idiom (span-property span 'idiom)) (rawname (span-property span 'rawname))) @@ -773,7 +777,7 @@ This is used to annotate the buffer with the result of proof steps." The daughter span covers the non whitespace content of the main span. We add the last output (when non-empty) to the hover display, and -also as the 'response property on the span. +also as the `response' property on the span. Optional argument MOUSEFACE means use the given face as a mouse highlight face, if it is a face, otherwise, if it is non-nil but not a face, @@ -782,7 +786,7 @@ do not add a mouse highlight. In any case, a mouse highlight and tooltip are only set if `proof-output-tooltips' is non-nil. -Argument FACE means add 'face property FACE to the span." +Argument FACE means add `face' property FACE to the span." (let* ((output (pg-last-output-displayform)) (new-start (save-excursion (goto-char (span-start span)) @@ -1077,7 +1081,7 @@ Otherwise retract it. Errors are ignored" (defun proof-deactivate-scripting-query-user-action () "Display the script and query the user for a deactivate action. -Returns 'retract, 'process or finally nil if user declined." +Returns `retract', `process' or finally nil if user declined." ;; Would be nicer to ask a single question, but ;; a nuisance to define our own dialogue since it ;; doesn't really fit with one of the standard ones. @@ -1120,7 +1124,7 @@ Returns 'retract, 'process or finally nil if user declined." nil))))) (defun proof-deactivate-scripting-choose-action () - "Select a deactivation action, 'process, 'retract or nil." + "Select a deactivation action, `process', `retract' or nil." (let ((auto-action (if (and proof-no-fully-processed-buffer (eq proof-auto-action-when-deactivating-scripting @@ -1147,7 +1151,7 @@ user option `proof-auto-action-when-deactivating-scripting'. If `proof-no-fully-processed-buffer' is t there is only the choice to fully retract the active scripting buffer. In this case the active scripting buffer is retracted even if it was fully processed. -Setting `proof-auto-action-when-deactivating-scripting' to 'process +Setting `proof-auto-action-when-deactivating-scripting' to `process' is ignored in this case. If the scripting buffer is (or has become) fully processed, and it is @@ -1379,9 +1383,9 @@ Argument SPAN has just been processed. This is the callback for all the normal commands. Besides stuff that is not yet documented here, this function - extends the locked region -- creates additional spans (without 'type property) for help, +- creates additional spans (without `type' property) for help, tooltips, color and menus -- merges spans with 'type as needed to achieve atomic undo for +- merges spans with `type' as needed to achieve atomic undo for proofs and sections - enters some commands and their spans in some database (with for me unknown purpose)" @@ -1478,10 +1482,10 @@ that is not yet documented here, this function "Retire commands that close a proof or some other region. This is a subroutine of `proof-done-advancing'. Besides stuff that is not yet documented here, this function -- creates additional spans (without 'type property) for help, +- creates additional spans (without `type' property) for help, tooltips, color and menus - in particular, adds the background color for omitted proofs -- merges spans with 'type as needed to achieve atomic undo for +- merges spans with `type' as needed to achieve atomic undo for proofs and sections; for Coq this is done at least for proofs and sections. - enters some commands and their spans in some database (with for @@ -1737,7 +1741,7 @@ them by type. Return a list of lists of the form where: - TYPE is a symbol indicating the type of text found, either 'cmd or 'comment; + TYPE is a symbol indicating the type of text found, either `cmd' or `comment'; TEXT is the string content taken from the buffer; ENDPOS is the position of the final character of the text. @@ -2009,7 +2013,7 @@ omit proofs feature. This function uses `proof-script-definition-end-regexp' to search for complete opaque proofs in the action list VANILLAS. Complete opaque proofs are replaced by `proof-script-proof-admit-command'. The span of -the admit command contains an 'omitted-proof-region property with +the admit command contains an `omitted-proof-region' property with the region of the omitted proof. This is used in `proof-done-advancing-save' to colour the omitted proof with `proof-omitted-proof-face'. @@ -2873,7 +2877,8 @@ Choice of function depends on configuration setting." (error "Configuration error: must set `proof-terminal-string' or one of its friends"))))) (defun proof-setup-imenu () - "Setup a default for imenu, perhaps using `proof-script-imenu-generic-expression'." + "Setup a default for imenu, +perhaps using `proof-script-imenu-generic-expression'." (unless ;; already setup, leave it alone (and (boundp 'imenu-generic-expression) imenu-generic-expression) diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el index 3882e709e..543170e54 100644 --- a/generic/proof-syntax.el +++ b/generic/proof-syntax.el @@ -1,4 +1,4 @@ -;;; proof-syntax.el --- Functions for dealing with syntax +;;; proof-syntax.el --- Functions for dealing with syntax -*- lexical-binding: t; -*- ;; This file is part of Proof General. @@ -66,22 +66,22 @@ nil if a region cannot be found." ;;;###autoload (defun proof-replace-regexp-in-string (regexp rep string) - "Like ‘replace-regexp-in-string’, but set ‘case-fold-search’ to ‘proof-case-fold-search’." + "‘replace-regexp-in-string’ obeying ‘proof-case-fold-search’." (let ((case-fold-search proof-case-fold-search)) (replace-regexp-in-string regexp rep string))) (defsubst proof-re-search-forward (regexp &optional bound noerror count) - "Like ‘re-search-forward’, but set ‘case-fold-search’ to ‘proof-case-fold-search’." + "‘re-search-forward’ obeying ‘proof-case-fold-search’." (let ((case-fold-search proof-case-fold-search)) (re-search-forward regexp bound noerror count))) (defsubst proof-re-search-backward (regexp &optional bound noerror count) - "Like ‘re-search-backward’, but set ‘case-fold-search’ to ‘proof-case-fold-search’." + "‘re-search-backward’ obeying ‘proof-case-fold-search’." (let ((case-fold-search proof-case-fold-search)) (re-search-backward regexp bound noerror count))) (defsubst proof-re-search-forward-safe (regexp &optional bound noerror count) - "Like ‘re-search-forward’, but set ‘case-fold-search’ to ‘proof-case-fold-search’." + "‘re-search-forward’ obeying ‘proof-case-fold-search’." (and regexp (let ((case-fold-search proof-case-fold-search)) (re-search-forward regexp bound noerror count)))) @@ -148,7 +148,7 @@ The returned value is one of the following symbols: (defun proof-looking-at-syntactic-context () "Determine if current point is at beginning or within comment/string context. -If so, return a symbol indicating this ('comment or 'string). +If so, return a symbol indicating this (`comment' or `string'). This function invokes if that is defined, otherwise it calls `proof-looking-at-syntactic-context'." (if (fboundp (proof-ass-sym syntactic-context)) @@ -249,7 +249,7 @@ may be a string or sexp evaluated to get a string." ((stringp (cdr (car alist))) (cdr (car alist))) (t - (eval (cdr (car alist))))))) + (eval (cdr (car alist)) t))))) (setq string (concat (substring string 0 (match-beginning 0)) replacement From e71b59e007af469d9de34646062d9d163fa30d39 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Mon, 28 Nov 2022 15:23:11 +0100 Subject: [PATCH 4/4] test: Clarify ci/{init-tests.el,coq-tests.el} --- ci/coq-tests.el | 10 +++------- ci/init-tests.el | 8 ++------ 2 files changed, 5 insertions(+), 13 deletions(-) diff --git a/ci/coq-tests.el b/ci/coq-tests.el index 38d9f5eac..327962d97 100644 --- a/ci/coq-tests.el +++ b/ci/coq-tests.el @@ -6,14 +6,15 @@ ;;; Eval this to run the tests interactively ;; ;; (progn (load-file "coq-tests.el") (call-interactively #'ert)) +;; +;; Note that loading this file triggers some side effects, such as: +;; (setq debug-on-error t) (unless (and (boundp 'coq-test-dir) coq-test-dir) ; if set by ./test.sh (if buffer-file-name (setq coq-test-dir (file-name-directory buffer-file-name)) (error "You should set 'coq-test-dir, or run coq-test.el from a file buffer."))) -;; FIXME: Merely loading a file should not have such side effects. -;; We should move that code into a function. (setq debug-on-error t) ; open the debugger on error -- may be commented-out (setq ert-batch-backtrace-right-margin 79) @@ -366,10 +367,5 @@ Tactic failure: Cannot solve this goal.")))) (coq-test-goto-before "(*proof*)") (backward-char 3) (should (span-at (point) 'proofusing)))))) - - - - -(provide 'coq-tests) ;;; coq-tests.el ends here diff --git a/ci/init-tests.el b/ci/init-tests.el index 5a73cf108..3ba416183 100644 --- a/ci/init-tests.el +++ b/ci/init-tests.el @@ -7,9 +7,6 @@ ;;; Code: -;; FIXME: Merely loading a file should not have such side effects. -;; We should move all of that code into a function. - ;; Setup MELPA (require 'package) (setq gnutls-algorithm-priority "NORMAL:-VERS-TLS1.3") @@ -29,8 +26,7 @@ (package-install 'ert-async)) (eval-when-compile - ;; FIXME: Why do we have this `require' and why is it within - ;; an `eval-when-compile'? - (require 'ert-async nil t)) + ;; This `require' command is just an "installation unit test". + (require 'ert-async)) ;;; init-tests.el ends here