diff options
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-abbrev.el | 77 | ||||
| -rw-r--r-- | coq/coq-compile-common.el | 341 | ||||
| -rw-r--r-- | coq/coq-db.el | 14 | ||||
| -rw-r--r-- | coq/coq-indent.el | 16 | ||||
| -rw-r--r-- | coq/coq-par-compile.el | 1493 | ||||
| -rw-r--r-- | coq/coq-par-test.el | 953 | ||||
| -rw-r--r-- | coq/coq-seq-compile.el | 67 | ||||
| -rw-r--r-- | coq/coq-smie.el | 63 | ||||
| -rw-r--r-- | coq/coq-syntax.el | 635 | ||||
| -rw-r--r-- | coq/coq-system.el | 147 | ||||
| -rw-r--r-- | coq/coq.el | 293 | ||||
| -rwxr-xr-x[-rw-r--r--] | coq/coqtags | 0 |
12 files changed, 3225 insertions, 874 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 3f8662e7..534c013d 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -148,6 +148,67 @@ It was constructed with `proof-defstringset-fn'.") :style toggle :selected coq-double-hit-enable :help "Automatically send commands when terminator typed twiced quickly."] + ("Auto Compilation" + ["Compile Before Require" + coq-compile-before-require-toggle + :style toggle + :selected coq-compile-before-require + :help "Check dependencies of required modules and compile on the fly."] + ["Parallel background compilation" + coq-compile-parallel-in-background-toggle + :style toggle + :selected coq-compile-parallel-in-background + :active coq-compile-before-require + :help ,(concat "Compile parallel in background or " + "sequentially with blocking ProofGeneral.")] + ["Keep going" + coq-compile-keep-going-toggle + :style toggle + :selected coq-compile-keep-going + :active (and coq-compile-before-require + coq-compile-parallel-in-background) + :help ,(concat "Continue background compilation after " + "the first error as far as possible")] + ["no quick" + (customize-set-variable 'coq-compile-quick 'no-quick) + :style radio + :selected (eq coq-compile-quick 'no-quick) + :active (and coq-compile-before-require + coq-compile-parallel-in-background) + :help "Compile without -quick but accept existion .vio's"] + ["quick no vio2vo" + (customize-set-variable 'coq-compile-quick 'quick-no-vio2vo) + :style radio + :selected (eq coq-compile-quick 'quick-no-vio2vo) + :active (and coq-compile-before-require + coq-compile-parallel-in-background) + :help "Compile with -quick, accept existing .vo's, don't run vio2vo"] + ["quick and vio2vo" + (customize-set-variable 'coq-compile-quick 'quick-and-vio2vo) + :style radio + :selected (eq coq-compile-quick 'quick-and-vio2vo) + :active (and coq-compile-before-require + coq-compile-parallel-in-background) + :help "Compile with -quick, accept existing .vo's, run vio2vo later"] + ["ensure vo" + (customize-set-variable 'coq-compile-quick 'ensure-vo) + :style radio + :selected (eq coq-compile-quick 'ensure-vo) + :active (and coq-compile-before-require + coq-compile-parallel-in-background) + :help "Ensure only vo's are used for consistency"] + ["Confirm External Compilation" + coq-confirm-external-compilation-toggle + :style toggle + :selected coq-confirm-external-compilation + :active (and coq-compile-before-require + (not (equal coq-compile-command ""))) + :help "Confirm external compilation command, see `coq-compile-command'."] + ["Abort Background Compilation" + coq-par-emergency-cleanup + :active (and coq-compile-before-require + coq-compile-parallel-in-background) + :help "Abort background compilation and kill all compilation processes."]) "" ["Print..." coq-Print :help "With prefix arg (C-u): Set Printing All first"] ["Check..." coq-Check :help "With prefix arg (C-u): Set Printing All first"] @@ -189,16 +250,18 @@ It was constructed with `proof-defstringset-fn'.") ["Print Scope/Visibility..." coq-PrintScope t]) ("OPTIONS" ["Set Printing All" coq-set-printing-all t] - ["UnSet Printing All" coq-unset-printing-all t] - ["Set Implicit Argument" coq-set-implicit-arguments t] - ["Unset Implicit Argument" coq-unset-implicit-arguments t] - ["Set Printing Width" coq-ask-adapt-printing-width-and-show t] - ["Set Printing Synth" coq-set-printing-synth t] - ["Unset Printing Synth" coq-unset-printing-synth t] + ["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 Coercions" coq-set-printing-coercions t] ["Unset Printing Coercions" coq-unset-printing-coercions t] + ["Set Printing Synth" coq-set-printing-synth t] + ["Unset Printing Synth" coq-unset-printing-synth t] + ["Set Printing Universes" coq-set-printing-universes t] + ["Unset Printing Universes" coq-unset-printing-universes t] ["Set Printing Wildcards" coq-set-printing-wildcards t] - ["Unset Printing Wildcards" coq-unset-printing-wildcards t]) + ["Unset Printing Wildcards" coq-unset-printing-wildcards t] + ["Set Printing Width" coq-ask-adapt-printing-width-and-show t]) "" ["ML4PG" (coq-activate-ml4pg) :help "Activates ML4PG: machine-learning methods for Proof General"] )) diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index 415f65ee..af3e70a4 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -18,6 +18,7 @@ (eval-when (compile) ;;(defvar coq-pre-v85 nil) + (require 'compile) (defvar coq-confirm-external-compilation nil); defpacustom (defvar coq-compile-parallel-in-background nil) ; defpacustom (proof-ready-for-assistant 'coq)) ; compile for coq @@ -92,11 +93,38 @@ Must be used together with `coq-par-enable'." ncpus nil))) -(defvar coq-internal-max-jobs 1 +(defvar coq--max-background-vio2vo-percentage-shadow 40 + "Internal shadow value of `coq-max-background-vio2vo-percentage'. +This variable does always contain the same value as +`coq-max-background-vio2vo-percentage'. It is used only to break +the dependency cycle between `coq-set-max-vio2vo-jobs' and +`coq-max-background-vio2vo-percentage'.") + +(defvar coq--internal-max-vio2vo-jobs 1 + "Internal number of vio2vo jobs. +This is the internal value, use +`coq-max-background-vio2vo-percentage' to configure.") + +(defvar coq--internal-max-jobs 1 "Value of `coq-max-background-compilation-jobs' translated to a number.") +(defun coq-set-max-vio2vo-jobs () + "Set `coq--internal-max-vio2vo-jobs'." + (setq coq--internal-max-vio2vo-jobs + (max 1 + (round (* coq--internal-max-jobs + coq--max-background-vio2vo-percentage-shadow + 0.01))))) + +(defun coq-max-vio2vo-setter (symbol new-value) + ":set function for `coq-max-background-vio2vo-percentage'. +SYMBOL should be 'coq-max-background-vio2vo-percentage" + (set symbol new-value) + (setq coq--max-background-vio2vo-percentage-shadow new-value) + (coq-set-max-vio2vo-jobs)) + (defun coq-max-jobs-setter (symbol new-value) - ":set function for `coq-max-background-compilation-jobs. + ":set function for `coq-max-background-compilation-jobs'. SYMBOL should be 'coq-max-background-compilation-jobs" (set symbol new-value) (cond @@ -106,7 +134,20 @@ SYMBOL should be 'coq-max-background-compilation-jobs" (setq new-value 1))) ((and (integerp new-value) (> new-value 0)) t) (t (setq new-value 1))) - (setq coq-internal-max-jobs new-value)) + (setq coq--internal-max-jobs new-value) + (coq-set-max-vio2vo-jobs)) + +(defun coq-compile-quick-setter (symbol new-value) + ":set function for `coq-compile-quick' for pre 8.5 compatibility. +Ignore any quick setting for Coq versions before 8.5." + (cond + ((or (eq new-value 'ensure-vo) (eq new-value 'no-quick)) + t) + ((coq--pre-v85) + (message "Ignore coq-compile-quick setting %s for Coq before 8.5" + new-value) + (setq new-value 'no-quick))) + (set symbol new-value)) ;;; user options and variables @@ -123,7 +164,7 @@ required library module and its dependencies are up-to-date. If not, they are compiled from the sources before the \"Require\" command is processed. This option can be set/reset via menu -`Coq -> Settings -> Compile Before Require'." +`Coq -> Auto Compilation -> Compile Before Require'." :type 'boolean :safe 'booleanp :group 'coq-auto-compile) @@ -140,7 +181,7 @@ the background. The maximal number of parallel compilation jobs is set with `coq-max-background-compilation-jobs'. This option can be set/reset via menu -`Coq -> Settings -> Compile Parallel In Background'." +`Coq -> Auto Compilation -> Compile Parallel In Background'." :type 'boolean :safe 'booleanp :group 'coq-auto-compile @@ -149,13 +190,100 @@ This option can be set/reset via menu ;; defpacustom fails to call :eval during inititialization, see trac #456 (coq-switch-compilation-method) +(defcustom coq-compile-quick 'no-quick + "Control quick compilation, vio2vo and vio/vo files auto compilation. +This option controls whether ``-quick'' is used for parallel +background compilation and whether up-date .vo or .vio files are +used or deleted. Please use the customization system to change +this option to ensure that any ``-quick'' setting is ignored for +Coq before 8.5. + +Note that ``-quick'' can be noticebly slower when your sources do +not declare section variables with ``Proof using''. Note that +even if you do declare section variables, ``-quick'' is typically +slower on small files. + +Use the default `no-quick', if you have not yet switched to +``Proof using''. Use `quick-no-vio2vo', if you want quick +recompilation without producing .vo files. Value +`quick-and-vio2vo' updates missing prerequisites with ``-quick'' +and starts vio2vo conversion on a subset of the availables +cores (see `coq-compile-vio2vo-percentage') when the quick +recompilation finished (but see below for a .vio .vo +incompatibility caveat). Note that all the previously described +modes might load .vio files and that you therefore might not +notice certain universe inconsistencies. Finally, use `ensure-vo' +for only importing .vo files with complete universe checks. + +Detailed description of the 4 modes: + +no-quick Compile outdated prerequisites without ``-quick'', + producing .vo files, but don't compile prerequisites + for which an up-to-date .vio file exists. Delete + or overwrite outdated .vo files. + +quick-no-vio2vo Compile outdated prerequisites with ``-quick'', + producing .vio files, but don't compile prerequisites + for which an up-to-date .vo file exists. Delete + or overwrite outdated .vio files. + +quick-and-vio2vo Same as `quick-no-vio2vo', but start vio2vo processes + after the last ``Require'' command has been processed + to convert the vio dependencies into vo files. With this + mode you might see asynchronous errors from vio2vo + compilation while you are processing stuff far below the + last require. vio2vo compilation is done on a subset of + the available cores, see `coq-compile-vio2vo-percentage'. + When `coq-compile-keep-going' is set, vio2vo compilation + is scheduled for those files for which coqc compilation + was successful. + + Warning: This mode does only work when you process require + commands in batches. Slowly single-stepping through require's + might lead to inconsistency errors when loading some + libraries, see Coq issue #5223. + +ensure-vo Ensure that all library dependencies are present as .vo + files and delete outdated .vio files or .vio files that + are more recent than the corresponding .vo file. This + setting is the only one that ensures soundness." + :type + '(radio + (const :tag "don't use -quick but accept existing vio files" no-quick) + (const :tag "use -quick, don't do vio2vo" quick-no-vio2vo) + (const :tag "use -quick and do vio2vo" quick-and-vio2vo) + (const :tag "ensure vo compilation, delete vio files" ensure-vo)) + :safe (lambda (v) (member v '(no-quick quick-no-vio2vo + quick-and-vio2vo ensure-vo))) + :set 'coq-compile-quick-setter + :group 'coq-auto-compile) + +(defun coq-compile-prefer-quick () + "Return t if a .vio file would be prefered." + (or + (eq coq-compile-quick 'quick-no-vio2vo) + (eq coq-compile-quick 'quick-and-vio2vo))) + +(defcustom coq-compile-keep-going t + "Continue compilation after the first error as far as possible. +Similar to ``make -k'', with this option enabled, the background +compilation continues after the first error as far as possible. +With this option disabled, background compilation is +immediately stopped after the first error. + +This option can be set/reset via menu +`Coq -> Auto Compilation -> Keep going'.") + +;; define coq-compile-keep-going-toggle +(proof-deftoggle coq-compile-keep-going) + (defcustom coq-max-background-compilation-jobs 'all-cpus "Maximal number of parallel jobs, if parallel compilation is enabled. Use the number of available CPU cores if this is set to 'all-cpus. This variable is the user setting. The value that is -really used is `coq-internal-max-jobs'. Use `coq-max-jobs-setter' +really used is `coq--internal-max-jobs'. Use `coq-max-jobs-setter' or the customization system to change this variable. Otherwise -your change will have no effect, because `coq-internal-max-jobs' +your change will have no effect, because `coq--internal-max-jobs' is not adapted." :type '(choice (const :tag "use all CPU cores" all-cpus) (integer :tag "fixed number" :value 1)) @@ -163,6 +291,24 @@ is not adapted." :set 'coq-max-jobs-setter :group 'coq-auto-compile) +(defcustom coq-max-background-vio2vo-percentage 40 + "Percentage of `coq-max-background-vio2vo-percentage' for vio2vo jobs. +This setting configures the maximal number of vio2vo background +jobs (if you set `coq-compile-quick' to 'quick-and-vio2vo) as +percentage of `coq-max-background-compilation-jobs'." + :type 'number + :safe 'numberp + :set 'coq-max-vio2vo-setter + :group 'coq-auto-compile) + +(defcustom coq-compile-vio2vo-delay 2.5 + "Delay in seconds for the vio2vo compilation. +This delay helps to avoid running into a library inconsistency +with 'quick-and-vio2vo, see Coq issue #5223." + :type 'number + :safe 'numberp + :group 'coq-auto-compile) + (defcustom coq-compile-command "" "External compilation command. If empty ProofGeneral compiles itself. If unset (the empty string) ProofGeneral computes the dependencies of @@ -266,23 +412,14 @@ of the regular expressions in this list then ProofGeneral does neither compile this file nor check its dependencies for compilation. It makes sense to include non-standard coq library directories here if they are not changed and if they are so big -that dependency checking takes noticeable time." +that dependency checking takes noticeable time. The regular +expressions in here are always matched against the .vo file name, +regardless whether ``-quick'' would be used to compile the file +or not." :type '(repeat regexp) :safe (lambda (v) (every 'stringp v)) :group 'coq-auto-compile) -(defcustom coq-compile-ignore-library-directory t - "If non-nil, ProofGeneral does not compile modules from the coq library. -Should be `t' for normal coq users. If `nil' library modules are -compiled if their sources are newer. - -This option has currently no effect, because Proof General uses -coqdep to translate qualified identifiers into library file names -and coqdep does not output dependencies in the standard library." - :type 'boolean - :safe 'booleanp - :group 'coq-auto-compile) - (defcustom coq-coqdep-error-regexp (concat "^\\*\\*\\* Warning: in file .*, library .* is required " "and has not been found") @@ -300,12 +437,6 @@ the latter condition into an error, then set this variable to :safe 'stringp :group 'coq-auto-compile) -(defconst coq-require-command-regexp - "^Require[ \t\n]+\\(Import\\|Export\\)?[ \t\n]*" - "Regular expression matching Require commands in Coq. -Should match \"Require\" with its import and export variants up to (but not -including) the first character of the first required module. The required -modules are matched separately with `coq-require-id-regexp'") (defconst coq-require-id-regexp "[ \t\n]*\\([A-Za-z0-9_']+\\(\\.[A-Za-z0-9_']+\\)*\\)[ \t\n]*" @@ -315,14 +446,22 @@ white space. The module identifier must be matched with group number 1. Note that the trailing dot in \"Require A.\" is not part of the module identifier and should therefore not be matched by this regexp.") +(defconst coq-require-command-regexp + (concat "^\\(?:From[ \t\n]+\\(?1:[A-Za-z0-9_']+\\(?:\\.[A-Za-z0-9_']+\\)*\\)" + "[ \t\n]*\\)?" + "\\(?2:Require[ \t\n]+\\(?:Import\\|Export\\)?\\)[ \t\n]*") + "Regular expression matching Require commands in Coq. +Should match \"Require\" with its import and export variants up to (but not +including) the first character of the first required module. The required +modules are matched separately with `coq-require-id-regexp'") + (defvar coq-compile-history nil "History of external Coq compilation commands.") -(defvar coq-compile-response-buffer "*coq-compile-response*" +(defvar coq--compile-response-buffer "*coq-compile-response*" "Name of the buffer to display error messages from coqc and coqdep.") - -(defvar coq-debug-auto-compilation nil +(defvar coq--debug-auto-compilation nil "*Display more messages during compilation") @@ -330,11 +469,11 @@ identifier and should therefore not be matched by this regexp.") (defun time-less-or-equal (time-1 time-2) "Return `t' if time value time-1 is earlier or equal to time-2. -A time value is a list of two integers as returned by `file-attributes'. -The first integer contains the upper 16 bits and the second the lower -16 bits of the time." - (or (time-less-p time-1 time-2) - (equal time-1 time-2))) +A time value is a list of two, three or four integers of the +form (high low micro pico) as returned by `file-attributes' or +'current-time'. First element high contains the upper 16 bits and +the second low the lower 16 bits of the time." + (not (time-less-p time-2 time-1))) (defun coq-max-dep-mod-time (dep-mod-times) "Return the maximum in DEP-MOD-TIMES. @@ -357,52 +496,53 @@ DEP-MOD-TIMES is empty it returns nil." max)) -;;; Compute command line for starting coqtop - - - - - ;;; ignore library files (defun coq-compile-ignore-file (lib-obj-file) "Check whether ProofGeneral should handle compilation of LIB-OBJ-FILE. Return `t' if ProofGeneral should skip LIB-OBJ-FILE and `nil' if -ProofGeneral should handle the file. For normal users it does, for instance, -not make sense to let ProofGeneral check if the coq standard library -is up-to-date." - (or - (and - coq-compile-ignore-library-directory - (eq (compare-strings coq-library-directory 0 nil - lib-obj-file 0 (length coq-library-directory)) - t) - (if coq-debug-auto-compilation - (message "Ignore lib file %s" lib-obj-file)) - t) - (if (some - (lambda (dir-regexp) (string-match dir-regexp lib-obj-file)) - coq-compile-ignored-directories) - (progn - (if coq-debug-auto-compilation - (message "Ignore %s" lib-obj-file)) - t) - nil))) - -;;; convert .vo files to .v files - -(defun coq-library-src-of-obj-file (lib-obj-file) +ProofGeneral should handle the file. For normal users it does, +for instance, not make sense to let ProofGeneral check if the coq +standard library is up-to-date. This function is always invoked +on the .vo file name, regardless whether the file would be +compiled with ``-quick'' or not." + (if (some + (lambda (dir-regexp) (string-match dir-regexp lib-obj-file)) + coq-compile-ignored-directories) + (progn + (when coq--debug-auto-compilation + (message "Ignore %s" lib-obj-file)) + t) + nil)) + +;;; convert .vo files to .v files and module names + +(defun coq-module-of-src-file (src-file) + "Return the module name for SRC-FILE. +SRC-FILE must be a .v file." + (let ((file (file-name-nondirectory src-file))) + (substring file 0 (max 0 (- (length file) 2))))) + +(defun coq-library-src-of-vo-file (lib-obj-file) "Return source file name for LIB-OBJ-FILE. Chops off the last character of LIB-OBJ-FILE to convert \"x.vo\" to \"x.v\"." (substring lib-obj-file 0 (- (length lib-obj-file) 1))) +(defun coq-library-vio-of-vo-file (vo-obj-file) + "Return .vio file name for VO-OBJ-FILE. +Changes the suffix from .vio to .vo. VO-OBJ-FILE must have a .vo suffix." + (concat (coq-library-src-of-vo-file vo-obj-file) "io")) + ;;; ancestor unlocking ;;; (locking is different for sequential and parallel compilation) (defun coq-unlock-ancestor (ancestor-src) "Unlock ANCESTOR-SRC." - (let* ((true-ancestor (file-truename ancestor-src))) + (let* ((default-directory + (buffer-local-value 'default-directory + (or proof-script-buffer (current-buffer)))) + (true-ancestor (file-truename ancestor-src))) (setq proof-included-files-list (delete true-ancestor proof-included-files-list)) (proof-restart-buffers (proof-files-to-buffers (list true-ancestor))))) @@ -413,22 +553,37 @@ Chops off the last character of LIB-OBJ-FILE to convert \"x.vo\" to \"x.v\"." (span-set-property span 'coq-locked-ancestors ())) -;;; manage coq-compile-respose-buffer - -(defun coq-init-compile-response-buffer (command) +;;; manage coq--compile-response-buffer + +(defun coq-compile-display-error (command error-message display) + "Display COMMAND and ERROR-MESSAGE in `coq--compile-response-buffer'. +If needed, reinitialize `coq--compile-response-buffer'. Then +display COMMAND and ERROR-MESSAGE." + (unless (buffer-live-p (get-buffer coq--compile-response-buffer)) + (coq-init-compile-response-buffer)) + (let ((inhibit-read-only t) + (deactivate-mark nil)) + (with-current-buffer coq--compile-response-buffer + (save-excursion + (goto-char (point-max)) + (insert command "\n" error-message "\n")))) + (when display + (coq-display-compile-response-buffer))) + +(defun coq-init-compile-response-buffer (&optional command) "Initialize the buffer for the compilation output. -If `coq-compile-response-buffer' exists, empty it. Otherwise -create a buffer with name `coq-compile-response-buffer', put +If `coq--compile-response-buffer' exists, empty it. Otherwise +create a buffer with name `coq--compile-response-buffer', put it into `compilation-mode' and store it in -`coq-compile-response-buffer' for later use. Argument COMMAND is +`coq--compile-response-buffer' for later use. Argument COMMAND is the command whose output will appear in the buffer." - (let ((buffer-object (get-buffer coq-compile-response-buffer))) + (let ((buffer-object (get-buffer coq--compile-response-buffer))) (if buffer-object (let ((inhibit-read-only t)) (with-current-buffer buffer-object (erase-buffer))) (setq buffer-object - (get-buffer-create coq-compile-response-buffer)) + (get-buffer-create coq--compile-response-buffer)) (with-current-buffer buffer-object (compilation-mode) ;; read-only-mode makes compilation fail if some messages need @@ -441,17 +596,47 @@ the command whose output will appear in the buffer." ;; the first line are not found for some reason ... (let ((inhibit-read-only t)) (with-current-buffer buffer-object - (insert "-*- mode: compilation; -*-\n\n" command "\n"))))) + (insert "-*- mode: compilation; -*-\n\n") + (when command + (insert command "\n")))))) (defun coq-display-compile-response-buffer () - "Display the errors in `coq-compile-response-buffer'." - (with-current-buffer coq-compile-response-buffer + "Display the errors in `coq--compile-response-buffer'." + (with-current-buffer coq--compile-response-buffer ;; fontification enables the error messages (let ((font-lock-verbose nil)) ; shut up font-lock messages (font-lock-fontify-buffer))) ;; Make it so the next C-x ` will use this buffer. - (setq next-error-last-buffer (get-buffer coq-compile-response-buffer)) - (proof-display-and-keep-buffer coq-compile-response-buffer 1 t)) + (setq next-error-last-buffer (get-buffer coq--compile-response-buffer)) + (proof-display-and-keep-buffer coq--compile-response-buffer 1 t) + ;; Partial fix for #54: ensure that the compilation response + ;; buffer is not in a dedicated window. + (mapc (lambda (w) (set-window-dedicated-p w nil)) + (get-buffer-window-list coq--compile-response-buffer nil t))) + + +;;; enable next-error to find vio2vo errors +;; +;; compilation-error-regexp-alist-alist is an alist mapping symbols to +;; what is expected for compilation-error-regexp-alist. This is +;; element of the form (REGEXP FILE [LINE COLUMN TYPE HYPERLINK +;; HIGHLIGHT...]). If REGEXP matches, the FILE'th subexpression gives +;; the file name, and the LINE'th subexpression gives the line number. +;; The COLUMN'th subexpression gives the column number on that line, +;; see the documentation of compilation-error-regexp-alist. +;; +;; Need to wrap adding the vio2vo error regex in eval-after-load, +;; because compile is loaded on demand and might not be present when +;; the user visits the first Coq file. + +(eval-after-load 'compile + '(progn + (push + '(coq-vio2vo + "File \\(.*\\): proof of [^:]*\\(: chars \\([0-9]*\\)-\\([0-9]*\\)\\)?" + 1 nil 3) + compilation-error-regexp-alist-alist) + (push 'coq-vio2vo compilation-error-regexp-alist))) ;;; save some buffers diff --git a/coq/coq-db.el b/coq/coq-db.el index 631df56d..0d9c0a6e 100644 --- a/coq/coq-db.el +++ b/coq/coq-db.el @@ -305,11 +305,21 @@ See `coq-syntax-db' for DB structure." "Face for unicode binders, by default a bold version of `font-lock-type-face'." :group 'proof-faces) +(defface coq-symbol-face + '((t :inherit default-face :bold coq-bold-unicode-binders)) + "Face for unicode binders, by default a bold version of `font-lock-type-face'." + :group 'proof-faces) + (defface coq-question-mark-face '((t :inherit font-lock-variable-name-face)) "Face for Ltac binders and evars." :group 'proof-faces) +(defface coq-context-qualifier-face + '((t :inherit font-lock-preprocessor-face :weight bold)) + "Face used for `ltac:', `constr:', and `uconstr:' headers." + :group 'proof-faces) + (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") @@ -322,6 +332,10 @@ Required so that 'coq-cheat-face is a proper facename") "Expression that evaluates to a face. 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") + (defconst coq-question-mark-face 'coq-question-mark-face) diff --git a/coq/coq-indent.el b/coq/coq-indent.el index fddfc373..e5179390 100644 --- a/coq/coq-indent.el +++ b/coq/coq-indent.el @@ -96,8 +96,8 @@ detect if they start something or not." (not (proof-string-match "{\\s-*\\(wf\\|measure\\)" str))))))) -(defconst coq-simple-cmd-ender-regexp "[^.]\\|\\=\\|\\.\\." - "Used internally. Matches the allow prefix of the coq \".\" command ending.") +(defconst coq-simple-cmd-ender-prefix-regexp "[^.]\\|\\=\\|\\.\\." + "Used internally. Matches the allowed prefixes of coq \".\" command ending.") (defconst coq-bullet-regexp-nospace "\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+" "Matches single bullet, WARNING: Lots of false positive. @@ -109,14 +109,14 @@ No context checking.") ;; bullets and curlys and spaces). This is used when search backward. ;; This variable is the regexp of possible prefixes (defconst coq-bullet-prefix-regexp - (concat "\\(?:\\(?:" coq-simple-cmd-ender-regexp "\\)" + (concat "\\(?:\\(?:" coq-simple-cmd-ender-prefix-regexp "\\)" "\\(?:\\.\\)\\(?:\\s-\\)\\(?:\\s-\\|{\\|}\\|-\\|+\\|\\*\\)*\\)")) ;; matches regular command end (. and ... followed by a space or buffer end) ;; ". " and "... " are command endings, ".. " is not, same as in ;; proof-script-command-end-regexp in coq.el (defconst coq-period-end-command - (concat "\\(?:\\(?2:" coq-simple-cmd-ender-regexp "\\)\\(?1:\\.\\)\\(?3:\\s-\\|\\'\\)\\)") + (concat "\\(?:\\(?2:" coq-simple-cmd-ender-prefix-regexp "\\)\\(?1:\\.\\)\\(?3:\\s-\\|\\'\\)\\)") "Matches coq regular syntax for ending a command (except bullets and curlies). This should match EXACTLY command ending syntax. No false @@ -194,10 +194,14 @@ command ended by the bullet-like regexp is empty. This is done in coq-smie.el, and see `coq-end-command-regexp-backward' for a more precise regexp (but only when searching backward).") +; Order here is significant, when two pattern match with the same +; starting position, the first regexp is preferred. period-command is +; the shorter one so let us have it at the end, but what about cury vs +; bullets? (defconst coq-end-command-regexp-backward (concat coq-bullet-end-command-backward "\\|" - coq-period-end-command "\\|" - coq-curlybracket-end-command-backward) + coq-curlybracket-end-command-backward "\\|" + coq-period-end-command) "Matches end of commands, including bullets and curlies. There are 3 substrings (2 and 3 may be nil): diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el index 5c37c382..8901a008 100644 --- a/coq/coq-par-compile.el +++ b/coq/coq-par-compile.el @@ -63,6 +63,7 @@ ;; 1- where to put the Require command and the items that follow it ;; 2- make sure ancestors are properly locked ;; 3- error reporting +;; 4- using -quick and the handling of .vo/.vio prerequisites ;; ;; For 1- where to put the Require command and the items that follow it: ;; @@ -84,12 +85,15 @@ ;; back into proof-action-list only if all top-level jobs of those ;; modules that are required before it are finished. ;; -;; A problem occurs with "Require b a.", where b depends on a. To -;; avoid cycles in the dependency graph, here the top-level -;; compilation job for "a" will be a so-called clone of the real -;; compilation job. The Require item is stored with the clone. The -;; real job has dependency links to all its clones. Every clone waits -;; until its real job has finished. +;; A problem occurs with "Require a. Require a.", where two different +;; action list pieces must be stored with the job for a. The solution +;; here is to clone the original job when it is needed more than one +;; time. This cloning is done in general and not only for top-level +;; jobs. So also when a.v and b.v both depend on c.v, the second +;; dependency link is managed by a clone of the job for c.v. Every +;; real job has dependency links to all its clones. All clones wait +;; until the original job has finished. (In retrospect it seems a +;; design without clone jobs might have been cleaner.) ;; ;; For 2- make sure ancestors are properly locked: ;; @@ -100,27 +104,62 @@ ;; when only "Require a." is retracted. ;; ;; The problem is solved with the 'coq-locked-ancestors property of -;; spans that contain Require commands and with the -;; coq-par-ancestor-files hash. Ancestors in the 'coq-locked-ancestors -;; property are unlocked when this span is retracted. As locking is -;; done eagerly (as soon as coqdep runs first on the file), I only -;; have to make sure the right files appear in 'coq-locked-ancestors. +;; spans that contain Require commands. Ancestors in the +;; 'coq-locked-ancestors property are unlocked when this span is +;; retracted. As locking is done eagerly (as soon as coqdep runs first +;; on the file), I only have to make sure the right files appear in +;; 'coq-locked-ancestors. ;; -;; Ancestor files accumulate in compilation jobs when the compilation -;; walks upwards the dependency tree. In the end, every top-level job -;; contains a list of all its direct and indirect ancestors. Because -;; of eager locking, all its ancestors are already locked, when a -;; top-level job is about to be retired. The coq-par-ancestor-files -;; hash therefore records whether some ancestor does already appear in -;; the 'coq-locked-ancestors property of some span before the current -;; one. If it doesn't, I store it in the current span. +;; Ancestors accumulate in compilation jobs when the compilation walks +;; upwards the dependency tree. In the end, every top-level job +;; contains a list of all its direct and indirect ancestors in its +;; 'ancestors property. Because of eager locking, all its ancestors +;; are already locked, when a top-level job is about to be retired. +;; Every job records in his 'locked propery whether the file +;; corresponding to this job has been registered in some +;; 'coq-locked-ancestors property already. ;; ;; For 3- error reporting: ;; -;; For now, all compilation jobs are killed on the first error. All -;; items that are not yet asserted are retract. This is done with -;; signalling an error and calling `coq-par-emergency-cleanup' in the -;; sentinel, if there was an error. +;; Depending on `coq-compile-keep-going' compilation can continue +;; after an error or stop immediately. For stopping immediately, +;; processing is aborted with a signal that eventually leads to +;; `coq-par-emergency-cleanup', which kills all compilation jobs, +;; retracts the queue region and resets all internal data. +;; +;; For `coq-compile-keep-going', the failing job and all dependants +;; are marked as 'failed. Queue dependants are marked with +;; 'queue-failed. These marked jobs continue with their normal state +;; transition, but omit certain steps (eg., running coqc). The first +;; tricky part is how to unlock ancestors. When marking jobs as +;; failed, their ancestors (and thereby also the files for the jobs +;; themselves) are unlocked, unless they are still participating in an +;; ongoing compilation. If a coqc compilation finishes and all +;; dependants are marked as failed, ancestors are also unlocked in the +;; same way. If a top-level job is marked as 'queue-failed, its +;; ancestors are unlocked when this job finishes coqc compilation. +;; +;; The second tricky part is how to delete the queue region. For that +;; the last top-level job is delayed until proof-action-list is empty. +;; Then the whole queue is deleted. +;; +;; For 4- using -quick and the handling of .vo/.vio prerequisites +;; +;; Coq accepts both .vo and .vio files for importing modules +;; regardless of it is running with -quick or not. However, it is +;; unclear which file is loaded when both, .vo and .vio, of a +;; dependency are present. Therefore I delete a .vio file when I +;; decide to rebuild a .vo file and vica versa. coqdep delivers +;; dependencies for both, .vio and .vo files. These dependencies are +;; identical for .vio and vo (last checked for coq trunk in October +;; 2016). For deciding whether prerequisites must be recompiled the +;; full path returned form coqdep is relevant. Because it seems odd to +;; store a full path without a .vo or .vio suffix I decided to always +;; store the .vo object file name in the 'vo-file property of +;; compilation jobs. Only when all dependencies are ready, in +;; `coq-par-job-needs-compilation' I decide whether to build a .vio or +;; .vo file and if already present .vo or .vio files must be deleted. +;; Only at that point the relevant property 'required-obj-file is set. ;; ;; ;; Properties of compilation jobs @@ -128,10 +167,18 @@ ;; 'name - some unique string, only used for debugging ;; 'queueitems - holds items from proof-action-list on ;; top-level jobs -;; 'obj-file - the .vo that this job has to make up-to-date -;; 'obj-mod-time - modification time of the .vo file, stored +;; 'vo-file - the .vo file for the module that this job has +;; to make up-to-date. This slot is filled when the +;; job is created and independent of whether a .vio +;; or .vo file must be made up-to-date. +;; 'required-obj-file - contains the .vio or .vo to be produced or nil +;; if that has not yet been decided. Does also contain +;; nil if no file needs to be rebuild at all. +;; 'obj-mod-time - modification time of 'required-obj-file, stored ;; here, to avoid double stat calls; -;; contains 'obj-does-not-exist in case .vo is absent +;; contains 'obj-does-not-exist in case that file is absent +;; 'use-quick - t if `coq-par-job-needs-compilation' decided to use +;; -quick ;; 'type - the type of the job, either 'clone or 'file ;; for real compilation jobs ;; 'state - the state of the job, see below @@ -158,11 +205,22 @@ ;; 'src-file - the .v file name ;; 'load-path - value of coq-load-path, propagated to all ;; dependencies -;; 'ancestor-files - list of ancestors, including the source file -;; of this job -;; 'require-span - present for top-level jobs only, there it +;; 'ancestors - list of ancestor jobs, for real compilation jobs +;; this list includes the job itself; may contain +;; duplicates +;; 'lock-state - nil for clone jobs, 'unlocked if the file +;; corresponding to job is not locked, 'locked if that +;; file has been locked, 'asserted if it has been +;; registered in some span in the 'coq-locked-ancestors +;; property already +;; 'require-span - present precisely for top-level jobs only, there it ;; contains the span that must finally store the ;; ancestors +;; 'vio2vo-needed - t if a subsequent vio2vo process is required to +;; build the .vo file. Otherwiese nil. +;; 'failed - t if coqdep or coqc for the job or one dependee failed. +;; 'queue-failed - t if some direct or indirect queue dependee is +;; marked 'failed ;; 'visited - used in the dependency cycle detection to mark ;; visited jobs ;; @@ -178,9 +236,10 @@ ;; finish ;; 'enqueued-coqc - coqc is running, or the job is enqueued, ;; waiting for a slot to start coqc -;; 'waiting-queue - the job is waiting until all top-level queue -;; dependencies finish (if there are any) -;; 'ready - ready +;; 'waiting-queue - coqc is finished and the job is waiting until +;; all top-level queue dependencies finish (if +;; there are any) +;; 'ready - ready, the .vo file might be missing though ;; ;; ;; State transition for clone jobs @@ -210,16 +269,8 @@ ;; 'coq-process-command - the command for error reporting ;; (as string list) ;; 'coq-par-process-killed - t if this process has been killed -;; -;; -;; Symbols in the coq-par-ancestor-files hash -;; -;; This hash maps file names to symbols. A file is present in the -;; hash, if it has been locked. -;; -;; 'locked - the file is not yet stored in the -;; 'coq-locked-ancestors property of some span -;; 'asserted - the file has been stored in some span +;; 'coq-process-rm - if not nil, a file to be deleted when +;; the process is killed ;; ;; ;; To print the states of the compilation jobs for debugging, eval @@ -237,7 +288,7 @@ ;; (mapc (lambda (p) (when (eq (get p 'type) 'clone) ;; (push p clones))) ;; (get v 'coqc-dependants))) -;; coq-compilation-object-hash) +;; coq--compilation-object-hash) ;; (mapc (lambda (v) ;; (message "%s type %s for %s state %s dep of %s queue dep of %s" ;; (get v 'name) @@ -251,41 +302,47 @@ ;;; Variables -(defvar coq-par-ancestor-files nil - "Hash remembering the state of locked ancestor files. -This hash maps true file names (in the sense of `file-truename') -to either 'locked or 'asserted. - -'locked means that this ancestor file has been locked -already (because it appeared in the dependency tree somewhere and -coqdep has been started on it) but has not been assigned to the -'coq-locked-ancestors property of some span. That is, 'locked -ancestors are not an ancestor of any required module in the -asserted region. - -'asserted means that this ancestor is the ancestor of some -asserted required module (and is in some 'coq-locked-ancestors -property).") - -(defvar coq-current-background-jobs 0 +(defvar coq--current-background-jobs 0 "Number of currently running background jobs.") -(defvar coq-compilation-object-hash nil +(defvar coq--compilation-object-hash nil "Hash for storing the compilation jobs. -The hash will only store real compilation jobs and no clones. -They are stored in order to avoid double compilation. The jobs -stored in here are uninterned symbols that carry all important +This hash only stores real compilation jobs and no clones. They +are stored in order to avoid double compilation. The jobs stored +in here are uninterned symbols that carry all important information in their property list. See the documentation in the -source file \"coq-par-compile.el\"") +source file \"coq-par-compile.el\". The hash always maps .vo file +names to compilation jobs, regardless of ``-quick''.") -(defvar coq-last-compilation-job nil +(defvar coq--last-compilation-job nil "Pointer to the last top-level compilation job. Used to link top-level jobs with queue dependencies.") -(defvar coq-par-next-id 1 +(defvar coq--compile-vio2vo-in-progress nil + "Set to t iff vio2vo is running in background.") + +(defvar coq--compile-vio2vo-delay-timer nil + "Holds the timer for the vio2vo delay.") + +(defvar coq--compile-vio2vo-start-id 0 + "Integer counter to detect races for `coq-par-require-processed'. +Assume compilation for the last top-level ``Require'' command +finishes but executing the ``Require'' takes so long that the +user can assert a next ``Require'' and that the second +compilation finishes before the first ``Require'' has been +processed. In this case there are two `coq-par-require-processed' +callbacks active, of which the first one must be ignored. For +each new callback this counter is incremented and when there is a +difference the call to `coq-par-require-processed' is ignored.") + +(defvar coq--par-next-id 1 "Increased for every job and process, to get unique job names. The names are only used for debugging.") +(defvar coq--par-delayed-last-job nil + "Inform the cycle detection that there is a delayed top-level job. +If t, there is a delayed top-level job (for which the compilation failed).") + ;;; utility functions @@ -324,45 +381,73 @@ latter greater then everything else." (t (time-less-p time-1 time-2)))) (defun coq-par-init-compilation-hash () - "(Re-)Initialize `coq-compilation-object-hash'." - (setq coq-compilation-object-hash (make-hash-table :test 'equal))) + "(Re-)Initialize `coq--compilation-object-hash'." + (setq coq--compilation-object-hash (make-hash-table :test 'equal))) -(defun coq-par-init-ancestor-hash () - "(Re-)Initialize `coq-par-ancestor-files'" - (setq coq-par-ancestor-files (make-hash-table :test 'equal)) - (mapc - (lambda (locked-anc) - (puthash locked-anc 'asserted coq-par-ancestor-files)) - proof-included-files-list)) +;;; generic queues +;; Standard implementation with two lists. +(defun coq-par-new-queue () + "Create a new empty queue." + (cons nil nil)) -;;; job queue +(defun coq-par-enqueue (queue x) + "Insert x in queue QUEUE." + (push x (car queue))) -(defun coq-par-new-compilation-queue () - "Create a new empty queue for `coq-par-compilation-queue'" - (cons nil nil)) +(defun coq-par-dequeue (queue) + "Dequeue the next item from QUEUE." + (let ((res (pop (cdr queue)))) + (unless res + (setcdr queue (nreverse (car queue))) + (setcar queue nil) + (setq res (pop (cdr queue)))) + res)) -(defvar coq-par-compilation-queue (coq-par-new-compilation-queue) - "Queue of compilation jobs with in and out end. -Use `coq-par-enqueue' and `coq-par-dequeue' to access the queue.") -(defun coq-par-enqueue (job) +;;; job queue + +(defvar coq-par-compilation-queue (coq-par-new-queue) + "Queue of compilation jobs that wait for a free core to get started. +Use `coq-par-job-enqueue' and `coq-par-job-dequeue' to access the +queue.") + +(defun coq-par-job-enqueue (job) "Insert job in the queue of waiting compilation jobs." - (push job (car coq-par-compilation-queue)) - (if coq-debug-auto-compilation - (message "%s: enqueue job in waiting queue" (get job 'name)))) + (coq-par-enqueue coq-par-compilation-queue job) + (when coq--debug-auto-compilation + (message "%s: enqueue job in waiting queue" (get job 'name)))) -(defun coq-par-dequeue () +(defun coq-par-job-dequeue () "Dequeue the next job from the compilation queue." - (let ((res (pop (cdr coq-par-compilation-queue)))) - (unless res - (setq coq-par-compilation-queue - (cons nil (nreverse (car coq-par-compilation-queue)))) - (setq res (pop (cdr coq-par-compilation-queue)))) - (if coq-debug-auto-compilation - (if res - (message "%s: dequeue" (get res 'name)) - (message "compilation queue empty"))) + (let ((res (coq-par-dequeue coq-par-compilation-queue))) + (when coq--debug-auto-compilation + (if res + (message "%s: dequeue" (get res 'name)) + (message "compilation queue empty"))) + res)) + + +;;; vio2vo queue + +(defvar coq-par-vio2vo-queue (coq-par-new-queue) + "Queue of jobs that need a vio2vo process. +Use `coq-par-vio2vo-enqueue' and `coq-par-vio2vo-dequeue' to +access the queue.") + +(defun coq-par-vio2vo-enqueue (job) + "Insert JOB in the queue for vio2vo processing." + (coq-par-enqueue coq-par-vio2vo-queue job) + (when coq--debug-auto-compilation + (message "%s: enqueue job in vio2vo queue" (get job 'name)))) + +(defun coq-par-vio2vo-dequeue () + "Dequeue the next job from the vio2vo queue." + (let ((res (coq-par-dequeue coq-par-vio2vo-queue))) + (when coq--debug-auto-compilation + (if res + (message "%s: vio2vo dequeue" (get res 'name)) + (message "vio2vo queue empty"))) res)) @@ -408,6 +493,21 @@ Use `coq-par-enqueue' and `coq-par-dequeue' to access the queue.") (put 'coq-compile-error-circular-dep 'error-message "Coq compilation error: Circular dependency") +;; coq-compile-error-rm +;; +;; Signaled when we have to delete a .vio or .vo file for consistency and +;; that deletion fails. +;; +;; This error is signaled with one data item -- the file-error error +;; description. Its car is the error symbol `file-error' and the cdr are +;; the data items for this error. They seem to be a list of strings with +;; different parts of the error message. + +(put 'coq-compile-error-rm 'error-conditions + '(error coq-compile-error coq-compile-error-rm)) +(put 'coq-compile-error-rm 'error-message + "Cannot remove outdated file.") + ;;; find circular dependencies in non-ready compilation jobs @@ -440,13 +540,13 @@ If no circle is found return nil, otherwise the list of files belonging to the circle." (let (cycle result) (maphash (lambda (key job) (put job 'visited nil)) - coq-compilation-object-hash) + coq--compilation-object-hash) (maphash (lambda (key job) (when (and (not cycle) (not (get job 'visited)) (eq (get job 'state) 'waiting-dep)) (setq cycle (coq-par-find-dependency-circle-for-job job nil)))) - coq-compilation-object-hash) + coq--compilation-object-hash) (dolist (j cycle) (when (eq (get j 'type) 'file) (push (get j 'src-file) result))) @@ -464,7 +564,7 @@ load-path options to coqdep." (list lib-src-file))) (defun coq-par-coqc-arguments (lib-src-file coq-load-path) - "Compute the command line arguments for invoking coqdep on LIB-SRC-FILE. + "Compute the command line arguments for invoking coqc on LIB-SRC-FILE. Argument COQ-LOAD-PATH must be `coq-load-path' from the buffer that triggered the compilation, in order to provide correct load-path options to coqdep." @@ -473,22 +573,33 @@ load-path options to coqdep." (defun coq-par-analyse-coq-dep-exit (status output command) "Analyse output OUTPUT of coqdep command COMMAND with exit status STATUS. -Returns the list of dependencies if there is no error. Otherwise, +Returns the list of .vo dependencies if there is no error. Otherwise, writes an error message into `coq-compile-response-buffer', makes -this buffer visible and returns a string." +this buffer visible and returns a string. + +This function does always return .vo dependencies, regardless of the +value of `coq-compile-quick'. If necessary, the conversion into .vio +files must be done elsewhere." + ;; (when coq--debug-auto-compilation + ;; (message "analyse coqdep output \"%s\"" output)) (if (or (not (eq status 0)) (string-match coq-coqdep-error-regexp output)) (progn ;; display the error - (coq-init-compile-response-buffer (mapconcat 'identity command " ")) - (let ((inhibit-read-only t)) - (with-current-buffer coq-compile-response-buffer (insert output))) - (coq-display-compile-response-buffer) + (coq-compile-display-error (mapconcat 'identity command " ") output t) "unsatisfied dependencies") - (if (string-match ": \\(.*\\)$" output) - (cdr-safe (split-string (match-string 1 output))) - ()))) + ;; In 8.5, coqdep produces two lines. Match with .* here to + ;; extract only a part of the first line. + ;; We could match against (concat "^[^:]*" obj-file "[^:]*: \\(.*\\)") + ;; to select the right line for either .vo or .vio dependencies. + ;; However, we want to accept a .vo prerequisite for a .vio target + ;; if it is recent enough. Therefore we actually need module dependencies + ;; instead of file dependencies and we derive them from the .vo line. + (when (string-match "\\`[^:]*: \\(.*\\)" output) + (cl-remove-if-not + (lambda (f) (string-match-p "\\.vo\\'" f)) + (split-string (match-string 1 output)))))) (defun coq-par-get-library-dependencies (lib-src-file coq-load-path &optional command-intro) @@ -513,7 +624,10 @@ error case. It is prepended to the displayed command. LIB-SRC-FILE should be an absolute file name. If it is, the dependencies are absolute too and the simplified treatment of `coq-load-path-include-current' in `coq-include-options' won't -break." +break. + +This function always computes the .vo file names. Conversion into .vio, +depending on `coq-compile-quick', must be done elsewhere." (let* ((coqdep-arguments (coq-par-coqdep-arguments lib-src-file coq-load-path)) (this-command (cons coq-dependency-analyzer coqdep-arguments)) @@ -521,21 +635,24 @@ break." (cons command-intro this-command) this-command)) coqdep-status coqdep-output) - ;; (if coq-debug-auto-compilation - ;; (message "call coqdep arg list: %s" coqdep-arguments)) + (when coq--debug-auto-compilation + (message "Run synchronously: %s" + (mapconcat 'identity full-command " "))) + ;; (when coq--debug-auto-compilation + ;; (message "CPGLD: call coqdep arg list: %s" coqdep-arguments)) (with-temp-buffer (setq coqdep-status (apply 'call-process coq-dependency-analyzer nil (current-buffer) nil coqdep-arguments)) (setq coqdep-output (buffer-string))) - ;; (if coq-debug-auto-compilation - ;; (message "coqdep status %s, output on %s: %s" + ;; (when coq--debug-auto-compilation + ;; (message "CPGLD: coqdep status %s, output on %s: %s" ;; coqdep-status lib-src-file coqdep-output)) (coq-par-analyse-coq-dep-exit coqdep-status coqdep-output full-command))) -(defun coq-par-map-module-id-to-obj-file (module-id coq-load-path) - "Map MODULE-ID to the appropriate coq object file. +(defun coq-par-map-module-id-to-vo-file (module-id coq-load-path &optional from) + "Map MODULE-ID to the appropriate coq object (.vo) file. The mapping depends of course on `coq-load-path'. The current implementation invokes coqdep with a one-line require command. This is probably slower but much simpler than modelling coq file @@ -545,15 +662,19 @@ decent error message. Argument COQ-LOAD-PATH must be `coq-load-path' from the buffer that triggered the compilation, in order to provide correct load-path options to coqdep. +This function always computes the .vo file name. Conversion into .vio, +depending on `coq-compile-quick', must be done elsewhere. + A peculiar consequence of the current implementation is that this function returns () if MODULE-ID comes from the standard library." (let ((coq-load-path - (if coq-load-path-include-current + (if (and coq-load-path-include-current (coq--pre-v85)) (cons default-directory coq-load-path) coq-load-path)) (coq-load-path-include-current nil) (temp-require-file (make-temp-file "ProofGeneral-coq" nil ".v")) - (coq-string (concat "Require " module-id ".")) + (coq-string (concat (if from (concat "From " from " ") "") + "Require " module-id ".")) result) (unwind-protect (progn @@ -563,8 +684,10 @@ function returns () if MODULE-ID comes from the standard library." (coq-par-get-library-dependencies temp-require-file coq-load-path - (concat "echo \"" coq-string "\" > " temp-require-file)))) + (concat "echo \"" coq-string "\" > " temp-require-file ";")))) (delete-file temp-require-file)) + (when coq--debug-auto-compilation + (message "coq-par-get-library-dependencies delivered \"%s\"" result)) (if (stringp result) ;; Error handling: coq-par-get-library-dependencies was not able to ;; translate module-id into a file name. We insert now a faked error @@ -587,14 +710,15 @@ function returns () if MODULE-ID comes from the standard library." ;; (coq-seq-display-compile-response-buffer) (error error-message))) (assert (<= (length result) 1) - "Internal error in coq-seq-map-module-id-to-obj-file") + nil "Internal error in coq-seq-map-module-id-to-obj-file") (car-safe result))) ;;; manage background jobs (defun coq-par-kill-all-processes () - "Kill all background coqc and coqdep compilation processes." + "Kill all background coqc, coqdep or vio2vo compilation processes. +Return t if some process was killed." ;; need to first mark processes as killed, because delete process ;; starts running sentinels in the order processes terminated, so ;; after the first delete-process we see sentinentels of non-killed @@ -613,58 +737,74 @@ function returns () if MODULE-ID comes from the standard library." (when (process-get process 'coq-compilation-job) (process-put process 'coq-par-process-killed t) (delete-process process) - (when coq-debug-auto-compilation + (when coq--debug-auto-compilation (message "%s %s: kill it" (get (process-get process 'coq-compilation-job) 'name) (process-name process))))) (process-list)) - (setq coq-current-background-jobs 0))) + (setq coq--current-background-jobs 0) + kill-needed)) -(defun coq-par-unlock-ancestors-on-error () +(defun coq-par-unlock-all-ancestors-on-error () "Unlock ancestors which are not in an asserted span. Used for unlocking ancestors on compilation errors." - (when coq-par-ancestor-files - ;; nil e.g. when enabling on-the-fly compilation after processing imports. + (when coq--compilation-object-hash (maphash - (lambda (ancestor state) - (when (eq state 'locked) - (coq-unlock-ancestor ancestor) - (puthash ancestor nil coq-par-ancestor-files))) - coq-par-ancestor-files))) + (lambda (key job) + (when (eq (get job 'lock-state) 'locked) + (coq-unlock-ancestor (get job 'src-file)) + (put job 'lock-state 'unlocked))) + coq--compilation-object-hash))) (defun coq-par-emergency-cleanup () "Emergency cleanup for parallel background compilation. Kills all processes, unlocks ancestors, clears the queue region and resets the internal state." - (coq-par-kill-all-processes) - (setq coq-par-compilation-queue (coq-par-new-compilation-queue)) - (setq coq-last-compilation-job nil) - (when proof-action-list - (setq proof-shell-interrupt-pending t)) - (coq-par-unlock-ancestors-on-error) - (proof-release-lock) - (proof-detach-queue) - (setq proof-second-action-list-active nil) - (coq-par-init-compilation-hash)) + (interactive) ; needed for menu + (let (proc-killed was-busy) + (when coq--debug-auto-compilation + (message "emergency cleanup")) + (setq proc-killed (coq-par-kill-all-processes)) + (when (and (boundp 'prover-was-busy) + (or proc-killed coq--last-compilation-job + coq--compile-vio2vo-in-progress + coq--compile-vio2vo-delay-timer)) + (setq prover-was-busy t)) + (setq coq-par-compilation-queue (coq-par-new-queue)) + (setq coq--last-compilation-job nil) + (setq coq-par-vio2vo-queue (coq-par-new-queue)) + (setq coq--compile-vio2vo-in-progress nil) + (when coq--compile-vio2vo-delay-timer + (cancel-timer coq--compile-vio2vo-delay-timer) + (setq coq--compile-vio2vo-delay-timer nil)) + (coq-par-unlock-all-ancestors-on-error) + (when proof-action-list + (setq proof-shell-interrupt-pending t)) + (proof-release-lock) + (proof-detach-queue) + (setq proof-second-action-list-active nil) + (coq-par-init-compilation-hash))) (defun coq-par-process-filter (process output) "Store output from coq background compilation." (process-put process 'coq-process-output (concat (process-get process 'coq-process-output) output))) -(defun coq-par-start-process (command arguments continuation job) +(defun coq-par-start-process (command arguments continuation job file-rm) "Start asynchronous compilation job for COMMAND. This function starts COMMAND with arguments ARGUMENTS for compilation job JOB, making sure that CONTINUATION runs when the -process finishes successfully." +process finishes successfully. FILE-RM, if not nil, denotes a +file to be deleted when the process is killed." (let ((process-connection-type nil) ; use pipes - (process-name (format "pro-%s" coq-par-next-id)) + (process-name (format "pro-%s" coq--par-next-id)) process) (with-current-buffer (or proof-script-buffer (current-buffer)) - (if coq-debug-auto-compilation - (message "%s %s: start %s %s" - (get job 'name) process-name - command (mapconcat 'identity arguments " "))) + (when coq--debug-auto-compilation + (message "%s %s: start %s %s in %s" + (get job 'name) process-name + command (mapconcat 'identity arguments " ") + default-directory)) (condition-case err ;; If the command is wrong, start-process aborts with an ;; error. However, in Emacs 23.4.1. it will leave a process @@ -679,12 +819,13 @@ process finishes successfully." (set-process-filter process 'coq-par-process-filter) (set-process-sentinel process 'coq-par-process-sentinel) (set-process-query-on-exit-flag process nil) - (setq coq-par-next-id (1+ coq-par-next-id)) - (setq coq-current-background-jobs (1+ coq-current-background-jobs)) + (setq coq--par-next-id (1+ coq--par-next-id)) + (setq coq--current-background-jobs (1+ coq--current-background-jobs)) (process-put process 'coq-compilation-job job) (process-put process 'coq-process-continuation continuation) (process-put process 'coq-process-command (cons command arguments)) - (process-put process 'coq-process-output "")))) + (process-put process 'coq-process-output "") + (process-put process 'coq-process-rm file-rm)))) (defun coq-par-process-sentinel (process event) "Sentinel for all background processes. @@ -694,28 +835,48 @@ that has been registered with that process. Normal compilation errors are reported with an error message." (condition-case err (if (process-get process 'coq-par-process-killed) - (if coq-debug-auto-compilation - (message "%s %s: skip sentinel, process killed" - (get (process-get process 'coq-compilation-job) 'name) - (process-name process))) - (let (exit-status) - (if coq-debug-auto-compilation - (message "%s %s: process status changed to %s" + (progn + (when coq--debug-auto-compilation + (message "%s %s: skip sentinel, process killed, %s" (get (process-get process 'coq-compilation-job) 'name) (process-name process) - event)) + (if (process-get process 'coq-process-rm) + (format "rm %s" + (process-get process 'coq-process-rm)) + "no file removal"))) + (if (process-get process 'coq-process-rm) + (ignore-errors + (delete-file (process-get process 'coq-process-rm)))) + (when (eq (process-get process 'coq-process-continuation) + 'coq-par-vio2vo-continuation) + (when coq--debug-auto-compilation + (message "%s: reenqueue for vio2vo" + (get (process-get process 'coq-compilation-job) 'name))) + (coq-par-vio2vo-enqueue + (process-get process 'coq-compilation-job)))) + (let (exit-status) + (when coq--debug-auto-compilation + (message "%s %s: process status changed to %s" + (get (process-get process 'coq-compilation-job) 'name) + (process-name process) + event)) (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))) + (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--compile-vio2vo-in-progress + (eq coq--current-background-jobs 0)) + (setq coq--compile-vio2vo-in-progress nil) + (message "vio2vo compilation finished")) (when (and - (eq coq-current-background-jobs 0) - coq-last-compilation-job) + (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 @@ -736,6 +897,46 @@ errors are reported with an error message." (signal (car err) (cdr err))))) +;;; vio2vo compilation + +(defun coq-par-run-vio2vo-queue () + "Start delayed vio2vo compilation." + (assert (not coq--last-compilation-job) + nil "normal compilation and vio2vo in parallel 3") + (setq coq--compile-vio2vo-in-progress t) + (setq coq--compile-vio2vo-delay-timer nil) + (when coq--debug-auto-compilation + (message "Start vio2vo processing for %d jobs" + (+ (length (car coq-par-vio2vo-queue)) + (length (cdr coq-par-vio2vo-queue))))) + (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. +This function ensures that vio2vo compilation starts after +`coq-compile-vio2vo-delay' seconds after the last module has been +loaded into Coq. When background compilation is successful, this +callback is inserted with a dummy item into proof-action-list +somewhere after the last require command." + ;; When the user asserts new stuff while the (previously) last + ;; require command is being processed, `coq--last-compilation-job' + ;; might get non-nil. In this case there is a new last compilation + ;; job that will eventually trigger vio2vo compilation. + (unless (or coq--last-compilation-job + (not (eq race-counter coq--compile-vio2vo-start-id))) + (setq coq--compile-vio2vo-delay-timer + (run-at-time coq-compile-vio2vo-delay nil + 'coq-par-run-vio2vo-queue)))) + +(defun coq-par-callback-queue-item (callback) + ;; A proof-action-list item has the form of + ;; (SPAN COMMANDS ACTION [DISPLAYFLAGS]) + ;; If COMMANDS is nil, the item is processed as comment and not sent + ;; to the proof assistant, only the callback is called, see + ;; proof-shell.el. + (list nil nil callback)) + + ;;; background job tasks (defun coq-par-job-coqc-finished (job) @@ -756,145 +957,351 @@ errors are reported with an error message." (put dependant 'coqc-dependency-count (1+ (get dependant 'coqc-dependency-count))) (push dependant (get dependee 'coqc-dependants)) - (if coq-debug-auto-compilation - (message "%s -> %s: add coqc dependency" - (get dependee 'name) (get dependant 'name)))) + (when coq--debug-auto-compilation + (message "%s -> %s: add coqc dependency" + (get dependee 'name) (get dependant 'name)))) (defun coq-par-add-queue-dependency (dependee dependant) "Add queue dependency from child job DEPENDEE to parent job DEPENDANT." (assert (and (not (get dependant 'queue-dependant-waiting)) - (not (get dependee 'queue-dependant)))) + (not (get dependee 'queue-dependant))) + nil "queue dependency cannot be added") (put dependant 'queue-dependant-waiting t) (put dependee 'queue-dependant dependant) - (if coq-debug-auto-compilation - (message "%s -> %s: add queue dependency" - (get dependee 'name) (get dependant 'name)))) - -(defun coq-par-get-obj-mod-time (job) - "Return modification time of the object file as `file-attributes' would do. -Making sure that file-attributes is called at most once for every job." - (let ((obj-time (get job 'obj-mod-time))) - (cond - ((consp obj-time) obj-time) - ((eq obj-time 'obj-does-not-exist) nil) - ((not obj-time) - (setq obj-time (nth 5 (file-attributes (get job 'obj-file)))) - (if obj-time - (put job 'obj-mod-time obj-time) - (put job 'obj-mod-time 'obj-does-not-exist)) - obj-time)))) + (when coq--debug-auto-compilation + (message "%s -> %s: add queue dependency" + (get dependee 'name) (get dependant 'name)))) (defun coq-par-job-needs-compilation (job) - "Determine whether job needs to get compiled." - (let (src-time obj-time) - (if (eq (get job 'youngest-coqc-dependency) 'just-compiled) + "Determine whether job needs to get compiled and do some side effects. +This function contains most of the logic nesseary to support +quick compilation according to `coq-compile-quick'. Taking +`coq-compile-quick' into account, it determines if a compilation +is necessary. The property 'required-obj-file is set either to +the file that we need to produce or to the up-to-date object +file. If compilation is needed, property 'use-quick is set when +-quick will be used. If no compilation is needed, property +'obj-mod-time remembers the time stamp of 'required-obj-file. +Indepent of whether compilation is required, .vo or .vio files +that are in the way are deleted. Note that the coq documentation +does not contain a statement, about what file is loaded, if both +a .vo and a .vio file are present. To be on the safe side, I +therefore delete a file if it might be in the way. Sets the +'vio2vo property on job if necessary." + (let* ((vo-file (get job 'vo-file)) + (vio-file (coq-library-vio-of-vo-file vo-file)) + (vo-obj-time (nth 5 (file-attributes vo-file))) + (vio-obj-time (nth 5 (file-attributes vio-file))) + (dep-time (get job 'youngest-coqc-dependency)) + (src-time (nth 5 (file-attributes (get job 'src-file)))) + file-to-delete max-obj-time vio-is-newer + other-file other-obj-time result) + (when coq--debug-auto-compilation + (message + (concat "%s: compare mod times: vo mod %s, vio mod %s, src mod %s, " + "youngest dep %s; vo < src : %s, vio < src : %s, " + "vo < dep : %s, vio < dep : %s") + (get job 'name) + (if vo-obj-time (current-time-string vo-obj-time) "-") + (if vio-obj-time (current-time-string vio-obj-time) "-") + (if src-time (current-time-string src-time) "-") + (if (eq dep-time 'just-compiled) "just compiled" + (current-time-string dep-time)) + (if vo-obj-time (time-less-p vo-obj-time src-time) "-") + (if vio-obj-time (time-less-p vio-obj-time src-time) "-") + (if vo-obj-time (coq-par-time-less vo-obj-time dep-time) "-") + (if vio-obj-time (coq-par-time-less vio-obj-time dep-time) "-"))) + ;; Compute first the max of vo-obj-time and vio-obj-time and remember + ;; which of both is newer. This is only meaningful if at least one of + ;; the .vo or .vio file exists. + (cond + ((and vio-obj-time vo-obj-time + (time-less-or-equal vo-obj-time vio-obj-time)) + (setq max-obj-time vio-obj-time) + (setq vio-is-newer t)) + ((and vio-obj-time vo-obj-time) + (setq max-obj-time vo-obj-time)) + (vio-obj-time + (setq max-obj-time vio-obj-time) + (setq vio-is-newer t)) + (t + (setq max-obj-time vo-obj-time))) + ;; Decide if and what to compile. + (if (or (eq dep-time 'just-compiled) ; a dep has been just compiled + (and (not vo-obj-time) (not vio-obj-time)) ; no obj exists + ;; src younger than any obj? + (time-less-or-equal max-obj-time src-time) + ;; dep younger than any obj? + (time-less-or-equal max-obj-time dep-time)) + ;; compilation is definitely needed (progn - (if coq-debug-auto-compilation - (message "%s: needs compilation because a dep was just compiled" - (get job 'name))) - t) - (setq src-time (nth 5 (file-attributes (get job 'src-file)))) - (setq obj-time (coq-par-get-obj-mod-time job)) - (if coq-debug-auto-compilation - (message - (concat "%s: compare mod times: obj mod %s, src mod %s, " - "youngest dep %s; obj <= src : %s, obj < dep : %s") - (get job 'name) - (current-time-string obj-time) - (current-time-string src-time) - (current-time-string (get job 'youngest-coqc-dependency)) - (if obj-time (time-less-or-equal obj-time src-time) "-") - (if obj-time - (time-less-p obj-time (get job 'youngest-coqc-dependency)) - "-"))) - (or - (not obj-time) ; obj does not exist - (time-less-or-equal obj-time src-time) ; src is newer - ; youngest dep is newer than obj - (time-less-p obj-time (get job 'youngest-coqc-dependency)))))) + (setq result t) + (if (coq-compile-prefer-quick) + (progn + (put job 'required-obj-file vio-file) + (put job 'use-quick t) + (when vo-obj-time + (setq file-to-delete vo-file)) + (when (eq coq-compile-quick 'quick-and-vio2vo) + (put job 'vio2vo-needed t))) + (put job 'required-obj-file vo-file) + (when vio-obj-time + (setq file-to-delete vio-file))) + (when coq--debug-auto-compilation + (message + (concat "%s: definitely need to compile to %s; delete %s") + (get job 'name) + (get job 'required-obj-file) + (if file-to-delete file-to-delete "noting")))) + ;; Either the .vio or the .vo file exists and one of .vio or .vo is + ;; younger than the source and the youngest dependency. Might not + ;; need to compile. + (if (eq coq-compile-quick 'ensure-vo) + (progn + (put job 'required-obj-file vo-file) + (if (or (not vio-is-newer) ; vo is newest + (and vo-obj-time ; vo is older than vio + ; but still newer than src or dep + (time-less-p src-time vo-obj-time) + (time-less-p dep-time vo-obj-time))) + ;; .vo is newer than src and youngest dep - don't compile + (progn + (put job 'obj-mod-time vo-obj-time) + ;; delete vio if it is outdated or newer than vo + (when (and vio-obj-time + (or vio-is-newer + (time-less-or-equal vio-obj-time src-time) + (time-less-or-equal vio-obj-time dep-time))) + (setq file-to-delete vio-file)) + (when coq--debug-auto-compilation + (message "%s: vo up-to-date 1; delete %s" + (get job 'name) + (if file-to-delete file-to-delete "noting")))) + ;; .vo outdated - need to compile + (setq result t) + ;; delete vio if it is outdated + (when (and vio-obj-time + (or (time-less-or-equal vio-obj-time src-time) + (time-less-or-equal vio-obj-time dep-time))) + (setq file-to-delete vio-file)) + (when coq--debug-auto-compilation + (message "%s: need to compile to vo; delete %s" + (get job 'name) + (if file-to-delete file-to-delete "noting"))))) + ;; There is an up-to-date .vio or .vo file and the user does not + ;; insist on either .vio or .vo - no need to compile. + ;; Ensure to delete outdated .vio or .vo files. + ;; First store the other obj file in other-file and other-obj-time. + (if vio-is-newer + (setq other-file vo-file + other-obj-time vo-obj-time) + (setq other-file vio-file + other-obj-time vio-obj-time)) + (if (and other-obj-time + (time-less-p src-time other-obj-time) + ;; dep-time is neither nil nor 'just-compiled here + (time-less-p dep-time other-obj-time)) + ;; Both the .vio and .vo exist and are up-to-date. Coq + ;; loads the younger one but we continue with the older + ;; one to avoid recompilation for the case where a vio2vo + ;; process took a long time for a dependency. + (progn + (put job 'required-obj-file other-file) + (put job 'obj-mod-time other-obj-time) + (when coq--debug-auto-compilation + (message (concat "%s: .vio and .vo up-to-date, " + "continue with the older %s") + (get job 'name) + (if vio-is-newer ".vio" ".vo")))) + ;; The other obj file does not exist or is outdated. + ;; Delete the outdated if it exists. + (when other-obj-time + (setq file-to-delete other-file)) + (if vio-is-newer + (progn + (put job 'required-obj-file vio-file) + (put job 'obj-mod-time vio-obj-time) + (when (eq coq-compile-quick 'quick-and-vio2vo) + (put job 'vio2vo-needed t)) + (when coq--debug-auto-compilation + (message "%s: vio up-to-date; delete %s" + (get job 'name) + (if file-to-delete file-to-delete "noting")))) + (put job 'required-obj-file vo-file) + (put job 'obj-mod-time vo-obj-time) + (when coq--debug-auto-compilation + (message "%s: vo up-to-date 2; delete %s" + (get job 'name) + (if file-to-delete file-to-delete "noting"))))))) + (when file-to-delete + (condition-case err + (delete-file file-to-delete) + (file-error + (signal 'coq-compile-error-rm err)))) + result)) + +(defun coq-par-retire-top-level-job (job) + "Register ancestors and start queue items. +This function performs the essential tasks for top-level jobs +when they transition from 'waiting-queue to 'ready: +- Registering ancestors in the span and recording this fact in + the 'lock-state property. +- Moving queue items back to `proof-action-list' and start their + execution. +- Insert `coq-par-require-processed' as callback if this is the + last top-level job, such that vio2vo compilation will start + eventually. + +This function can safely be called for non-top-level jobs. This +function must not be called for failed jobs." + (assert (not (get job 'failed)) + nil "coq-par-retire-top-level-job precondition failed") + (let ((span (get job 'require-span)) + (items (get job 'queueitems))) + (when (and span coq-lock-ancestors) + (dolist (anc-job (get job 'ancestors)) + (assert (not (eq (get anc-job 'lock-state) 'unlocked)) + nil "bad ancestor lock state") + (when (eq (get anc-job 'lock-state) 'locked) + (put anc-job 'lock-state 'asserted) + (push (get anc-job 'src-file) + (span-property span 'coq-locked-ancestors))))) + (when items + (when (and (eq coq-compile-quick 'quick-and-vio2vo) + (eq coq--last-compilation-job job)) + (let ((vio2vo-counter + (setq coq--compile-vio2vo-start-id + (1+ coq--compile-vio2vo-start-id)))) + ;; Insert a notification callback for when the last require + ;; queue item has been processed. + (setq items + (cons + (car items) ; this is the require + (cons + (coq-par-callback-queue-item + `(lambda (span) (coq-par-require-processed ,vio2vo-counter))) + (cdr items)))))) + (proof-add-to-queue items 'advancing) + (when coq--debug-auto-compilation + (message "%s: add %s items to action list" + (get job 'name) (length items))) + (put job 'queueitems nil)))) (defun coq-par-kickoff-queue-maybe (job) "Try transition 'waiting-queue -> 'ready for job JOB. This transition is only possible if JOB is in state 'waiting-queue and if it has no queue dependee. If this is the case, the following actions are taken: -- for top-level jobs (non-nil 'require-span property), ancestors - are registered in `coq-par-ancestor-files' and in the span in - 'queue-span -- processing of items in 'queueitems is started +- for successful top-level jobs (non-nil 'require-span property), ancestors + are registered in the 'queue-span and marked as 'asserted in their + 'lock-state property +- processing of items in 'queueitems is started (if JOB is successful) - a possible queue dependant gets it's dependency cleared, and, if possible the 'waiting-queue -> 'ready transition is (recursively) done for the dependant - if this job is the last top-level compilation - job (`coq-last-compilation-job') then the last compilation job - and `proof-second-action-list-active' are cleared." + job (`coq--last-compilation-job') then the last compilation job + and `proof-second-action-list-active' are cleared and vio2vo + processing is triggered. +- If compilation failed, the (failing) last top-level job is + delayed until `proof-action-list' is empty, possibly by + registering this call as a callback in an empty + proof-action-list item. When proof-action-list is empty, the + queue span is deleted, remaining spans are cleared and the + `proof-shell-busy' lock is freed." (if (or (not (eq (get job 'state) 'waiting-queue)) (get job 'queue-dependant-waiting)) - (if coq-debug-auto-compilation - (if (not (eq (get job 'state) 'waiting-queue)) - (message "%s: no queue kickoff because in state %s" - (get job 'name) (get job 'state)) - (message - "%s: no queue kickoff because waiting for queue dependency" - (get job 'name)))) - (if coq-debug-auto-compilation - (message "%s: has itself no queue dependency" (get job 'name))) - (when (and (get job 'require-span) coq-lock-ancestors) - (let ((span (get job 'require-span))) - (dolist (f (get job 'ancestor-files)) - (unless (eq (gethash f coq-par-ancestor-files) 'asserted) - (puthash f 'asserted coq-par-ancestor-files) - (span-set-property - span 'coq-locked-ancestors - (cons f (span-property span 'coq-locked-ancestors))))))) - (when (get job 'queueitems) - (proof-add-to-queue (get job 'queueitems) 'advancing) - (if coq-debug-auto-compilation - (message "%s: add %s items to action list" - (get job 'name) (length (get job 'queueitems)))) - (put job 'queueitems nil)) - (put job 'state 'ready) - (if coq-debug-auto-compilation + (when coq--debug-auto-compilation + (if (not (eq (get job 'state) 'waiting-queue)) + (message "%s: no queue kickoff because in state %s" + (get job 'name) (get job 'state)) + (message + "%s: no queue kickoff because waiting for queue dependency" + (get job 'name)))) + (when coq--debug-auto-compilation + (message "%s: has itself no queue dependency" (get job 'name))) + (unless (get job 'failed) + (coq-par-retire-top-level-job job)) + (when (and (get job 'failed) (get job 'require-span)) + (setq coq--par-delayed-last-job nil)) + (if (and (get job 'failed) + (eq coq--last-compilation-job job) + proof-action-list) + (progn + (when coq--debug-auto-compilation + (message "%s: delay queue kickoff until action list is empty" + (get job 'name))) + (setq coq--par-delayed-last-job t) + (proof-add-to-queue + (list (coq-par-callback-queue-item + `(lambda (span) (coq-par-kickoff-queue-maybe ',job)))) + 'advancing)) + (put job 'state 'ready) + (when coq--debug-auto-compilation (message "%s: ready" (get job 'name))) - (let ((dependant (get job 'queue-dependant))) - (if dependant - (progn - (assert (not (eq coq-last-compilation-job job))) - (put dependant 'queue-dependant-waiting nil) - (if coq-debug-auto-compilation + (let ((dependant (get job 'queue-dependant))) + (if dependant + (progn + (assert (not (eq coq--last-compilation-job job)) + nil "coq--last-compilation-job invariant error") + (put dependant 'queue-dependant-waiting nil) + (when coq--debug-auto-compilation (message "%s -> %s: clear queue dependency, kickoff queue at %s" (get job 'name) (get dependant 'name) (get dependant 'name))) - (coq-par-kickoff-queue-maybe dependant) - (if coq-debug-auto-compilation + (coq-par-kickoff-queue-maybe dependant) + (when coq--debug-auto-compilation (message "%s: queue kickoff finished" (get job 'name)))) - (when (eq coq-last-compilation-job job) - (setq coq-last-compilation-job nil) - (setq proof-second-action-list-active nil) - (if coq-debug-auto-compilation + (when (eq coq--last-compilation-job job) + (when (get job 'failed) + ;; proof-action-list is empty, see above + ;; variables that hold the queue span are buffer local + (with-current-buffer (or proof-script-buffer (current-buffer)) + (proof-script-clear-queue-spans-on-error nil)) + (proof-release-lock) + (when (eq coq-compile-quick 'quick-and-vio2vo) + (assert (not coq--compile-vio2vo-delay-timer) + nil "vio2vo timer set before last compilation job") + (setq coq--compile-vio2vo-delay-timer + (run-at-time coq-compile-vio2vo-delay nil + 'coq-par-run-vio2vo-queue)))) + (setq coq--last-compilation-job nil) + (setq proof-second-action-list-active nil) + (when coq--debug-auto-compilation (message "clear last compilation job")) - (message "Library compilation finished")) - (if coq-debug-auto-compilation + (message "Library compilation %s" + (if (get job 'failed) "failed" "finished successfully"))) + (when coq--debug-auto-compilation (message "%s: no queue dependant, queue kickoff finished" - (get job 'name))))))) + (get job 'name)))))))) (defun coq-par-compile-job-maybe (job) "Choose next action for JOB after dependencies are ready. -First JOB is put into state 'enqueued-coqc. Then, if JOB needs -compilation, compilation is started or enqueued and JOB stays in -'enqueued-coqc for the time being. Otherwise, the transition -'enqueued-coqc -> 'waiting-queue is done and, if possible, also -'waiting-queue -> 'ready." +First JOB is put into state 'enqueued-coqc. Then it is determined +if JOB needs compilation, what file must be produced (depending +on `coq-compile-quick') and if a .vio or .vo file must be +deleted. If necessary, deletion happens immediately. If JOB needs +compilation, compilation is started or the JOB is enqueued and +JOB stays in 'enqueued-coqc for the time being. Otherwise, the +transition 'enqueued-coqc -> 'waiting-queue is done and, if +possible, also 'waiting-queue -> 'ready." (put job 'state 'enqueued-coqc) - (if (coq-par-job-needs-compilation job) + ;; Note that coq-par-job-needs-compilation sets 'required-obj-file + ;; as a side effect and deletes .vo or .vio files that are in the way. + ;; It also sets the 'vio2vo-needed property if needed. + (if (and (not (get job 'failed)) (coq-par-job-needs-compilation job)) (coq-par-start-or-enqueue job) - (if coq-debug-auto-compilation - (message "%s: up-to-date, no compilation" (get job 'name))) + (when coq--debug-auto-compilation + (message "%s: %s, no compilation" + (get job 'name) + (if (get job 'failed) "failed" "up-to-date"))) + (when (get job 'vio2vo-needed) + (coq-par-vio2vo-enqueue job)) (coq-par-kickoff-coqc-dependants job (get job 'youngest-coqc-dependency)))) (defun coq-par-decrease-coqc-dependency (dependant dependee-time - dependee-ancestor-files) + dependee-ancestors) "Clear Coq dependency and update dependee information in DEPENDANT. This function handles a Coq dependency from child dependee to parent dependant when the dependee has finished compilation (ie. @@ -907,18 +1314,20 @@ if it reaches 0, the next transition is triggered for DEPENDANT. For 'file jobs this is 'waiting-dep -> 'enqueued-coqc and for 'clone jobs this 'waiting-dep -> 'waiting-queue." ;(message "%s: CPDCD with time %s" (get dependant 'name) dependee-time) - (assert (eq (get dependant 'state) 'waiting-dep)) + (assert (eq (get dependant 'state) 'waiting-dep) + nil "wrong state of parent dependant job") (when (coq-par-time-less (get dependant 'youngest-coqc-dependency) dependee-time) (put dependant 'youngest-coqc-dependency dependee-time)) - (put dependant 'ancestor-files - (append dependee-ancestor-files (get dependant 'ancestor-files))) + (put dependant 'ancestors + (append dependee-ancestors (get dependant 'ancestors))) (put dependant 'coqc-dependency-count (1- (get dependant 'coqc-dependency-count))) - (assert (<= 0 (get dependant 'coqc-dependency-count))) - (if coq-debug-auto-compilation - (message "%s: coqc dependency count down to %d" - (get dependant 'name) (get dependant 'coqc-dependency-count))) + (assert (<= 0 (get dependant 'coqc-dependency-count)) + nil "dependency count below zero") + (when coq--debug-auto-compilation + (message "%s: coqc dependency count down to %d" + (get dependant 'name) (get dependant 'coqc-dependency-count))) (when (coq-par-dependencies-ready dependant) (cond ((eq (get dependant 'type) 'file) @@ -939,7 +1348,8 @@ waiting-queue for JOB. DEP-TIME is either 'just-compiled, when JOB has just finished compilation, or the most recent modification time of all -dependencies of JOB. +dependencies of JOB. (If compilation for JOB failed, DEP-TIME is +meaningless but should nevertheless be a non-nil valid argument.) This function makes the following actions. - Clear the dependency from JOB to all its dependants, thereby @@ -948,50 +1358,87 @@ This function makes the following actions. - save the maximum of DEP-TIME and .vo modification time in 'youngest-coqc-dependency, in case we later create a clone of this job - put JOB into state 'waiting-queue -- try to trigger the transition 'waiting-queue -> ready for JOB" - (let ((ancestor-files (get job 'ancestor-files))) +- try to trigger the transition 'waiting-queue -> ready for JOB +- If JOB is successful but all dependants have failed, unlock all + ancestors in case they are not participating in a still ongoing + compilation." + (let ((ancestors (get job 'ancestors)) + (dependant-alive nil)) + (put job 'state 'waiting-queue) ;; take max of dep-time and obj-mod-time ;; ;; dep-time is either 'just-compiled or 'youngest-coqc-dependency of ;; the dependee, in the latter case obj-mod-time is greater than ;; dep-time, because otherwise we would have compiled the file. For ;; a clone job the max has already been taken when processing the - ;; original file. - (unless (or (eq dep-time 'just-compiled) (eq (get job 'type) 'clone)) - (setq dep-time (coq-par-get-obj-mod-time job))) + ;; original file. If coqdep failed, 'obj-mod-time is not set. + (unless (or (eq dep-time 'just-compiled) (eq (get job 'type) 'clone) + (get job 'failed)) + (setq dep-time (get job 'obj-mod-time))) (put job 'youngest-coqc-dependency dep-time) - (if coq-debug-auto-compilation - (message "%s: kickoff %d coqc dependencies with time %s" - (get job 'name) (length (get job 'coqc-dependants)) - (if (eq dep-time 'just-compiled) - 'just-compiled - (current-time-string dep-time)))) - (put job 'state 'waiting-queue) - (mapc - (lambda (dependant) - (coq-par-decrease-coqc-dependency dependant dep-time ancestor-files)) - (get job 'coqc-dependants)) - (if coq-debug-auto-compilation - (message "%s: coqc kickoff finished, maybe kickoff queue" - (get job 'name))) + (when coq--debug-auto-compilation + (message "%s: kickoff %d coqc dependencies with time %s" + (get job 'name) (length (get job 'coqc-dependants)) + (if (eq dep-time 'just-compiled) + 'just-compiled + (current-time-string dep-time)))) + (dolist (dependant (get job 'coqc-dependants)) + (coq-par-decrease-coqc-dependency dependant dep-time ancestors) + (unless (get dependant 'failed) + (setq dependant-alive t))) + (when coq--debug-auto-compilation + (message (concat "%s: coqc kickoff finished, %s dependant alive, " + "maybe kickoff queue") + (get job 'name) + (if dependant-alive "some" "no"))) + (assert (or (not (get job 'failed)) (not dependant-alive)) + nil "failed job with non-failing dependant") + (when (or (and (not dependant-alive) + (not (get job 'require-span)) + (not (get job 'failed))) + (and (get job 'queue-failed) (not (get job 'failed)))) + ;; job has not failed, but all dependants have 'failed set, or + ;; top-level job marked with 'queue-failed changes to 'failed + (when (get job 'queue-failed) + (when coq--debug-auto-compilation + (message "%s: queue-failed -> failed, unlock ancestors" + (get job 'name))) + (put job 'failed t)) + (coq-par-unlock-job-ancestors-on-error job)) (coq-par-kickoff-queue-maybe job))) (defun coq-par-start-coqdep (job) "Start coqdep for JOB. -Besides starting the background process, the source file is -locked, registered in the 'ancestor-files property of JOB and in -`coq-par-ancestor-files'" - (let ((true-src (file-truename (get job 'src-file)))) - (when coq-lock-ancestors - (proof-register-possibly-new-processed-file true-src) - (put job 'ancestor-files (list true-src)) - (unless (gethash true-src coq-par-ancestor-files) - (puthash true-src 'locked coq-par-ancestor-files))) +Lock the source file and start the coqdep background process" + (when (and coq-lock-ancestors + (eq (get job 'lock-state) 'unlocked)) + (proof-register-possibly-new-processed-file (get job 'src-file)) + (push job (get job 'ancestors)) + (put job 'lock-state 'locked)) + (coq-par-start-process + coq-dependency-analyzer + (coq-par-coqdep-arguments (get job 'src-file) (get job 'load-path)) + 'coq-par-process-coqdep-result + job + nil)) + +(defun coq-par-start-vio2vo (job) + "Start vio2vo background job." + (let ((arguments (coq-include-options (get job 'load-path))) + (module (coq-module-of-src-file (get job 'src-file))) + (default-directory + (file-name-directory (file-truename (get job 'src-file))))) + (when coq--debug-auto-compilation + (message "%s: start vio2vo for %s" + (get job 'name) + (get job 'src-file))) + (message "vio2vo %s" (get job 'src-file)) (coq-par-start-process - coq-dependency-analyzer - (coq-par-coqdep-arguments (get job 'src-file) (get job 'load-path)) - 'coq-par-process-coqdep-result - job))) + coq-prog-name + (nconc arguments (list "-schedule-vio2vo" "1" module)) + 'coq-par-vio2vo-continuation + job + (get job 'vo-file)))) (defun coq-par-start-task (job) "Start the background job for which JOB is waiting. @@ -1002,32 +1449,45 @@ coqdep or coqc are started for it." ((eq job-state 'enqueued-coqdep) (coq-par-start-coqdep job)) ((eq job-state 'enqueued-coqc) - (message "Recompile %s" (get job 'src-file)) - (coq-par-start-process - coq-compiler - (coq-par-coqc-arguments (get job 'src-file) (get job 'load-path)) - 'coq-par-coqc-continuation - job))))) + (message "Recompile %s%s" + (if (get job 'use-quick) "-quick " "") + (get job 'src-file)) + (let ((arguments + (coq-par-coqc-arguments (get job 'src-file) (get job 'load-path)))) + (when (get job 'use-quick) + (push "-quick" arguments)) + (coq-par-start-process + coq-compiler + arguments + 'coq-par-coqc-continuation + job + (get job 'required-obj-file)))) + ((eq job-state 'ready) + (coq-par-start-vio2vo job)) + (t (assert nil nil "coq-par-start-task with invalid job"))))) (defun coq-par-start-jobs-until-full () "Start background jobs until the limit is reached." - (let ((next-job t)) - (while (and next-job - (< coq-current-background-jobs coq-internal-max-jobs)) - (setq next-job (coq-par-dequeue)) - (when next-job - (coq-par-start-task next-job))))) + (let ((max-jobs (if coq--compile-vio2vo-in-progress + coq--internal-max-vio2vo-jobs + coq--internal-max-jobs)) + next-job) + (while (and (< coq--current-background-jobs max-jobs) + (setq next-job (if coq--compile-vio2vo-in-progress + (coq-par-vio2vo-dequeue) + (coq-par-job-dequeue)))) + (coq-par-start-task next-job)))) (defun coq-par-start-or-enqueue (new-job) "Start NEW-JOB or put it into the queue of waiting jobs. NEW-JOB goes already into the waiting queue, if the number of background jobs is one below the limit. This is in order to leave room for Proof General." - (if (< (1+ coq-current-background-jobs) coq-internal-max-jobs) + (if (< (1+ coq--current-background-jobs) coq--internal-max-jobs) (coq-par-start-task new-job) - (coq-par-enqueue new-job))) + (coq-par-job-enqueue new-job))) -(defun coq-par-create-library-job (module-obj-file coq-load-path queue-dep +(defun coq-par-create-library-job (module-vo-file coq-load-path queue-dep require-span dependant) "Create a new compilation job for MODULE-OBJ-FILE. If there is already a job for MODULE-OBJ-FILE a new clone job is @@ -1051,25 +1511,26 @@ If the new job is a clone job, its state is a queue dependency QUEUE-DEP (which cannot be ready yet) - 'ready otherwise -If the new job is a 'file job it's state is 'enqueued-coqdep. If +If the new job is a 'file job its state is 'enqueued-coqdep. If there is space, coqdep is started immediately, otherwise the new job is put into the compilation queue. This function returns the newly created job." - (let* ((orig-job (gethash module-obj-file coq-compilation-object-hash)) + (let* ((orig-job (gethash module-vo-file coq--compilation-object-hash)) (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 'obj-file module-obj-file) + (put new-job 'name (format "job-%d" coq--par-next-id)) + (setq coq--par-next-id (1+ coq--par-next-id)) + (put new-job 'vo-file module-vo-file) (put new-job 'coqc-dependency-count 0) (put new-job 'require-span require-span) + ;; fields 'required-obj-file and obj-mod-time are implicitely set to nil (if orig-job - ;; there is already a compilation job for module-obj-file + ;; there is already a compilation job for module-vo-file (progn (put new-job 'type 'clone) - (if coq-debug-auto-compilation - (message "%s: create %s compilation job for %s" - (get new-job 'name) (get new-job 'type) module-obj-file)) + (when coq--debug-auto-compilation + (message "%s: create %s compilation job for %s" + (get new-job 'name) (get new-job 'type) module-vo-file)) (when queue-dep (coq-par-add-queue-dependency queue-dep new-job)) (if (coq-par-job-coqc-finished orig-job) @@ -1079,44 +1540,143 @@ This function returns the newly created job." (put new-job 'state 'ready)) (put new-job 'youngest-coqc-dependency (get orig-job 'youngest-coqc-dependency)) - (put new-job 'ancestor-files (get orig-job 'ancestor-files))) + (put new-job 'ancestors (get orig-job 'ancestors))) (coq-par-add-coqc-dependency orig-job new-job) (put new-job 'state 'waiting-dep) (put new-job 'youngest-coqc-dependency '(0 0)))) - ;; there is no compilation for this file yet + ;; there is no compilation job for this file yet (put new-job 'type 'file) (put new-job 'state 'enqueued-coqdep) - (put new-job 'src-file (coq-library-src-of-obj-file module-obj-file)) + (put new-job 'src-file (coq-library-src-of-vo-file module-vo-file)) (when (equal (get new-job 'src-file) (buffer-file-name proof-script-buffer)) (signal 'coq-compile-error-circular-dep (concat dependant " -> scripting buffer"))) - (message "Check %s" (get new-job 'src-file)) (put new-job 'load-path coq-load-path) (put new-job 'youngest-coqc-dependency '(0 0)) - (puthash module-obj-file new-job coq-compilation-object-hash) - (if coq-debug-auto-compilation - (message "%s: create %s compilation for %s" - (get new-job 'name) (get new-job 'type) module-obj-file)) + (puthash module-vo-file new-job coq--compilation-object-hash) + (when coq--debug-auto-compilation + (message "%s: create %s compilation for %s" + (get new-job 'name) (get new-job 'type) module-vo-file)) + (if (member (file-truename (get new-job 'src-file)) + proof-included-files-list) + (put new-job 'lock-state 'asserted) + (put new-job 'lock-state 'unlocked)) (when queue-dep (coq-par-add-queue-dependency queue-dep new-job)) + (message "Check %s" (get new-job 'src-file)) (coq-par-start-or-enqueue new-job)) new-job)) +(defun coq-par-ongoing-compilation (job) + "Determine if the source file for JOB needs to stay looked. +Return t if job has a direct or indirect dependant that has not +failed yet and that is in a state before 'waiting-queue. Also, +return t if JOB has a dependant that is a top-level job which has +not yet failed." + (assert (not (eq (get job 'lock-state) 'asserted)) + nil "coq-par-ongoing-compilation precondition failed") + (cond + ((get job 'failed) + nil) + ((or (eq (get job 'state) 'waiting-dep) + (eq (get job 'state) 'enqueued-coqc) + ;; top-level job that has compilation finished but has not + ;; been asserted yet + (and (eq (get job 'state) 'waiting-queue) (get job 'require-span)) + ;; Note that job cannot be a top-level in state 'ready, + ;; because we started from job with 'lock-state property equal + ;; to 'locked. Top-level job in state 'ready have all + ;; dependees with 'lock-state equal to 'asserted. + ) + t) + ;; Note that non-top-level jobs switch to 'waiting-queue as soon as + ;; all dependencies are ready, before they start to deal with the + ;; ancestors. We might therefore see here non-top-level jobs in + ;; state 'waiting-queue: they have successfully finished their + ;; compilation and are about to go to state 'ready. + ((or (eq (get job 'state) 'ready) + (eq (get job 'state) 'waiting-queue)) + ;; internal ready job + (let ((dependants (get job 'coqc-dependants)) + (res nil) + dep) + (while (and (not res) (setq dep (pop dependants))) + (setq res (coq-par-ongoing-compilation dep))) + res)) + (t + (assert nil nil + "impossible ancestor state %s on job %s" + (get job 'state) (get job 'name))))) + +(defun coq-par-unlock-job-ancestors-on-error (job) + "Unlock those ancestors of JOB that need to be unlocked. +For a failing job JOB, an ancestor need to stay looked if there +is still some compilation going on for which this ancestor is a +dependee or if a top level job with JOB as ancestor has finished +it's compilation successfully. In all other cases the ancestor +must be unlocked." + (dolist (anc-job (get job 'ancestors)) + (when (and (eq (get anc-job 'lock-state) 'locked) + (not (coq-par-ongoing-compilation anc-job))) + (when coq--debug-auto-compilation + (message "%s: %s unlock because no ongoing compilation" + (get anc-job 'name) (get anc-job 'src-file))) + (coq-unlock-ancestor (get anc-job 'src-file)) + (put anc-job 'lock-state 'unlocked)))) + +(defun coq-par-mark-queue-failing (job) + "Mark JOB with 'queue-failed. +Mark JOB with 'queue-failed, and, if JOB is in state +'waiting-queue, transition to 'failed and unlock ancestors as +appropriate." + (unless (or (get job 'failed) (get job 'queue-failed)) + (put job 'queue-failed t) + (assert (not (eq (get job 'state) 'ready)) + nil "coq-par-mark-queue-failing impossible state") + (when coq--debug-auto-compilation + (message "%s: mark as queue-failed, %s" + (get job 'name) + (if (eq (get job 'state) 'waiting-queue) + "failed, and unlock ancestors" + "wait"))) + (when (eq (get job 'state) 'waiting-queue) + (put job 'failed t) + (coq-par-unlock-job-ancestors-on-error job)) + (when (get job 'queue-dependant) + (coq-par-mark-queue-failing (get job 'queue-dependant))))) + +(defun coq-par-mark-job-failing (job) + "Mark all dependants of JOB as failing and unlock ancestors as appropriate. +Set the 'failed property on all direct and indirect dependants of +JOB. Along the way, unlock ancestors as determined by +`coq-par-ongoing-compilation'. Mark queue dependants with +'queue-failed." + (unless (get job 'failed) + (put job 'failed t) + (when coq--debug-auto-compilation + (message "%s: mark as failed and unlock free ancestors" (get job 'name))) + (coq-par-unlock-job-ancestors-on-error job) + (dolist (dependant (get job 'coqc-dependants)) + (coq-par-mark-job-failing dependant)) + (when (get job 'queue-dependant) + (coq-par-mark-queue-failing (get job 'queue-dependant))))) + (defun coq-par-process-coqdep-result (process exit-status) "Coqdep continuation function: Process coqdep output. -This function analyses the coqdep output of PROCESS and signals -an error if necessary. If there was no coqdep error, the -following actions are taken. +This function analyses the coqdep output of PROCESS. In case of +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. - 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 Coq dependency is registered from the new job to the current job. For dependencies that are 'ready already, the most recent ancestor modification time is propagated. -- if there are no dependencies or all dependencies are ready - already, the next transition to 'enqueued-coqc is triggered for - the current job +- if there are no dependencies (especially if coqdep failed) or + all dependencies are ready already, the next transition to + 'enqueued-coqc is triggered for the current job - otherwise the current job is left alone until somebody decreases its dependency count to 0 @@ -1130,88 +1690,123 @@ is directly passed to `coq-par-analyse-coq-dep-exit'." (process-get process 'coq-process-command))) job-max-time) (if (stringp dependencies-or-error) - (signal 'coq-compile-error-coqdep (get job 'src-file)) + (if coq-compile-keep-going + (coq-par-mark-job-failing job) + (signal 'coq-compile-error-coqdep (get job 'src-file))) ;; no coqdep error -- work on dependencies - (if coq-debug-auto-compilation - (message "%s: dependencies of %s are %s" - (get job 'name) (get job 'src-file) dependencies-or-error)) - (put job 'state 'waiting-dep) + (when coq--debug-auto-compilation + (message "%s: dependencies of %s are %s" + (get job 'name) (get job 'src-file) dependencies-or-error)) (setq job-max-time (get job 'youngest-coqc-dependency)) - (mapc - (lambda (dep-obj-file) - (unless (coq-compile-ignore-file dep-obj-file) - (let* ((dep-job (coq-par-create-library-job dep-obj-file - (get job 'load-path) - nil nil - (get job 'src-file))) - (dep-time (get dep-job 'youngest-coqc-dependency))) - (when (coq-par-time-less job-max-time dep-time) - (setq job-max-time dep-time)) - (unless (coq-par-job-coqc-finished dep-job) - (coq-par-add-coqc-dependency dep-job job))))) - dependencies-or-error) - (put job 'youngest-coqc-dependency job-max-time) - (if (coq-par-dependencies-ready job) - (progn - (if coq-debug-auto-compilation - (message "%s: coqc dependencies finished" (get job 'name))) - (coq-par-compile-job-maybe job)) - (if coq-debug-auto-compilation - (message "%s: wait for %d dependencies" - (get job 'name) (get job 'coqc-dependency-count))))))) + (dolist (dep-vo-file dependencies-or-error) + (unless (coq-compile-ignore-file dep-vo-file) + (let* ((dep-job (coq-par-create-library-job dep-vo-file + (get job 'load-path) + nil nil + (get job 'src-file))) + (dep-time (get dep-job 'youngest-coqc-dependency))) + (when (coq-par-time-less job-max-time dep-time) + (setq job-max-time dep-time)) + (unless (coq-par-job-coqc-finished dep-job) + (coq-par-add-coqc-dependency dep-job job))))) + (put job 'youngest-coqc-dependency job-max-time)) + ;; common part for job where coqdep was successful and where + ;; coqdep failed (when coq-compile-keep-going) + (put job 'state 'waiting-dep) + (if (coq-par-dependencies-ready job) + (progn + (when coq--debug-auto-compilation + (message "%s: coqc dependencies finished" (get job 'name))) + (coq-par-compile-job-maybe job)) + (when coq--debug-auto-compilation + (message "%s: wait for %d dependencies" + (get job 'name) (get job 'coqc-dependency-count)))))) (defun coq-par-coqc-continuation (process exit-status) - "Coqc Continuation function. -Signal an error, if coqc failed. Otherwise, trigger the -transition 'enqueued-coqc -> 'waiting-queue for the job behind -PROCESS." - (if (eq exit-status 0) - ;; coqc success - (coq-par-kickoff-coqc-dependants - (process-get process 'coq-compilation-job) - 'just-compiled) - ;; coqc error - (coq-init-compile-response-buffer - (mapconcat 'identity (process-get process 'coq-process-command) " ")) - (let ((inhibit-read-only t)) - (with-current-buffer coq-compile-response-buffer - (insert (process-get process 'coq-process-output)))) - (coq-display-compile-response-buffer) - (signal 'coq-compile-error-coqc - (get (process-get process 'coq-compilation-job) 'src-file)))) + "Coqc continuation function. +If coqc failed, signal an error or mark the job as 'failed, and +unlock ancestors as appropriate. If coqc was successful, trigger +the transition 'enqueued-coqc -> 'waiting-queue for the job +behind PROCESS." + (let ((job (process-get process 'coq-compilation-job))) + (if (eq exit-status 0) + (progn + ;; coqc success + (when (get job 'vio2vo-needed) + (coq-par-vio2vo-enqueue job)) + (coq-par-kickoff-coqc-dependants job 'just-compiled)) + ;; coqc error + (coq-compile-display-error + (mapconcat 'identity (process-get process 'coq-process-command) " ") + (process-get process 'coq-process-output) + t) + (if coq-compile-keep-going + (progn + (coq-par-mark-job-failing job) + (coq-par-kickoff-coqc-dependants + job + (get job 'youngest-coqc-dependency))) + (signal 'coq-compile-error-coqc + (get (process-get process 'coq-compilation-job) 'src-file)))))) + +(defun coq-par-vio2vo-continuation (process exit-status) + "vio2vo continuation function." + (let ((job (process-get process 'coq-compilation-job))) + (if (eq exit-status 0) + ;; success - nothing to do + (when coq--debug-auto-compilation + (message "%s: vio2vo finished successfully" (get job 'name))) + (when coq--debug-auto-compilation + (message "%s: vio2vo failed" (get job 'name))) + (coq-compile-display-error + (concat + "cd " + (file-name-directory (file-truename (get job 'src-file))) + "; " + (mapconcat 'identity (process-get process 'coq-process-command) " ")) + (process-get process 'coq-process-output) + t) + ;; don't signal an error or abort other vio2vo processes + ))) ;;; handle Require commands when queue is extended -(defun coq-par-handle-module (module-id span) +(defun coq-par-handle-module (module-id span &optional from) "Handle compilation of module MODULE-ID. This function translates MODULE-ID to a file name. If compilation for this file is not ignored, a new top-level compilation job is created. If there is a new top-level compilation job, it is saved -in `coq-last-compilation-job'. +in `coq--last-compilation-job'. This function must be evaluated with the buffer that triggered the compilation as current, otherwise a wrong `coq-load-path' might be used." - (let ((module-obj-file - (coq-par-map-module-id-to-obj-file module-id coq-load-path)) + (when coq--debug-auto-compilation + (if from + (message "handle required module \"%s\" from \"%s\"" module-id from) + (message "handle required module \"%s\" without from clause" module-id))) + (let ((module-vo-file + (coq-par-map-module-id-to-vo-file module-id coq-load-path from)) module-job) - (if coq-debug-auto-compilation - (message "check compilation for module %s from object file %s" - module-id module-obj-file)) - ;; coq-par-map-module-id-to-obj-file currently returns () for + (when coq--debug-auto-compilation + (if module-vo-file + (message "check compilation for module %s from object file %s" + module-id module-vo-file) + (message "nothing to check for module %s" module-id))) + ;; coq-par-map-module-id-to-vo-file currently returns () for ;; standard library modules! - (when (and module-obj-file - (not (coq-compile-ignore-file module-obj-file))) + (when (and module-vo-file + (not (coq-compile-ignore-file module-vo-file))) (setq module-job - (coq-par-create-library-job module-obj-file coq-load-path - coq-last-compilation-job span + (coq-par-create-library-job module-vo-file coq-load-path + coq--last-compilation-job span "scripting buffer")) - (setq coq-last-compilation-job module-job) - (if coq-debug-auto-compilation - (message "%s: this job is the last compilation job now" - (get coq-last-compilation-job 'name)))))) + (setq coq--last-compilation-job module-job) + (when coq--debug-auto-compilation + (message "%s: this job is the last compilation job now" + (get coq--last-compilation-job 'name)))))) (defun coq-par-handle-require-list (require-items) "Start compilation for the required modules in the car of REQUIRE-ITEMS. @@ -1225,17 +1820,20 @@ to file names and creates one top-level compilation job for each required module that is not ignored (eg via `coq-compile-ignored-directories'). Jobs are started immediately if possible. The last such created job is remembered in -`coq-last-compilation-job'. The REQUIRE-ITEMS are attached to +`coq--last-compilation-job'. The REQUIRE-ITEMS are attached to this last top-level job or directly to proof-action-list, if there is no last compilation job." (let* ((item (car require-items)) (string (mapconcat 'identity (nth 1 item) " ")) (span (car item)) - start) + prefix start) + (when coq--debug-auto-compilation + (message "handle require command \"%s\"" string)) ;; We know there is a require in string. But we have to match it ;; again in order to get the end position. (string-match coq-require-command-regexp string) (setq start (match-end 0)) + (setq prefix (match-string 1 string)) (span-add-delete-action span `(lambda () @@ -1243,21 +1841,27 @@ there is no last compilation job." ;; add a compilation job for all required modules (while (string-match coq-require-id-regexp string start) (setq start (match-end 0)) - (coq-par-handle-module (match-string 1 string) span)) + (coq-par-handle-module (match-string 1 string) span prefix)) ;; add the asserted items to the last compilation job - (if coq-last-compilation-job + (if coq--last-compilation-job (progn - (assert (not (coq-par-job-is-ready coq-last-compilation-job))) - (put coq-last-compilation-job 'queueitems require-items) - (if coq-debug-auto-compilation - (message "%s: attach %s items" - (get coq-last-compilation-job 'name) - (length require-items)))) + (assert (not (coq-par-job-is-ready coq--last-compilation-job)) + nil "last compilation job from previous compilation ready") + (put coq--last-compilation-job 'queueitems + (nconc (get coq--last-compilation-job 'queueitems) + require-items)) + (when coq--debug-auto-compilation + (message "%s: attach %s items (containing now %s items)" + (get coq--last-compilation-job 'name) + (length require-items) + (length (get coq--last-compilation-job 'queueitems))))) ;; or add them directly to queueitems if there is no compilation job ;; (this happens if the modules are ignored for compilation) (setq queueitems (nconc queueitems require-items)) - (if coq-debug-auto-compilation - (message "attach %s items to queueitems" (length require-items)))))) + (when coq--debug-auto-compilation + (message "attach %s items to queueitems (containing now %s items)" + (length require-items) + (length queueitems)))))) (defun coq-par-item-require-predicate (item) @@ -1279,7 +1883,7 @@ If `coq-compile-before-require' is non-nil, this function starts the compilation (if necessary) of the dependencies ansynchronously in parallel in the background. -If there is a last compilation job (`coq-last-compilation-job') +If there is a last compilation job (`coq--last-compilation-job') then the queue region is extended, while some background compilation is still running. In this case I have to preserve the internal state. Otherwise the hash of the compilation jobs and @@ -1297,44 +1901,52 @@ first of these batches, buffers are saved with Finally, `proof-second-action-list-active' is set if I keep some queue items because they have to wait for a compilation job. Then the maximal number of background compilation jobs is started." - (when coq-debug-auto-compilation + (when coq--debug-auto-compilation (message "%d items were added to the queue, scan for require" (length queueitems))) - (unless coq-last-compilation-job + (unless coq--last-compilation-job (coq-par-init-compilation-hash) - (coq-par-init-ancestor-hash)) + (coq-init-compile-response-buffer)) (let ((splitted-items (split-list-at-predicate queueitems 'coq-par-item-require-predicate))) - (if coq-last-compilation-job + (if coq--last-compilation-job (progn - (put coq-last-compilation-job 'queueitems - (nconc (get coq-last-compilation-job 'queueitems) + (put coq--last-compilation-job 'queueitems + (nconc (get coq--last-compilation-job 'queueitems) (car splitted-items))) (setq queueitems nil) (message "attach first %s items to job %s" (length (car splitted-items)) - (get coq-last-compilation-job 'name))) + (get coq--last-compilation-job 'name))) (setq queueitems (car splitted-items)) - (if coq-debug-auto-compilation - (message "attach first %s items directly to queue" - (length (car splitted-items))))) + (when coq--debug-auto-compilation + (message "attach first %s items directly to queue" + (length (car splitted-items))))) ;; XXX handle external compilation here, compile everything ;; with one command, use compilation-finish-functions to get ;; notification (when (cdr splitted-items) + (when coq--compile-vio2vo-delay-timer + (cancel-timer coq--compile-vio2vo-delay-timer) + (setq coq--compile-vio2vo-delay-timer nil)) + (when coq--compile-vio2vo-in-progress + (assert (not coq--last-compilation-job) + nil "normal compilation and vio2vo in parallel 2") + ;; there are only vio2vo background processes + (coq-par-kill-all-processes) + (setq coq--compile-vio2vo-in-progress nil)) ;; save buffers before invoking the first coqdep (coq-compile-save-some-buffers) - (mapc (lambda (require-items) - (coq-par-handle-require-list require-items)) - (cdr splitted-items))) - (when coq-last-compilation-job + (dolist (require-items (cdr splitted-items)) + (coq-par-handle-require-list require-items))) + (when coq--last-compilation-job (setq proof-second-action-list-active t)) (coq-par-start-jobs-until-full) - (if coq-debug-auto-compilation - (if coq-last-compilation-job - (message "return control, waiting for background jobs") - (message "return control, no background jobs"))))) + (when coq--debug-auto-compilation + (if coq--last-compilation-job + (message "return control, waiting for background jobs") + (message "return control, no background jobs"))))) (defun coq-par-preprocess-require-commands () "Coq function for `proof-shell-extend-queue-hook' doing parallel compilation. @@ -1349,6 +1961,17 @@ does the error checking/reporting for (coq-compile-error (coq-par-emergency-cleanup) (message "%s %s" (get (car err) 'error-message) (cdr err))) + (coq-unclassifiable-version + (coq-par-emergency-cleanup) + (if (equal (cdr err) "trunk") + (message + (concat "your Coq version \"trunk\" is too unspecific for " + "Proof General; please customize coq-pinned-version")) + (message "%s \"%s\"; consider customizing coq-pinned-version" + (get (car err) 'error-message) (cdr err)))) + (file-error + (coq-par-emergency-cleanup) + (message "Error: %s" (mapconcat 'identity (cdr err) ": "))) (error (message "unexpected error during parallel compilation: %s" err) diff --git a/coq/coq-par-test.el b/coq/coq-par-test.el new file mode 100644 index 00000000..f60baacf --- /dev/null +++ b/coq/coq-par-test.el @@ -0,0 +1,953 @@ +;; coq-par-test.el --- tests for parallel compilation +;; Copyright (C) 2016 Hendrik Tews +;; Authors: Hendrik Tews +;; License: GPL (GNU GENERAL PUBLIC LICENSE) +;; Maintainer: Hendrik Tews <hendrik@askra.de> +;; +;;; Commentary: +;; +;; This file file contains tests for `coq-par-job-needs-compilation'. +;; It specifies for all combinations of `coq-compile-quick', existing +;; files and relative file ages the required result and side effects +;; of `coq-par-job-needs-compilation'. +;; +;; Run the tests with +;; emacs -batch -L . -L ../generic -L ../lib -load coq-par-test.el +;; +;;; TODO: +;; +;; - integrate into PG build and test(?) system + + +(require 'coq-par-compile) + +(defconst coq--par-job-needs-compilation-tests + ;; for documentation see the doc string following the init value + '( + ;; present files | compilation? | delete | 'req-obj-file + ;; ==================================================================== + ;; all of src dep vo vio present + ((src dep vo vio) + (no-quick nil nil vo ) + (quick nil nil vo ) + (ensure-vo nil vio vo )) + + ((src dep vio vo) + (no-quick nil nil vio) + (quick nil nil vio) + (ensure-vo nil nil vo )) + + ((src vo dep vio) + (no-quick nil vo vio) + (quick nil vo vio) + (ensure-vo t nil vo )) + + ((src vo vio dep) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((src vio dep vo) + (no-quick nil vio vo ) + (quick nil vio vo ) + (ensure-vo nil vio vo )) + + ((src vio vo dep) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ;; present files | compilation? | delete | 'req-obj-file + ((dep src vio vo) + (no-quick nil nil vio) + (quick nil nil vio) + (ensure-vo nil nil vo )) + + ((dep src vo vio) + (no-quick nil nil vo ) + (quick nil nil vo ) + (ensure-vo nil vio vo )) + + ((dep vo vio src) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((dep vo src vio) + (no-quick nil vo vio) + (quick nil vo vio) + (ensure-vo t nil vo )) + + ((dep vio vo src) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((dep vio src vo) + (no-quick nil vio vo ) + (quick nil vio vo ) + (ensure-vo nil vio vo )) + + ((vo src dep vio) + (no-quick nil vo vio) + (quick nil vo vio) + (ensure-vo t nil vo )) + + ;; present files | compilation? | delete | 'req-obj-file + ((vo src vio dep) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((vo dep src vio) + (no-quick nil vo vio ) + (quick nil vo vio ) + (ensure-vo t nil vo )) + + ((vo dep vio src) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((vo vio src dep) + (no-quick t vio vo ) + (quick t vo vio ) + (ensure-vo t vio vo )) + + ((vo vio dep src) + (no-quick t vio vo ) + (quick t vo vio ) + (ensure-vo t vio vo )) + + ((vio src vo dep) + (no-quick t vio vo ) + (quick t vo vio ) + (ensure-vo t vio vo )) + + ((vio src dep vo) + (no-quick nil vio vo ) + (quick nil vio vo ) + (ensure-vo nil vio vo )) + + ((vio dep vo src) + (no-quick t vio vo ) + (quick t vo vio ) + (ensure-vo t vio vo )) + + ;; present files | compilation? | delete | 'req-obj-file + ((vio dep src vo) + (no-quick nil vio vo ) + (quick nil vio vo ) + (ensure-vo nil vio vo )) + + ((vio vo dep src) + (no-quick t vio vo ) + (quick t vo vio ) + (ensure-vo t vio vo )) + + ((vio vo src dep) + (no-quick t vio vo ) + (quick t vo vio ) + (ensure-vo t vio vo )) + + + ;; only src dep vo present + ((src dep vo) + (no-quick nil nil vo ) + (quick nil nil vo ) + (ensure-vo nil nil vo )) + + ((src vo dep) + (no-quick t nil vo ) + (quick t vo vio ) + (ensure-vo t nil vo )) + + ((dep src vo) + (no-quick nil nil vo ) + (quick nil nil vo ) + (ensure-vo nil nil vo )) + + ((dep vo src) + (no-quick t nil vo ) + (quick t vo vio ) + (ensure-vo t nil vo )) + + ((vo src dep) + (no-quick t nil vo ) + (quick t vo vio ) + (ensure-vo t nil vo )) + + ((vo dep src) + (no-quick t nil vo ) + (quick t vo vio ) + (ensure-vo t nil vo )) + + + ;; present files | compilation? | delete | 'req-obj-file + ;; only src dep vio present + ((src dep vio) + (no-quick nil nil vio ) + (quick nil nil vio ) + (ensure-vo t nil vo )) + + ((src vio dep) + (no-quick t vio vo ) + (quick t nil vio ) + (ensure-vo t vio vo )) + + ((dep src vio) + (no-quick nil nil vio ) + (quick nil nil vio ) + (ensure-vo t nil vo )) + + ((dep vio src) + (no-quick t vio vo ) + (quick t nil vio ) + (ensure-vo t vio vo )) + + ((vio src dep) + (no-quick t vio vo ) + (quick t nil vio ) + (ensure-vo t vio vo )) + + ((vio dep src) + (no-quick t vio vo ) + (quick t nil vio ) + (ensure-vo t vio vo )) + + + ;; present files | compilation? | delete | 'req-obj-file + ;; only src vo vio present + ((src vo vio) + (no-quick nil nil vo ) + (quick nil nil vo ) + (ensure-vo nil vio vo )) + + ((src vio vo) + (no-quick nil nil vio) + (quick nil nil vio) + (ensure-vo nil nil vo )) + + ((vo src vio) + (no-quick nil vo vio ) + (quick nil vo vio ) + (ensure-vo t nil vo )) + + ((vo vio src) + (no-quick t vio vo ) + (quick t vo vio ) + (ensure-vo t vio vo )) + + ((vio src vo) + (no-quick nil vio vo ) + (quick nil vio vo ) + (ensure-vo nil vio vo )) + + ((vio vo src) + (no-quick t vio vo ) + (quick t vo vio ) + (ensure-vo t vio vo )) + + + ;; present files | compilation? | delete | 'req-obj-file + ;; only src dep present + ((src dep) + (no-quick t nil vo ) + (quick t nil vio ) + (ensure-vo t nil vo )) + + ((dep src) + (no-quick t nil vo ) + (quick t nil vio ) + (ensure-vo t nil vo )) + + + ;; only src vo present + ((src vo) + (no-quick nil nil vo ) + (quick nil nil vo ) + (ensure-vo nil nil vo )) + + ((vo src) + (no-quick t nil vo ) + (quick t vo vio ) + (ensure-vo t nil vo )) + + + ;; only src vio present + ((src vio) + (no-quick nil nil vio ) + (quick nil nil vio ) + (ensure-vo t nil vo )) + + ((vio src) + (no-quick t vio vo ) + (quick t nil vio ) + (ensure-vo t vio vo )) + + + ;; only src present + ((src) + (no-quick t nil vo ) + (quick t nil vio ) + (ensure-vo t nil vo )) + + ;; present files | compilation? | delete | 'req-obj-file + ;; + ;; test cases for some objects with identical time stamp + ;; + ;; 4 files with same time stamp + (((src vo dep vio)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ;; 3 files with same time stamp + (((src vo dep) vio) + (no-quick nil vo vio ) + (quick nil vo vio ) + (ensure-vo t nil vo )) + + ((vio (src vo dep)) + (no-quick t vio vo ) + (quick t vo vio ) + (ensure-vo t vio vo )) + + (((src vo vio) dep) + (no-quick t vio vo ) + (quick t vo vio ) + (ensure-vo t vio vo )) + + ((dep (src vo vio)) + (no-quick t vio vo ) + (quick t vo vio ) + (ensure-vo t vio vo )) + + (((src dep vio) vo) + (no-quick nil vio vo ) + (quick nil vio vo ) + (ensure-vo nil vio vo )) + + ;; present files | compilation? | delete | 'req-obj-file + ((vo (src dep vio)) + (no-quick t vio vo ) + (quick t vo vio ) + (ensure-vo t vio vo )) + + (((vo dep vio) src) + (no-quick t vio vo ) + (quick t vo vio ) + (ensure-vo t vio vo )) + + ((src (vo dep vio)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ;; 2 times 2 files with same time stamp + (((src vo) (dep vio)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + (((dep vio) (src vo)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + (((src dep) (vo vio)) + ;; could also use the vio as 'req-obj-file in the first 2 cases here + (no-quick nil nil vo ) + (quick nil nil vo ) + (ensure-vo nil vio vo )) + + (((vo vio) (src dep)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + (((src vio) (vo dep)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ;; present files | compilation? | delete | 'req-obj-file + (((vo dep) (src vio)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ;; 2 files with same time stamp + (((src vo) dep vio) + (no-quick nil vo vio) + (quick nil vo vio) + (ensure-vo t nil vo )) + + (((src vo) vio dep) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((dep (src vo) vio) + (no-quick nil vo vio) + (quick nil vo vio) + (ensure-vo t nil vo )) + + ((dep vio (src vo)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((vio (src vo) dep) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((vio dep (src vo)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ;; present files | compilation? | delete | 'req-obj-file + (((src dep) vo vio) + (no-quick nil nil vo ) + (quick nil nil vo ) + (ensure-vo nil vio vo )) + + (((src dep) vio vo) + (no-quick nil nil vio) + (quick nil nil vio) + (ensure-vo nil nil vo )) + + ((vo (src dep) vio) + (no-quick nil vo vio) + (quick nil vo vio) + (ensure-vo t nil vo )) + + ((vo vio (src dep)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((vio (src dep) vo) + (no-quick nil vio vo ) + (quick nil vio vo ) + (ensure-vo nil vio vo )) + + ((vio vo (src dep)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + (((src vio) vo dep) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + (((src vio) dep vo) + (no-quick nil vio vo ) + (quick nil vio vo ) + (ensure-vo nil vio vo )) + + ((vo (src vio) dep) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ;; present files | compilation? | delete | 'req-obj-file + ((vo dep (src vio)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((dep (src vio) vo) + (no-quick nil vio vo ) + (quick nil vio vo ) + (ensure-vo nil vio vo )) + + ((dep vo (src vio)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + (((vo dep) src vio) + (no-quick nil vo vio ) + (quick nil vo vio ) + (ensure-vo t nil vo )) + + (((vo dep) vio src) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((src (vo dep) vio) + (no-quick nil vo vio) + (quick nil vo vio) + (ensure-vo t nil vo )) + + ((src vio (vo dep)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((vio (vo dep) src) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((vio src (vo dep)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ;; present files | compilation? | delete | 'req-obj-file + (((vo vio) src dep) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + (((vo vio) dep src) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((src (vo vio) dep) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((src dep (vo vio)) + ;; could also use the vio as 'req-obj-file in the first 2 cases here + (no-quick nil nil vo ) + (quick nil nil vo ) + (ensure-vo nil vio vo )) + + ((dep (vo vio) src) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((dep src (vo vio)) + ;; could also use the vio as 'req-obj-file in the first 2 cases here + (no-quick nil nil vo ) + (quick nil nil vo ) + (ensure-vo nil vio vo )) + + (((dep vio) src vo) + (no-quick nil vio vo ) + (quick nil vio vo ) + (ensure-vo nil vio vo )) + + (((dep vio) vo src) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((src (dep vio) vo) + (no-quick nil vio vo ) + (quick nil vio vo ) + (ensure-vo nil vio vo )) + + ;; present files | compilation? | delete | 'req-obj-file + ((src vo (dep vio)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((vo (dep vio) src) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((vo src (dep vio)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ;; 2 files with the same time stamp out of 3 files + ;; without vio + (((src dep vo)) + (no-quick t nil vo ) + (quick t vo vio) + (ensure-vo t nil vo )) + + (((src dep) vo) + (no-quick nil nil vo ) + (quick nil nil vo ) + (ensure-vo nil nil vo )) + + ((vo (src dep)) + (no-quick t nil vo ) + (quick t vo vio) + (ensure-vo t nil vo )) + + (((src vo) dep) + (no-quick t nil vo ) + (quick t vo vio) + (ensure-vo t nil vo )) + + ((dep (src vo)) + (no-quick t nil vo ) + (quick t vo vio) + (ensure-vo t nil vo )) + + (((dep vo) src) + (no-quick t nil vo ) + (quick t vo vio) + (ensure-vo t nil vo )) + + ;; present files | compilation? | delete | 'req-obj-file + ((src (dep vo)) + (no-quick t nil vo ) + (quick t vo vio) + (ensure-vo t nil vo )) + + ;; without vo + (((src dep vio)) + (no-quick t vio vo ) + (quick t nil vio) + (ensure-vo t vio vo )) + + (((src dep) vio) + (no-quick nil nil vio ) + (quick nil nil vio ) + (ensure-vo t nil vo )) + + ((vio (src dep)) + (no-quick t vio vo ) + (quick t nil vio) + (ensure-vo t vio vo )) + + (((src vio) dep) + (no-quick t vio vo ) + (quick t nil vio) + (ensure-vo t vio vo )) + + ((dep (src vio)) + (no-quick t vio vo ) + (quick t nil vio) + (ensure-vo t vio vo )) + + (((dep vio) src) + (no-quick t vio vo ) + (quick t nil vio) + (ensure-vo t vio vo )) + + ((src (dep vio)) + (no-quick t vio vo ) + (quick t nil vio) + (ensure-vo t vio vo )) + + ;; without dep + (((src vio vo)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + (((src vio) vo) + (no-quick nil vio vo ) + (quick nil vio vo ) + (ensure-vo nil vio vo )) + + ((vo (src vio)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + (((src vo) vio) + (no-quick nil vo vio ) + (quick nil vo vio ) + (ensure-vo t nil vo )) + + ;; present files | compilation? | delete | 'req-obj-file + ((vio (src vo)) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + (((vio vo) src) + (no-quick t vio vo ) + (quick t vo vio) + (ensure-vo t vio vo )) + + ((src (vio vo)) + ;; could also use the vio as 'req-obj-file in the first 2 cases here + (no-quick nil nil vo ) + (quick nil nil vo ) + (ensure-vo nil vio vo )) + + ;; 2 files with identical time stamp out of 2 files + (((src dep)) + (no-quick t nil vo ) + (quick t nil vio ) + (ensure-vo t nil vo )) + + (((src vo)) + (no-quick t nil vo ) + (quick t vo vio ) + (ensure-vo t nil vo )) + + (((src vio)) + (no-quick t vio vo ) + (quick t nil vio ) + (ensure-vo t vio vo )) + ) + "Test and result specification for `coq-par-job-needs-compilation'. + +List of tests. A test is a list of 4 elements. The first element, +a list, specifies the existing files and their relative age. In +there, `src' stands for the source (x.v) file, `dep' for +a (already compiled) dependency (dep.vo or dep.vio), `vo' for the +.vo file (x.vo) and `vio' for the .vio file (x.vio). A label in +the list denotes an existing file, a missing label a missing +file. The first element is the oldest file, the last element the +newest file. A sublist specifies a set of files with identical +time stamps. For example, ``(src (vo vio) dep)'' specifies source +is older than .vo and .vio, .vo and .vio have identical last +modification time stamps and .vo and .vio are older than the +dependency. + +Elements 2-4 of a test specify the results and side effects of +`coq-par-job-needs-compilation' for all setting of +`coq-compile-quick' on the file configuration described in +element 1. The options `quick-no-vio2vo' and `quick-and-vio2vo' +are specified together with label `quick'. Each result and side +effect specification (also called a variant in the source code +below) is itself a list of 4 elements. Element 1 is the value for +`coq-compile-quick', where `quick' denotes both `quick-no-vio2vo' +and `quick-and-vio2vo'. Element 2 specifies the result of +`coq-par-job-needs-compilation', nil for don't compile, t for do +compile. Elements 3-5 specify side effects. Element 3 which file +must be deleted, where nil means no file must be deleted. Element +4 specifies which file name must be stored in the +`required-obj-file' property of the job. This file will be used +as the compiled module library. In case compilation is +needed (element 2 equals t), this is the target of the +compilation. + +This list contains 1 test for all possible file configuration and +relative ages.") + +(defun coq-par-test-flatten-files (file-descr) + "Flatten a file description test case list into a list of files." + (let (result) + (dolist (f file-descr result) + (if (listp f) + (setq result (append f result)) + (push f result))))) + +(defun test-coq-par-test-data-invarint () + "Wellformedness check for the test specifications." + (mapc + (lambda (test) + (let ((test-id (format "%s" (car test)))) + ;; a test is a list of 4 elements and the first element is a list itself + (assert + (and + (eq (length test) 4) + (listp (car test))) + nil (concat test-id " 1")) + (mapc + (lambda (variant) + ;; a variant is a list of 4 elements + (assert (eq (length variant) 4) nil (concat test-id " 2")) + (let ((files (coq-par-test-flatten-files (car test))) + (quick-mode (car variant)) + (compilation-result (nth 1 variant)) + (delete-result (nth 2 variant)) + (req-obj-result (nth 3 variant))) + ;; the delete field, when set, must be a member of the files list + (assert (or (not delete-result) + (member delete-result files)) + nil (concat test-id " 3")) + ;; 8.4 compatibility check + (when (and (or (eq quick-mode 'no-quick) (eq quick-mode 'ensure-vo)) + (not (member 'vio files))) + (assert (not delete-result) + nil (concat test-id " 4")) + (assert (eq compilation-result + (not (eq (car (last (car test))) 'vo))) + nil (concat test-id " 5"))))) + (cdr test)))) + coq--par-job-needs-compilation-tests)) + +(defun test-coq-par-sym-to-file (dir sym) + "Convert a test file symbol SYM to a file name in directory DIR." + (let ((file (cond + ((eq sym 'src) "a.v") + ((eq sym 'dep) "dep.vo") + ((eq sym 'vo) "a.vo") + ((eq sym 'vio) "a.vio") + (t (assert nil))))) + (concat dir "/" file))) + +(defun test-coq-par-one-test (counter dir file-descr variant dep-just-compiled) + "Do one test for one specific `coq-compile-quick' value. + +This function creates the files in DIR, sets up a job with the +necessary fields, calls `coq--par-job-needs-compilation-tests' and +test the result and side effects wth `assert'." + (let ((id (format "%s: %s %s%s" counter (car variant) file-descr + (if dep-just-compiled " just" ""))) + (job (make-symbol "coq-compile-job-symbol")) + (module-vo-file (concat dir "/a.vo")) + (quick-mode (car variant)) + (compilation-result (nth 1 variant)) + (delete-result (nth 2 variant)) + (req-obj-result (nth 3 variant)) + (different-counter 5) + (same-counter 5) + (different-not-ok t) + (same-not-ok t) + (last-different-time-stamp '(0 0)) + (file-descr-flattened (coq-par-test-flatten-files file-descr)) + same-time-stamp file-list + obj-mod-result result) + (message "test case %s/576: %s %s%s" counter (car variant) file-descr + (if dep-just-compiled " just" "")) + (when (not compilation-result) + (setq obj-mod-result req-obj-result)) + (ignore-errors + (delete-directory dir t)) + (make-directory dir) + (setq coq-compile-quick quick-mode) + (put job 'vo-file module-vo-file) + (put job 'src-file (coq-library-src-of-vo-file module-vo-file)) + (put job 'youngest-coqc-dependency '(0 0)) + (put job 'name id) + ;; create files in order + (while different-not-ok + ;; (message "enter different loop %s at %s" + ;; different-counter (current-time)) + (setq different-not-ok nil) + (setq different-counter (1- different-counter)) + (assert (> different-counter 0) + nil "create files with different time stamps failed") + (dolist (same-descr file-descr) + (when (symbolp same-descr) + (setq same-descr (list same-descr))) + (setq file-list + (mapcar (lambda (sym) (test-coq-par-sym-to-file dir sym)) + same-descr)) + ;; (message "try %s files %s" same-descr file-list) + (setq same-counter 5) + (setq same-not-ok t) + (while same-not-ok + (setq same-counter (1- same-counter)) + (assert (> same-counter 0) + nil "create files with same time stamp filed") + (dolist (file file-list) + (with-temp-file file t)) + ;; check now that all the files in file-list have the same time stamp + (setq same-not-ok nil) + (setq same-time-stamp (nth 5 (file-attributes (car file-list)))) + ;; (message "got first time stamp %s" same-time-stamp) + (dolist (file (cdr file-list)) + (let ((ots (nth 5 (file-attributes file)))) + ;; (message "got other time stamp %s" ots) + (unless (equal same-time-stamp ots) + (setq same-not-ok t))))) + ;; (message "successful finished %s" same-descr) + (when (member 'dep same-descr) + (put job 'youngest-coqc-dependency + (nth 5 (file-attributes (test-coq-par-sym-to-file dir 'dep))))) + ;; (message "XX %s < %s = %s" + ;; last-different-time-stamp same-time-stamp + ;; (time-less-p last-different-time-stamp same-time-stamp)) + (unless (time-less-p last-different-time-stamp same-time-stamp) + ;; error - got the same time stamp + ;; (message "unsuccsessful - need different retry") + (setq different-not-ok t)) + (setq last-different-time-stamp same-time-stamp) + (sleep-for 0 15))) + (when dep-just-compiled + (put job 'youngest-coqc-dependency 'just-compiled)) + (setq result (coq-par-job-needs-compilation job)) + ;; check result + (assert (eq result compilation-result) + nil (concat id " result")) + ;; check file deletion + (assert (or (not delete-result) + (not (file-attributes + (test-coq-par-sym-to-file dir delete-result)))) + nil (concat id " delete file")) + ;; check no other file is deleted + (dolist (f file-descr-flattened) + (unless (eq f delete-result) + (assert (file-attributes (test-coq-par-sym-to-file dir f)) + nil (format "%s non del file %s: %s" + id f + (test-coq-par-sym-to-file dir f))))) + ;; check value of 'required-obj-file property + (assert (equal (get job 'required-obj-file) + (test-coq-par-sym-to-file dir req-obj-result)) + nil (concat id " required-obj-file")) + ;; check 'obj-mod-time property + (if obj-mod-result + (assert + (equal + (get job 'obj-mod-time) + (nth 5 (file-attributes + (test-coq-par-sym-to-file dir obj-mod-result)))) + nil (concat id " obj-mod-time non nil")) + (assert (not (get job 'obj-mod-time)) + nil (concat id " obj-mod-time nil"))) + ;; check 'use-quick property + (assert (eq (not (not (and compilation-result (eq req-obj-result 'vio)))) + (get job 'use-quick)) + nil (concat id " use-quick")) + ;; check vio2vo-needed property + (assert (eq + (and (eq quick-mode 'quick-and-vio2vo) + (eq req-obj-result 'vio) + (or (eq delete-result 'vo) + (not (member 'vo file-descr-flattened)))) + (get job 'vio2vo-needed)) + nil (concat id " vio2vo-needed wrong")) + (ignore-errors + (delete-directory dir t)))) + +(defvar test-coq-par-counter 0 + "Stupid counter.") + +(defun test-coq-par-one-spec (dir files variant dep-just-compiled) + "Run one test for one variant and split it for the 2 quick settings." + (if (eq (car variant) 'quick) + (progn + (test-coq-par-one-test test-coq-par-counter dir files + (cons 'quick-no-vio2vo (cdr variant)) + dep-just-compiled) + (setq test-coq-par-counter (1+ test-coq-par-counter)) + (test-coq-par-one-test test-coq-par-counter dir files + (cons 'quick-and-vio2vo (cdr variant)) + dep-just-compiled)) + (test-coq-par-one-test test-coq-par-counter dir files variant + dep-just-compiled)) + (setq test-coq-par-counter (1+ test-coq-par-counter))) + +(defun test-coq-par-job-needs-compilation (dir) + "Check test data wellformedness and run all the tests." + (test-coq-par-test-data-invarint) + (setq test-coq-par-counter 1) + (mapc + (lambda (test) + (mapc + (lambda (variant) + (test-coq-par-one-spec dir (car test) variant nil) + (when (eq (car (last (car test))) 'dep) + (test-coq-par-one-spec dir (car test) variant t))) + (cdr test))) + coq--par-job-needs-compilation-tests)) + +(condition-case err + (progn + (test-coq-par-job-needs-compilation (make-temp-name "/tmp/coq-par-test")) + (message "test completed successfully")) + (error + (message "test failed with %s" err) + (kill-emacs 1))) + + +(provide 'coq-par-test) + +;;; coq-par-test.el ends here diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el index e00a2793..a1b2d30a 100644 --- a/coq/coq-seq-compile.el +++ b/coq/coq-seq-compile.el @@ -64,7 +64,7 @@ error occurred and the returned list is the (possibly empty) list of file names LIB-SRC-FILE depends on. If an error occurs this funtion displays -`coq-compile-response-buffer' with the complete command and its +`coq--compile-response-buffer' with the complete command and its output. The optional argument COMMAND-INTRO is only used in the error case. It is prepended to the displayed command. @@ -77,17 +77,17 @@ break." (nconc (coq-include-options coq-load-path (file-name-directory lib-src-file) (coq--pre-v85)) (list lib-src-file))) coqdep-status coqdep-output) - (if coq-debug-auto-compilation - (message "call coqdep arg list: %S" coqdep-arguments)) + (when coq--debug-auto-compilation + (message "call coqdep arg list: %S" coqdep-arguments)) (with-temp-buffer (setq coqdep-status (apply 'call-process coq-dependency-analyzer nil (current-buffer) nil coqdep-arguments)) (setq coqdep-output (buffer-string))) - (if coq-debug-auto-compilation - (message "coqdep status %s, output on %s: %s" - coqdep-status lib-src-file coqdep-output)) + (when coq--debug-auto-compilation + (message "coqdep status %s, output on %s: %s" + coqdep-status lib-src-file coqdep-output)) (if (or (not (eq coqdep-status 0)) (string-match coq-coqdep-error-regexp coqdep-output)) @@ -99,7 +99,7 @@ break." (coq-init-compile-response-buffer (mapconcat 'identity full-command " ")) (let ((inhibit-read-only t)) - (with-current-buffer coq-compile-response-buffer + (with-current-buffer coq--compile-response-buffer (insert coqdep-output))) (coq-display-compile-response-buffer) "unsatisfied dependencies") @@ -109,7 +109,7 @@ break." (defun coq-seq-compile-library (src-file) "Recompile coq library SRC-FILE. -Display errors in buffer `coq-compile-response-buffer'." +Display errors in buffer `coq--compile-response-buffer'." (message "Recompile %s" src-file) (let ((coqc-arguments (nconc @@ -118,16 +118,16 @@ Display errors in buffer `coq-compile-response-buffer'." coqc-status) (coq-init-compile-response-buffer (mapconcat 'identity (cons coq-compiler coqc-arguments) " ")) - (if coq-debug-auto-compilation - (message "call coqc arg list: %s" coqc-arguments)) + (when coq--debug-auto-compilation + (message "call coqc arg list: %s" coqc-arguments)) (setq coqc-status (apply 'call-process - coq-compiler nil coq-compile-response-buffer t coqc-arguments)) - (if coq-debug-auto-compilation - (message "compilation %s exited with %s, output |%s|" - src-file coqc-status - (with-current-buffer coq-compile-response-buffer - (buffer-string)))) + coq-compiler nil coq--compile-response-buffer t coqc-arguments)) + (when coq--debug-auto-compilation + (message "compilation %s exited with %s, output |%s|" + src-file coqc-status + (with-current-buffer coq--compile-response-buffer + (buffer-string)))) (unless (eq coqc-status 0) (coq-display-compile-response-buffer) (let ((terminated-text (if (numberp coqc-status) @@ -178,8 +178,8 @@ OBJ have identical modification times." (progn (coq-seq-compile-library src) 'just-compiled) - (if coq-debug-auto-compilation - (message "Skip compilation of %s" src)) + (when coq--debug-auto-compilation + (message "Skip compilation of %s" src)) obj-time)))) (defun coq-seq-make-lib-up-to-date (coq-obj-hash span lib-obj-file) @@ -202,8 +202,8 @@ function." (let ((result (gethash lib-obj-file coq-obj-hash))) (if result (progn - (if coq-debug-auto-compilation - (message "Checked %s already" lib-obj-file)) + (when coq--debug-auto-compilation + (message "Checked %s already" lib-obj-file)) result) ;; lib-obj-file has not been checked -- do it now (message "Check %s" lib-obj-file) @@ -212,7 +212,7 @@ function." (setq result '(0 0)) (let* ((lib-src-file (expand-file-name - (coq-library-src-of-obj-file lib-obj-file))) + (coq-library-src-of-vo-file lib-obj-file))) dependencies deps-mod-time) (if (file-exists-p lib-src-file) ;; recurse into dependencies now @@ -260,7 +260,7 @@ therefore the customizations for `compile' do not apply." (let* ((local-compile-command coq-compile-command) (physical-dir (file-name-directory absolute-module-obj-file)) (module-object (file-name-nondirectory absolute-module-obj-file)) - (module-source (coq-library-src-of-obj-file module-object)) + (module-source (coq-library-src-of-vo-file module-object)) (requiring-file buffer-file-name)) (mapc (lambda (substitution) @@ -282,9 +282,9 @@ therefore the customizations for `compile' do not apply." (compilation-start local-compile-command) (coq-seq-lock-ancestor span - (coq-library-src-of-obj-file absolute-module-obj-file))))) + (coq-library-src-of-vo-file absolute-module-obj-file))))) -(defun coq-seq-map-module-id-to-obj-file (module-id span) +(defun coq-seq-map-module-id-to-obj-file (module-id span &optional from) "Map MODULE-ID to the appropriate coq object file. The mapping depends of course on `coq-load-path'. The current implementation invokes coqdep with a one-line require command. @@ -301,7 +301,7 @@ function returns () if MODULE-ID comes from the standard library." coq-load-path)) (coq-load-path-include-current nil) (temp-require-file (make-temp-file "ProofGeneral-coq" nil ".v")) - (coq-string (concat "Require " module-id ".")) + (coq-string (concat (if from (concat "From " from " ") "") "Require " module-id ".")) result) (unwind-protect (progn @@ -315,16 +315,16 @@ function returns () if MODULE-ID comes from the standard library." (if (stringp result) ;; Error handling: coq-seq-get-library-dependencies was not able to ;; translate module-id into a file name. We insert now a faked error - ;; message into coq-compile-response-buffer to make next-error happy. + ;; message into coq--compile-response-buffer to make next-error happy. (let ((error-message (format "Cannot find library %s in loadpath" module-id)) (inhibit-read-only t)) - ;; Writing a message into coq-compile-response-buffer for next-error + ;; Writing a message into coq--compile-response-buffer for next-error ;; does currently not work. We do have exact position information ;; about the span, but we don't know how much white space there is ;; between the start of the span and the start of the command string. - ;; Check that coq-compile-response-buffer is a valid buffer! - ;; (with-current-buffer coq-compile-response-buffer + ;; Check that coq--compile-response-buffer is a valid buffer! + ;; (with-current-buffer coq--compile-response-buffer ;; (insert ;; (format "File \"%s\", line %d\n%s.\n" ;; (buffer-file-name (span-buffer span)) @@ -337,7 +337,7 @@ function returns () if MODULE-ID comes from the standard library." "Internal error in coq-seq-map-module-id-to-obj-file") (car-safe result))) -(defun coq-seq-check-module (coq-object-local-hash-symbol span module-id) +(defun coq-seq-check-module (coq-object-local-hash-symbol span module-id &optional from) "Locate MODULE-ID and compile if necessary. If `coq-compile-command' is not nil the whole task of checking which modules need compilation and the compilation itself is done by an external @@ -354,7 +354,7 @@ the coq-obj-hash, which is used during internal compilation (see `coq-seq-make-lib-up-to-date'). This way one hash will be used for all \"Require\" commands added at once to the queue." - (let ((module-obj-file (coq-seq-map-module-id-to-obj-file module-id span))) + (let ((module-obj-file (coq-seq-map-module-id-to-obj-file module-id span from))) ;; coq-seq-map-module-id-to-obj-file currently returns () for ;; standard library modules! (when module-obj-file @@ -382,7 +382,8 @@ compilation (if necessary) of the dependencies." (when (and string (string-match coq-require-command-regexp string)) (let ((span (car item)) - (start (match-end 0))) + (start (match-end 0)) + (prefix (match-string 1 string))) (span-add-delete-action span `(lambda () @@ -392,7 +393,7 @@ compilation (if necessary) of the dependencies." (while (string-match coq-require-id-regexp string start) (setq start (match-end 0)) (coq-seq-check-module 'coq-object-hash-symbol span - (match-string 1 string)))))))))) + (match-string 1 string) prefix))))))))) (provide 'coq-seq-compile) diff --git a/coq/coq-smie.el b/coq/coq-smie.el index a609727a..1c0b9c67 100644 --- a/coq/coq-smie.el +++ b/coq/coq-smie.el @@ -107,7 +107,7 @@ attention to case differences." (goto-char pt) ;; looking for a dummy token to see if we fail before reaching ;; strt, which means that we were in a prenthesized expression. - (coq-smie-search-token-backward "#dummy#" strt) + (coq-smie-search-token-backward '("#dummy#") strt) (> (point) strt))))) (defun coq-smie-.-deambiguate () @@ -318,7 +318,7 @@ force indentation." The point should be at the beginning of the command name." (save-excursion ; FIXME Is there other module starting commands? (cond - ((looking-back "with\\s-+") "module") ; lowecase means Module that is not a declaration keyword (like in with Module) + ((looking-back "with\\s-+" nil) "module") ; lowecase means Module that is not a declaration keyword (like in with Module) ((proof-looking-at "\\(Module\\|Section\\)\\>") (if (coq-lonely-:=-in-this-command) "Module start" "Module def"))))) @@ -379,6 +379,9 @@ The point should be at the beginning of the command name." ;; we can. (save-excursion (coq-smie-backward-token))) + ;; easier to return directly than calling coq-smie-backward-token + ((member tok '("lazymatch" "multimatch")) "match") + ;; detect "with signature", otherwies use coq-smie-backward-token ((equal tok "with") (let ((p (point))) @@ -456,15 +459,13 @@ The point should be at the beginning of the command name." ((member corresp '("Inductive" "CoInductive")) ":= inductive") ((equal corresp "let") ":= let") ((equal corresp "where") ":= inductive") ;; inductive or fixpoint, nevermind - ((or (looking-back "{")) ":= record") + ((or (looking-back "{" nil)) ":= record") (t ":=")))) ; a parenthesis stopped the search (defun coq-smie-backward-token () - (let* ((tok (smie-default-backward-token)) - (start (save-excursion (coq-find-real-start) (point))) - (is-tactic (coq-smie-is-tactic))) + (let* ((tok (smie-default-backward-token))) (cond ;; Distinguish between "," from quantification and other uses of ;; "," (tuples, tactic arguments) @@ -487,8 +488,8 @@ The point should be at the beginning of the command name." (cond ((member backtok '("." "Ltac")) "; tactic") ((equal backtok nil) - (if (or (looking-back "(") (looking-back "\\[") - (and (looking-back "{") + (if (or (looking-back "(" nil) (looking-back "\\[") + (and (looking-back "{" nil) (equal (coq-smie-backward-token) "{ subproof"))) ;; recursive call "; tactic" "; record")))))) @@ -504,10 +505,10 @@ The point should be at the beginning of the command name." (equal (coq-smie-backward-token) "; tactic")) ;; recursive "|| tactic") ;; this is wrong half of the time but should not harm indentation - ((and (equal backtok nil) (looking-back "(")) "||") + ((and (equal backtok nil) (looking-back "(" nil)) "||") ((equal backtok nil) - (if (or (looking-back "\\[") - (and (looking-back "{") + (if (or (looking-back "\\[" nil) + (and (looking-back "{" nil) (equal (coq-smie-backward-token) "{ subproof"))) ;; recursive call "|| tactic" "||")))))) @@ -548,7 +549,7 @@ The point should be at the beginning of the command name." (forward-char -1) (if (looking-at "{") "{ subproof" "} subproof")) - ((and (equal tok ":") (looking-back "\\<\\(constr\\|ltac\\)")) + ((and (equal tok ":") (looking-back "\\<\\(constr\\|ltac\\|uconstr\\)" nil)) ": ltacconstr") ((equal tok ":=") @@ -698,10 +699,14 @@ Lemma foo: forall n, :type 'boolean :group 'coq) +(defun coq-indent-safep (indent) + (>= indent 0)) + (defcustom coq-indent-proofstart 2 "Number of spaces used to indent after a proof start." :type 'integer - :group 'coq) + :group 'coq + :safe #'coq-indent-safep) (defcustom coq-indent-semicolon-tactical 2 "Number of spaces used to indent after the first tactical semi colon of a serie. @@ -718,12 +723,14 @@ Lemma foo: forall n, tac3; tac4." :type 'integer - :group 'coq) + :group 'coq + :safe #'coq-indent-safep) (defcustom coq-indent-modulestart 2 "Number of spaces used to indent after a module or section start." :type 'integer - :group 'coq) + :group 'coq + :safe #'coq-indent-safep) (defcustom coq-smie-after-bolp-indentation 2 "Number of spaces used to indent after a quantifier *not* on its own line. @@ -741,7 +748,8 @@ If it is set to 2 (default) it is as follows: x <= 0 -> x = 0. " :type 'integer - :group 'coq) + :group 'coq + :safe #'coq-indent-safep) (defcustom coq-match-indent 2 "Number of space used to indent cases of a match expression. @@ -754,7 +762,9 @@ match n with end Typical values are 2 or 4." - :type 'integer :group 'coq) + :type 'integer + :group 'coq + :safe #'coq-indent-safep) ;; - TODO: remove tokens "{ subproof" and "} subproof" but they are ;; needed by the lexers at a lot of places. @@ -959,14 +969,15 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies." ;; now ( tac3 ; <- neither here ;; tac5) ; ;; ] - ((and (equal token "; tactic") - coq-indent-semicolon-tactical - (not (coq-smie-is-ltacdef)) - (not (coq-smie-is-inside-parenthesized-tactic))) - (if (or (not (smie-rule-parent-p "; tactic")) - (and smie--parent - (coq-smie--same-line-as-parent - (nth 1 smie--parent) (point)))) + ((equal token "; tactic") + (if (and (smie-rule-hanging-p) + coq-indent-semicolon-tactical + (not (coq-smie-is-ltacdef)) + (not (coq-smie-is-inside-parenthesized-tactic)) + (or (not (smie-rule-parent-p "; tactic")) + (and smie--parent + (coq-smie--same-line-as-parent + (nth 1 smie--parent) (point))))) coq-indent-semicolon-tactical nil)) @@ -984,7 +995,7 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies." ;; the command terminated by ". proofstart". ((equal token ". proofstart") (save-excursion (forward-char -1) (coq-find-real-start) - `(column . ,(+ coq-indent-modulestart (current-column))))) + `(column . ,(+ coq-indent-proofstart (current-column))))) ((equal token ". modulestart") (save-excursion (forward-char -1) (coq-find-real-start) `(column . ,(+ coq-indent-modulestart (current-column))))))) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 37867dca..2f6104fe 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -119,10 +119,9 @@ so for the following reasons: :group 'coq) - +;; user shortcuts are prioritized by being put at the end (defvar coq-tactics-db (append - coq-user-tactics-db '( ("absurd " "abs" "absurd " t "absurd") ("apply" "ap" "apply " t "apply") @@ -136,10 +135,12 @@ so for the following reasons: ("autorewrite with in" "arwi" "autorewrite with @{db,db...} in @{hyp}" t) ("autorewrite with using" "arwu" "autorewrite with @{db,db...} using @{tac}" t) ("autorewrite with" "ar" "autorewrite with @{db,db...}" t "autorewrite") - ("case" "c" "case " t "case") + ("case" nil "case " t "case") ("case_eq" "ceq" "case_eq " t "case_eq") ("case_type" "cty" "case_type " t "case_type") - ("cbv" "cbv" "cbv beta [#] delta iota zeta" t "cbv") + ("cbn" "c" "cbn" t "cbn") + ("cbn (with flags)" "cbn" "cbn beta delta [#] iota zeta" t "cbn") + ("cbv" "cbv" "cbv beta delta [#] iota zeta" t "cbv") ("change in" "chi" "change # in #" t) ("change with in" "chwi" "change # with # in #" t) ("change with" "chw" "change # with" t) @@ -188,7 +189,8 @@ so for the following reasons: ("eleft" "eleft" "eleft" t "eleft") ("elim using" "elu" "elim # using #" t) ("elim" "e" "elim #" t "elim") - ("elimtype" "elt" "elimtype" "elimtype") + ("elimtype" "elt" "elimtype" t "elimtype") + ("enough" "eng" "enough (#: #).\n{ #\n}" t "enough") ("erewrite" "er" "erewrite #" t "erewrite") ("eright" "erig" "eright" "eright") ("esplit" "esp" "esplit" t "esplit") @@ -226,20 +228,26 @@ so for the following reasons: ("inversion using in" "invui" "inversion # using # in #" t) ("inversion_clear" "invcl" "inversion_clear" t "inversion_clear") ("lapply" "lap" "lapply" t "lapply") - ("lazy" "lazy" "lazy beta [#] delta iota zeta" t "lazy") + ("lazy" "lazy" "lazy beta delta [#] iota zeta" t "lazy") ("lazymatch with" "m" "lazymatch # with\n| # => #\nend") ("left" "left" "left" t "left") + ("lia" nil "lia" t "lia") ("linear" "lin" "linear" t "linear") ("load" "load" "load" t "load") + ("lra" nil "lra" t "lra") ("move after" "mov" "move # after #" t "move") ("multimatch with" "m" "multimatch # with\n| # => #\nend") - ("now_show" nil "now_show" t "now_show") + ("nia" nil "nia" t "nia") + ("now_show" nil "now_show" t "now_show") + ("nra" nil "nra" t "nra") + ("nsatz" nil "nsatz" t "nsatz") ("omega" "o" "omega" t "omega") ("pattern" "pat" "pattern" t "pattern") ("pattern(s)" "pats" "pattern # , #" t) ("pattern at" "pata" "pattern # at #" t) ("pose" "po" "pose ( # := # )" t "pose") ("prolog" "prol" "prolog" t "prolog") + ("psatz" nil "psatz" t "psatz") ("quote" "quote" "quote" t "quote") ("quote []" "quote2" "quote # [#]" t) ("red" "red" "red" t "red") @@ -258,6 +266,7 @@ so for the following reasons: ("rewrite" "r" "rewrite #" t "rewrite") ("right" "rig" "right" t "right") ;; ("ring" "ring" "ring #" t "ring") + ("romega" nil "romega" t "romega") ("set in * |-" "seth" "set ( # := #) in * |-" t) ("set in *" "set*" "set ( # := #) in *" t) ("set in |- *" "setg" "set ( # := #) in |- *" t) @@ -268,7 +277,8 @@ so for the following reasons: ("setoid_rewrite" "strew" "setoid_rewrite #" t "setoid_rewrite") ("setoid rewrite" "strew" "setoid rewrite #" t "setoid\\s-+rewrite") ("simpl" "s" "simpl" t "simpl") - ("simpl" "sa" "simpl # at #" t) + ("simpl at" "sa" "simpl # at #" t) + ("simpl (all flags)" "simpl" "simpl beta delta [#] iota zeta" t) ("simple destruct" "sdes" "simple destruct" t "simple\\s-+destruct") ("simple inversion" "sinv" "simple inversion" t "simple\\s-+inversion") ("simple induction" "sind" "simple induction" t "simple\\s-+induction") @@ -308,13 +318,14 @@ so for the following reasons: ("unlock" "unlock" "unlock #" t "unlock") ("suffices" "suffices" "suffices # : #" t "suffices") ("suff" "suff" "suff # : #" t "suff") - )) + ) + coq-user-tactics-db) "Coq tactics information list. See `coq-syntax-db' for syntax. " ) +;; user shortcuts are prioritized by being put at the end (defvar coq-solve-tactics-db (append - coq-user-solve-tactics-db '( ("assumption" "as" "assumption" t "assumption") ("eassumption" "eas" "eassumption" t "eassumption") @@ -331,25 +342,34 @@ so for the following reasons: ("fail" "fa" "fail" nil) ("field" "field" "field" t "field") ("gfail" "gfa" "gfail" nil "gfail") + ("lia" nil "lia" t "lia") + ("lra" nil "lra" t "lra") + ("nia" nil "nia" t "nia") + ("nra" nil "nra" t "nra") + ("nsatz" nil "nsatz" t "nsatz") ("omega" "o" "omega" t "omega") + ("romega" nil "romega" t "romega") + ("psatz" nil "psatz" t "psatz") ("reflexivity" "refl" "reflexivity #" t "reflexivity") ("ring" "ring" "ring #" t "ring") ("solve" nil "solve [ # | # ]" nil "solve") ("tauto" "ta" "tauto" t "tauto") ;; SSReflect solving tactics. ("done" nil "done" nil "done") - )) + ) + coq-user-solve-tactics-db) "Coq tactic(al)s that solve a subgoal." ) (defvar coq-solve-cheat-tactics-db (append - coq-user-cheat-tactics-db '(("admit" nil "admit" t "admit") - ("Admitted" nil "Admitted" t "Admitted"))) + ("Admitted" nil "Admitted" t "Admitted")) + coq-user-cheat-tactics-db) "Coq tactic(al)s that solve a subgoal." ) +;; FIXME is this needed? (defvar develock-coq-font-lock-keywords '((develock-find-long-lines (1 'develock-long-line-1 t) @@ -363,7 +383,6 @@ so for the following reasons: (defvar coq-tacticals-db (append - coq-user-tacticals-db '( ("info" nil "info #" nil "info") ("first" nil "first [ # | # ]" nil "first") @@ -382,7 +401,8 @@ so for the following reasons: ("||" nil "# || #" nil) ;; SSReflect tacticals. ("last" "lst" nil t "last") - )) + ) + coq-user-tacticals-db) "Coq tacticals information list. See `coq-syntax-db' for syntax.") @@ -390,6 +410,7 @@ so for the following reasons: (defvar coq-decl-db '( + ("Local Axiom" nil "Local Axiom # : #" t "Local\\s-+Axiom") ("Axiom" "ax" "Axiom # : #" t "Axiom") ("Global Variable" "gv" "Global Variable #: #." t "Global\\s-+Variable") ("Global Variables" "gvs" "Global Variables # , #: #." t "Global\\s-+Variables") @@ -400,6 +421,7 @@ so for the following reasons: ("Hint Rewrite ->" "hrw" "Hint Rewrite -> @{t1,t2...} using @{tac} : @{db}." t "Hint\\s-+Rewrite") ("Hint Rewrite <-" "hrw" "Hint Rewrite <- @{t1,t2...} using @{tac} : @{db}." t ) ("Hint Unfold" "hu" "Hint Unfold # : #." t "Hint\\s-+Unfold") + ("Existing Class" nil "Existing Class " t "Existing\\s-+Class") ("Existing Instance" nil "Existing Instance " t "Existing\\s-+Instance") ("Existing Instances" nil "Existing Instances " t "Existing\\s-+Instances") ("Hypothesis" "hyp" "Hypothesis #: #" t "Hypothesis") @@ -409,6 +431,8 @@ so for the following reasons: ("Conjecture" "conj" "Conjecture #: #." t "Conjecture") ("Variable" "v" "Variable #: #." t "Variable") ("Variables" "vs" "Variables # , #: #." t "Variables") + ("Context" nil "Context #, (# : #)." t "Context") + ("Local Coercion" nil "Local Coercion @{id} : @{typ1} >-> @{typ2}." t "Local\\s-+Coercion") ("Coercion" "coerc" "Coercion @{id} : @{typ1} >-> @{typ2}." t "Coercion") ) "Coq declaration keywords information list. See `coq-syntax-db' for syntax." @@ -425,6 +449,7 @@ so for the following reasons: ("Declare Module Import <: :=" "dmi2" "Declare Module # <: # := #." t);; careful ("Declare Module Export : :=" "dme" "Declare Module # : # := #." t) ("Declare Module Export <: :=" "dme2" "Declare Module # <: # := #." t);; careful + ("Local Definition" nil "Local Definition #:# := #." t "Local\\s-+Definition");; careful ("Definition" "def" "Definition #:# := #." t "Definition");; careful ("Definition (2 args)" "def2" "Definition # (# : #) (# : #):# := #." t) ("Definition (3 args)" "def3" "Definition # (# : #) (# : #) (# : #):# := #." t) @@ -455,6 +480,7 @@ so for the following reasons: ("Instance" nil "Instance #:#.\nProof.\n#Defined." t "Instance") ("Program Instance" "pinstance" "Program Instance [ # ] => # where \n# := #;\n# := #." t "Program\\s-+Instance") ("Let" "Let" "Let # : # := #." t "Let") + ("Local Ltac" nil "Local Ltac # := #" t "Local\\s-+Ltac") ("Ltac" "ltac" "Ltac # := #" t "Ltac") ("Module :=" "mo" "Module # : # := #." t ) ; careful ("Module <: :=" "mo2" "Module # <: # := #." t ) ; careful @@ -517,6 +543,7 @@ so for the following reasons: '( ("About" nil "About #." nil "About") ("Check" nil "Check" nil "Check") + ("Fail" nil "Fail" nil "fail") ("Inspect" nil "Inspect #." nil "Inspect") ("Locate File" nil "Locate File \"#\"." nil "Locate\\s-+File") ("Locate Library" nil "Locate Library #." nil "Locate\\s-+Library") @@ -531,133 +558,344 @@ so for the following reasons: ("SearchPattern" nil "SearchPattern (#)" nil "SearchPattern") ("SearchRewrite" nil "SearchRewrite #" nil "SearchRewrite") ("Show" nil "Show #." nil "Show") - ("Test" nil "Test" nil "Test" nil t) - ("Test Printing Depth" nil "Test Printing Depth." nil "Test\\s-+Printing\\s-+Depth") - ("Test Printing If" nil "Test Printing If #." nil "Test\\s-+Printing\\s-+If") - ("Test Printing Let" nil "Test Printing Let #." nil "Test\\s-+Printing\\s-+Let") - ("Test Printing Synth" nil "Test Printing Synth." nil "Test\\s-+Printing\\s-+Synth") - ("Test Printing Width" nil "Test Printing Width." nil "Test\\s-+Printing\\s-+Width") - ("Test Printing Wildcard" nil "Test Printing Wildcard." nil "Test\\s-+Printing\\s-+Wildcard") + ("Test" nil "Test" nil "Test" nil t) ; let us not highlight all possible options for Test + ("Timeout" nil "Timeout" nil "Timeout") ) "Coq queries command, that deserve a separate menu for sending them to coq without insertion. " ) - ;; command that are not declarations, definition or goal starters (defvar coq-other-commands-db - '( - ("Add Parametric Relation" nil "Add Parametric Relation : " t "Add\\s-+Parametric\\s-+Relation") - ("BeginSubproof" "bs" "BeginSubproof.\n#\nEndSubproof." t "BeginSubproof") - ("EndSubproof" "es" "EndSubproof.#" t "EndSubproof") - ;; ("Abort" nil "Abort." t "Abort" nil nil);don't appear in menu -; ("Add" nil "Add #." nil "Add" nil t) - ("Add Abstract Ring" nil "Add Abstract Ring #." t "Add\\s-+Abstract\\s-+Ring") - ("Add Abstract Semi Ring" nil "Add Abstract Semi Ring #." t "Add\\s-+Abstract\\s-+Semi\\s-+Ring") - ("Add Field" nil "Add Field #." t "Add\\s-+Field") - ("Add LoadPath" nil "Add LoadPath #." nil "Add\\s-+LoadPath") - ("Add ML Path" nil "Add ML Path #." nil "Add\\s-+ML\\s-+Path") - ("Add Printing" nil "Add Printing #." t "Add\\s-+Printing") - ("Add Printing If" nil "Add Printing If #." t "Add\\s-+Printing\\s-+If") - ("Add Printing Let" nil "Add Printing Let #." t "Add\\s-+Printing\\s-+Let") - ("Add Rec LoadPath" nil "Add Rec LoadPath #." nil "Add\\s-+Rec\\s-+LoadPath") - ("Add Rec ML Path" nil "Add Rec ML Path #." nil "Add\\s-+Rec\\s-+ML\\s-+Path") - ("Add Ring" nil "Add Ring #." t "Add\\s-+Ring") - ("Add Semi Ring" nil "Add Semi Ring #." t "Add\\s-+Semi\\s-+Ring") - ("Add Setoid" nil "Add Setoid #." t "Add\\s-+Setoid") - ("Admit Obligations" "oblsadmit" "Admit Obligations." nil "Admit\\s-+Obligations") - ("Arguments Scope" "argsc" "Arguments Scope @{id} [ @{_} ]" t "Arguments\\s-+Scope") - ("Arguments" "args" "Arguments @{id} : @{rule}" t "Arguments") - ("Bind Scope" "bndsc" "Bind Scope @{scope} with @{type}" t "Bind\\s-+Scope") - ("Canonical Structure" nil "Canonical Structure #." t "Canonical\\s-+Structure") - ("Cd" nil "Cd #." nil "Cd") - ("Local Close Scope" "lclsc" "Local Close Scope #" t "Local\\s-+Close\\s-+Scope") - ("Close Scope" "clsc" "Close Scope #" t "Close\\s-+Scope") - ("Comments" nil "Comments #." nil "Comments") - ("Declare" nil "Declare #." nil "Declare") - ("Delimit Scope" "delsc" "Delimit Scope @{scope} with @{id}." t "Delimit\\s-+Scope" ) - ("Eval" nil "Eval #." nil "Eval") - ("Export" nil "Export #." t "Export") - ("Extract Constant" "extrc" "Extract Constant @{id} => \"@{id}\"." nil "Extract\\s-+Constant") - ("Extract Inlined Constant" "extric" "Extract Inlined Constant @{id} => \"@{id}\"." nil "Extract\\s-+Inlined\\s-+Constant") - ("Extract Inductive" "extri" "Extract Inductive @{id} => \"@{id}\" [\"@{id}\" \"@{id...}\"]." nil "Extract") - ("Extraction (in a file)" "extrf" "Extraction \"@{file}\" @{id}." nil) - ("Extraction Inline" nil "Extraction Inline #." t "Extraction\\s-+Inline") - ("Extraction NoInline" nil "Extraction NoInline #." t "Extraction\\s-+NoInline") - ("Extraction Language" "extrlang" "Extraction Language #." t "Extraction\\s-+Language") - ("Extraction Library" "extrl" "Extraction Library @{id}." nil "Extraction\\s-+Library") - ("Extraction" "extr" "Extraction @{id}." nil "Extraction") - ("Focus" nil "Focus #." nil "Focus") - ("Generalizable Variables" nil "Generalizable Variables #." t "Generalizable\\s-+Variables") - ("Generalizable All Variables" nil "Generalizable All Variables." t "Generalizable\\s-+All\\s-+Variables") - ("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") - ("Implicit Arguments" nil "Implicit Arguments # [#]." t "Implicit\\s-+Arguments") - ("Implicit Types" nil "Implicit Types # : #." t "Implicit\\s-+Types") - ("Import" nil "Import #." t "Import") - ("Infix" "inf" "Infix \"#\" := # (at level #) : @{scope}." t "Infix") - ("Notation (assoc)" "notas" "Notation \"#\" := # (at level #, # associativity)." t) - ("Notation (at assoc)" "notassc" "Notation \"#\" := # (at level #, # associativity) : @{scope}." t) - ("Notation (at at scope)" "notasc" "Notation \"#\" := # (at level #, # at level #) : @{scope}." t) - ("Notation (at at)" "nota" "Notation \"#\" := # (at level #, # at level #)." t) - ("Notation (only parsing)" "notsp" "Notation # := # (only parsing)." t) - ("Local Notation" "lnots" "Local Notation # := #." t "Local\\s-+Notation") - ("Local Notation (only parsing)" "lnotsp" "Local Notation # := # (only parsing)." t) - ("Notation (simple)" "nots" "Notation # := #." t "Notation") - ("Typeclasses Opaque" nil "Typeclasses Opaque #." nil "Typeclasses\\s-+Opaque") - ("Opaque" nil "Opaque #." nil "Opaque") - ("Obligation Tactic" nil "Obligation Tactic := #." t "Obligation\\s-+Tactic") - ("Local Open Scope" nil "Local Open Scope #" t "Local\\s-+Open\\s-+Scope") - ("Open Local Scope" nil "Open Local Scope #" t "Open\\s-+Local\\s-+Scope") - ("Open Scope" "opsc" "Open Scope #" t "Open\\s-+Scope") - ("Preterm" nil "Preterm." nil "Preterm") - ("Qed" nil "Qed." nil "Qed") - ("Recursive Extraction" "recextr" "Recursive Extraction @{id}." nil "Recursive\\s-+Extraction") - ("Recursive Extraction Library" "recextrl" "Recursive Extraction Library @{id}." nil "Recursive\\s-+Extraction\\s-+Library") - ("Recursive Extraction Module" "recextrm" "Recursive Extraction Module @{id}." nil "Recursive\\s-+Extraction\\s-+Module") - ("Remove LoadPath" nil "Remove LoadPath" nil "Remove\\s-+LoadPath") - ("Remove LoadPath" nil "Remove LoadPath" nil "Remove\\s-+LoadPath") - ("Remove Printing If" nil "Remove Printing If #." t "Remove\\s-+Printing\\s-+If") - ("Remove Printing Let" nil "Remove Printing Let #." t "Remove\\s-+Printing\\s-+Let") - ("Require Export" nil "Require Export #." t "Require\\s-+Export") - ("Require Import" nil "Require Import #." t "Require\\s-+Import") - ("Require" nil "Require #." t "Require") - ("Reserved Notation" nil "Reserved Notation" nil "Reserved\\s-+Notation") - ("Reset Extraction Inline" nil "Reset Extraction Inline." t "Reset\\s-+Extraction\\s-+Inline") - ("Save" nil "Save." t "Save") - ("Set Extraction AutoInline" nil "Set Extraction AutoInline" t "Set\\s-+Extraction\\s-+AutoInline") - ("Set Extraction Optimize" nil "Set Extraction Optimize" t "Set\\s-+Extraction\\s-+Optimize") - ("Set Implicit Arguments" nil "Set Implicit Arguments" t "Set\\s-+Implicit\\s-+Arguments") - ("Set Strict Implicit" nil "Set Strict Implicit" t "Set\\s-+Strict\\s-+Implicit") - ("Set Printing Synth" nil "Set Printing Synth" t "Set\\s-+Printing\\s-+Synth") - ("Set Printing Wildcard" nil "Set Printing Wildcard" t "Set\\s-+Printing\\s-+Wildcard") - ("Set Printing All" "sprall" "Set Printing All" t "Set\\s-+Printing\\s-+All") - ("Set Hyps Limit" nil "Set Hyps Limit #." nil "Set\\s-+Hyps\\s-+Limit") - ("Set Printing Coercions" nil "Set Printing Coercions." t "Set\\s-+Printing\\s-+Coercions") - ("Set Printing Notations" "sprn" "Set Printing Notations" t "Set\\s-+Printing\\s-+Notations") - ("Set Undo" nil "Set Undo #." nil "Set\\s-+Undo") - ("Solve Obligations" "oblssolve" "Solve Obligations using #." t "Solve\\s-+Obligations") - ("Tactic Notation" nil "Tactic Notation # := #." t "Tactic\\s-+Notation") - ("Transparent" nil "Transparent #." nil "Transparent") - - ("Unfocus" nil "Unfocus." nil "Unfocus") - ("Unset Extraction AutoInline" nil "Unset Extraction AutoInline" t "Unset\\s-+Extraction\\s-+AutoInline") - ("Unset Extraction Optimize" nil "Unset Extraction Optimize" t "Unset\\s-+Extraction\\s-+Optimize") - ("Unset Implicit Arguments" nil "Unset Implicit Arguments" t "Unset\\s-+Implicit\\s-+Arguments") - ("Unset Strict Implicit" nil "Unset Strict Implicit" t "Unset\\s-+Strict\\s-+Implicit") - ("Unset Printing Synth" nil "Unset Printing Synth" t "Unset\\s-+Printing\\s-+Synth") - ("Unset Printing Wildcard" nil "Unset Printing Wildcard" t "Unset\\s-+Printing\\s-+Wildcard") - ("Unset Hyps Limit" nil "Unset Hyps Limit" nil "Unset\\s-+Hyps\\s-+Limit") - ("Unset Printing All" "unsprall" "Unset Printing All" nil "Unset\\s-+Printing\\s-+All") - ("Unset Printing Coercion" nil "Unset Printing Coercion #." t "Unset\\s-+Printing\\s-+Coercion") - ("Unset Printing Coercions" nil "Unset Printing Coercions." nil "Unset\\s-+Printing\\s-+Coercions") - ("Unset Printing Notations" "unsprn" "Unset Printing Notations" nil "Unset\\s-+Printing\\s-+Notations") - ("Unset Undo" nil "Unset Undo." nil "Unset\\s-+Undo") - ; ("print" "pr" "print #" "print") - ) + '( + ("Add Parametric Relation" nil "Add Parametric Relation : " t "Add\\s-+Parametric\\s-+Relation") + ;; ("Abort" nil "Abort." t "Abort" nil nil);don't appear in menu + ;; ("Add" nil "Add #." nil "Add" nil t) + ("Add Abstract Ring" nil "Add Abstract Ring #." t "Add\\s-+Abstract\\s-+Ring") + ("Add Abstract Semi Ring" nil "Add Abstract Semi Ring #." t "Add\\s-+Abstract\\s-+Semi\\s-+Ring") + ("Add Field" nil "Add Field #." t "Add\\s-+Field") + ("Add LoadPath" nil "Add LoadPath #." nil "Add\\s-+LoadPath") + ("Add ML Path" nil "Add ML Path #." nil "Add\\s-+ML\\s-+Path") + ("Add Printing" nil "Add Printing #." t "Add\\s-+Printing") + ("Add Printing If" nil "Add Printing If #." t "Add\\s-+Printing\\s-+If") + ("Add Printing Let" nil "Add Printing Let #." t "Add\\s-+Printing\\s-+Let") + ("Add Rec LoadPath" nil "Add Rec LoadPath #." nil "Add\\s-+Rec\\s-+LoadPath") + ("Add Rec ML Path" nil "Add Rec ML Path #." nil "Add\\s-+Rec\\s-+ML\\s-+Path") + ("Add Ring" nil "Add Ring #." t "Add\\s-+Ring") + ("Add Semi Ring" nil "Add Semi Ring #." t "Add\\s-+Semi\\s-+Ring") + ("Add Setoid" nil "Add Setoid #." t "Add\\s-+Setoid") + ("Admit Obligations" "oblsadmit" "Admit Obligations." nil "Admit\\s-+Obligations") + ("Arguments Scope" "argsc" "Arguments Scope @{id} [ @{_} ]" t "Arguments\\s-+Scope") + ("Local Arguments" nil "Local Arguments @{id} : @{rule}" t "Local\\s-+Arguments") + ("Arguments" "args" "Arguments @{id} : @{rule}" t "Arguments") + ("Bind Scope" "bndsc" "Bind Scope @{scope} with @{type}" t "Bind\\s-+Scope") + ("Canonical Structure" nil "Canonical Structure #." t "Canonical\\s-+Structure") + ("Cd" nil "Cd #." nil "Cd") + ("Local Close Scope" "lclsc" "Local Close Scope #" t "Local\\s-+Close\\s-+Scope") + ("Close Scope" "clsc" "Close Scope #" t "Close\\s-+Scope") + ("Comments" nil "Comments #." nil "Comments") + ("Declare" nil "Declare #." nil "Declare") + ("Delimit Scope" "delsc" "Delimit Scope @{scope} with @{id}." t "Delimit\\s-+Scope" ) + ("Eval" nil "Eval #." nil "Eval") + ("Export" nil "Export #." t "Export") + ("Extract Constant" "extrc" "Extract Constant @{id} => \"@{id}\"." nil "Extract\\s-+Constant") + ("Extract Inlined Constant" "extric" "Extract Inlined Constant @{id} => \"@{id}\"." nil "Extract\\s-+Inlined\\s-+Constant") + ("Extract Inductive" "extri" "Extract Inductive @{id} => \"@{id}\" [\"@{id}\" \"@{id...}\"]." nil "Extract") + ("Extraction (in a file)" "extrf" "Extraction \"@{file}\" @{id}." nil) + ("Extraction Inline" nil "Extraction Inline #." t "Extraction\\s-+Inline") + ("Extraction NoInline" nil "Extraction NoInline #." t "Extraction\\s-+NoInline") + ("Extraction Language" "extrlang" "Extraction Language #." t "Extraction\\s-+Language") + ("Extraction Library" "extrl" "Extraction Library @{id}." nil "Extraction\\s-+Library") + ("Extraction" "extr" "Extraction @{id}." nil "Extraction") + ("Focus" nil "Focus #." nil "Focus") + ("Generalizable Variables" nil "Generalizable Variables #." t "Generalizable\\s-+Variables") + ("Generalizable All Variables" nil "Generalizable All Variables." t "Generalizable\\s-+All\\s-+Variables") + ("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") + ("Implicit Arguments" nil "Implicit Arguments # [#]." t "Implicit\\s-+Arguments") + ("Implicit Types" nil "Implicit Types # : #." t "Implicit\\s-+Types") + ("Import" nil "Import #." t "Import") + ("Include" nil "Include #." t "Include") + ("Infix" "inf" "Infix \"#\" := # (at level #) : @{scope}." t "Infix") + ("Notation (assoc)" "notas" "Notation \"#\" := # (at level #, # associativity)." t) + ("Notation (at assoc)" "notassc" "Notation \"#\" := # (at level #, # associativity) : @{scope}." t) + ("Notation (at at scope)" "notasc" "Notation \"#\" := # (at level #, # at level #) : @{scope}." t) + ("Notation (at at)" "nota" "Notation \"#\" := # (at level #, # at level #)." t) + ("Notation (only parsing)" "notsp" "Notation # := # (only parsing)." t) + ("Local Notation" "lnots" "Local Notation # := #." t "Local\\s-+Notation") + ("Local Notation (only parsing)" "lnotsp" "Local Notation # := # (only parsing)." t) + ("Notation (simple)" "nots" "Notation # := #." t "Notation") + ("Typeclasses Opaque" nil "Typeclasses Opaque #." nil "Typeclasses\\s-+Opaque") + ("Opaque" nil "Opaque #." nil "Opaque") + ("Obligation Tactic" nil "Obligation Tactic := #." t "Obligation\\s-+Tactic") + ("Local Open Scope" nil "Local Open Scope #" t "Local\\s-+Open\\s-+Scope") + ("Open Local Scope" nil "Open Local Scope #" t "Open\\s-+Local\\s-+Scope") + ("Open Scope" "opsc" "Open Scope #" t "Open\\s-+Scope") + ("Preterm" nil "Preterm." nil "Preterm") + ("Qed" nil "Qed." nil "Qed") + ("Recursive Extraction" "recextr" "Recursive Extraction @{id}." nil "Recursive\\s-+Extraction") + ("Recursive Extraction Library" "recextrl" "Recursive Extraction Library @{id}." nil "Recursive\\s-+Extraction\\s-+Library") + ("Recursive Extraction Module" "recextrm" "Recursive Extraction Module @{id}." nil "Recursive\\s-+Extraction\\s-+Module") + ("Remove LoadPath" nil "Remove LoadPath" nil "Remove\\s-+LoadPath") + ("Remove LoadPath" nil "Remove LoadPath" nil "Remove\\s-+LoadPath") + ("Remove Printing If" nil "Remove Printing If #." t "Remove\\s-+Printing\\s-+If") + ("Remove Printing Let" nil "Remove Printing Let #." t "Remove\\s-+Printing\\s-+Let") + ("Require Export" nil "Require Export #." t "Require\\s-+Export") + ("Require Import" nil "Require Import #." t "Require\\s-+Import") + ("Require" nil "Require #." t "Require") + ("Reserved Infix" nil "Reserved Infix" nil "Reserved\\s-+Infix") + ("Reserved Notation" nil "Reserved Notation" nil "Reserved\\s-+Notation") + ("Reset Extraction Inline" nil "Reset Extraction Inline." t "Reset\\s-+Extraction\\s-+Inline") + ("Save" nil "Save." t "Save") + ("Set Asymmetric Patterns" nil "Set Asymmetric Patterns" t "Set Asymmetric\\s-+Patterns") + ("Set Atomic Load" nil "Set Atomic Load" t "Set Atomic\\s-+Load") + ("Set Automatic Coercions Import" nil "Set Automatic Coercions Import" t "Set Automatic\\s-+Coercions\\s-+Import") + ("Set Automatic Introduction" nil "Set Automatic Introduction" t "Set Automatic\\s-+Introduction") + ("Set Boolean Equality Schemes" nil "Set Boolean Equality Schemes" t "Set Boolean\\s-+Equality\\s-+Schemes") + ("Set Bracketing Last Introduction Pattern" nil "Set Bracketing Last Introduction Pattern" t "Set Bracketing\\s-+Last\\s-+Introduction\\s-+Pattern") + ("Set Bullet Behavior" nil "Set Bullet Behavior" t "Set Bullet\\s-+Behavior") + ("Set Case Analysis Schemes" nil "Set Case Analysis Schemes" t "Set Case\\s-+Analysis\\s-+Schemes") + ("Set Compat Notations" nil "Set Compat Notations" t "Set Compat\\s-+Notations") + ("Set Congruence Depth" nil "Set Congruence Depth" t "Set Congruence\\s-+Depth") + ("Set Congruence Verbose" nil "Set Congruence Verbose" t "Set Congruence\\s-+Verbose") + ("Set Contextual Implicit" nil "Set Contextual Implicit" t "Set Contextual\\s-+Implicit") + ("Set Debug Auto" nil "Set Debug Auto" t "Set Debug\\s-+Auto") + ("Set Debug Eauto" nil "Set Debug Eauto" t "Set Debug\\s-+Eauto") + ("Set Debug RAKAM" nil "Set Debug RAKAM" t "Set Debug\\s-+RAKAM") + ("Set Debug Tactic Unification" nil "Set Debug Tactic Unification" t "Set Debug\\s-+Tactic\\s-+Unification") + ("Set Debug Trivial" nil "Set Debug Trivial" t "Set Debug\\s-+Trivial") + ("Set Debug Unification" nil "Set Debug Unification" t "Set Debug\\s-+Unification") + ("Set Decidable Equality Schemes" nil "Set Decidable Equality Schemes" t "Set Decidable\\s-+Equality\\s-+Schemes") + ("Set Default Clearing Used Hypotheses" nil "Set Default Clearing Used Hypotheses" t "Set Default\\s-+Clearing\\s-+Used\\s-+Hypotheses") + ("Set Default Goal Selector" nil "Set Default Goal Selector" t "Set Default\\s-+Goal\\s-+Selector") + ("Set Default Proof Mode" nil "Set Default Proof Mode" t "Set Default\\s-+Proof\\s-+Mode") + ("Set Default Proof Using" nil "Set Default Proof Using" t "Set Default\\s-+Proof\\s-+Using") + ("Set Default Timeout" nil "Set Default Timeout" t "Set Default\\s-+Timeout") + ("Set Dependent Propositions Elimination" nil "Set Dependent Propositions Elimination" t "Set Dependent\\s-+Propositions\\s-+Elimination") + ("Set Discriminate Introduction" nil "Set Discriminate Introduction" t "Set Discriminate\\s-+Introduction") + ("Set Dump Bytecode" nil "Set Dump Bytecode" t "Set Dump\\s-+Bytecode") + ("Set Elimination Schemes" nil "Set Elimination Schemes" t "Set Elimination\\s-+Schemes") + ("Set Equality Scheme" nil "Set Equality Scheme" t "Set Equality\\s-+Scheme") + ("Set Extraction AccessOpaque" nil "Set Extraction AccessOpaque" t "Set Extraction\\s-+AccessOpaque") + ("Set Extraction AutoInline" nil "Set Extraction AutoInline" t "Set Extraction\\s-+AutoInline") + ("Set Extraction Conservative Types" nil "Set Extraction Conservative Types" t "Set Extraction\\s-+Conservative\\s-+Types") + ("Set Extraction File Comment" nil "Set Extraction File Comment" t "Set Extraction\\s-+File\\s-+Comment") + ("Set Extraction Flag" nil "Set Extraction Flag" t "Set Extraction\\s-+Flag") + ("Set Extraction KeepSingleton" nil "Set Extraction KeepSingleton" t "Set Extraction\\s-+KeepSingleton") + ("Set Extraction Optimize" nil "Set Extraction Optimize" t "Set Extraction\\s-+Optimize") + ("Set Extraction SafeImplicits" nil "Set Extraction SafeImplicits" t "Set Extraction\\s-+SafeImplicits") + ("Set Extraction TypeExpand" nil "Set Extraction TypeExpand" t "Set Extraction\\s-+TypeExpand") + ("Set Firstorder Depth" nil "Set Firstorder Depth" t "Set Firstorder\\s-+Depth") + ("Set Hide Obligations" nil "Set Hide Obligations" t "Set Hide\\s-+Obligations") + ("Set Implicit Arguments" nil "Set Implicit Arguments" t "Set Implicit\\s-+Arguments") + ("Set Info Auto" nil "Set Info Auto" t "Set Info\\s-+Auto") + ("Set Info Eauto" nil "Set Info Eauto" t "Set Info\\s-+Eauto") + ("Set Info Level" nil "Set Info Level" t "Set Info\\s-+Level") + ("Set Info Trivial" nil "Set Info Trivial" t "Set Info\\s-+Trivial") + ("Set Injection L2R Pattern Order" nil "Set Injection L2R Pattern Order" t "Set Injection\\s-+L2R\\s-+Pattern\\s-+Order") + ("Set Injection On Proofs" nil "Set Injection On Proofs" t "Set Injection\\s-+On\\s-+Proofs") + ("Set Inline Level" nil "Set Inline Level" t "Set Inline\\s-+Level") + ("Set Intuition Iff Unfolding" nil "Set Intuition Iff Unfolding" t "Set Intuition\\s-+Iff\\s-+Unfolding") + ("Set Intuition Negation Unfolding" nil "Set Intuition Negation Unfolding" t "Set Intuition\\s-+Negation\\s-+Unfolding") + ("Set Kernel Term Sharing" nil "Set Kernel Term Sharing" t "Set Kernel\\s-+Term\\s-+Sharing") + ("Set Keyed Unification" nil "Set Keyed Unification" t "Set Keyed\\s-+Unification") + ("Set Loose Hint Behavior" nil "Set Loose Hint Behavior" t "Set Loose\\s-+Hint\\s-+Behavior") + ("Set Maximal Implicit Insertion" nil "Set Maximal Implicit Insertion" t "Set Maximal\\s-+Implicit\\s-+Insertion") + ("Set Nonrecursive Elimination Schemes" nil "Set Nonrecursive Elimination Schemes" t "Set Nonrecursive\\s-+Elimination\\s-+Schemes") + ("Set Parsing Explicit" nil "Set Parsing Explicit" t "Set Parsing\\s-+Explicit") + ("Set Primitive Projections" nil "Set Primitive Projections" t "Set Primitive\\s-+Projections") + ("Set Printing All" nil "Set Printing All" t "Set Printing\\s-+All") + ("Set Printing Coercions" nil "Set Printing Coercions" t "Set Printing\\s-+Coercions") + ("Set Printing Depth" nil "Set Printing Depth" t "Set Printing\\s-+Depth") + ("Set Printing Existential Instances" nil "Set Printing Existential Instances" t "Set Printing\\s-+Existential\\s-+Instances") + ("Set Printing Implicit" nil "Set Printing Implicit" t "Set Printing\\s-+Implicit") + ("Set Printing Implicit Defensive" nil "Set Printing Implicit Defensive" t "Set Printing\\s-+Implicit\\s-+Defensive") + ("Set Printing Matching" nil "Set Printing Matching" t "Set Printing\\s-+Matching") + ("Set Printing Notations" nil "Set Printing Notations" t "Set Printing\\s-+Notations") + ("Set Printing Primitive Projection Compatibility" nil "Set Printing Primitive Projection Compatibility" t "Set Printing\\s-+Primitive\\s-+Projection\\s-+Compatibility") + ("Set Printing Primitive Projection Parameters" nil "Set Printing Primitive Projection Parameters" t "Set Printing\\s-+Primitive\\s-+Projection\\s-+Parameters") + ("Set Printing Projections" nil "Set Printing Projections" t "Set Printing\\s-+Projections") + ("Set Printing Records" nil "Set Printing Records" t "Set Printing\\s-+Records") + ("Set Printing Synth" nil "Set Printing Synth" t "Set Printing\\s-+Synth") + ("Set Printing Universes" nil "Set Printing Universes" t "Set Printing\\s-+Universes") + ("Set Printing Width" nil "Set Printing Width" t "Set Printing\\s-+Width") + ("Set Printing Wildcard" nil "Set Printing Wildcard" t "Set Printing\\s-+Wildcard") + ("Set Program Mode" nil "Set Program Mode" t "Set Program\\s-+Mode") + ("Set Proof Using Clear Unused" nil "Set Proof Using Clear Unused" t "Set Proof\\s-+Using\\s-+Clear\\s-+Unused") + ("Set Record Elimination Schemes" nil "Set Record Elimination Schemes" t "Set Record\\s-+Elimination\\s-+Schemes") + ("Set Refine Instance Mode" nil "Set Refine Instance Mode" t "Set Refine\\s-+Instance\\s-+Mode") + ("Set Regular Subst Tactic" nil "Set Regular Subst Tactic" t "Set Regular\\s-+Subst\\s-+Tactic") + ("Set Reversible Pattern Implicit" nil "Set Reversible Pattern Implicit" t "Set Reversible\\s-+Pattern\\s-+Implicit") + ("Set Rewriting Schemes" nil "Set Rewriting Schemes" t "Set Rewriting\\s-+Schemes") + ("Set Short Module Printing" nil "Set Short Module Printing" t "Set Short\\s-+Module\\s-+Printing") + ("Set Shrink Obligations" nil "Set Shrink Obligations" t "Set Shrink\\s-+Obligations") + ("Set SimplIsCbn" nil "Set SimplIsCbn" t "Set SimplIsCbn") + ("Set Standard Proposition Elimination Names" nil "Set Standard Proposition Elimination Names" t "Set Standard\\s-+Proposition\\s-+Elimination\\s-+Names") + ("Set Strict Proofs" nil "Set Strict Proofs" t "Set Strict\\s-+Proofs") + ("Set Strict Universe Declaration" nil "Set Strict Universe Declaration" t "Set Strict\\s-+Universe\\s-+Declaration") + ("Set Strongly Strict Implicit" nil "Set Strongly Strict Implicit" t "Set Strongly\\s-+Strict\\s-+Implicit") + ("Set Suggest Proof Using" nil "Set Suggest Proof Using" t "Set Suggest\\s-+Proof\\s-+Using") + ("Set Tactic Compat Context" nil "Set Tactic Compat Context" t "Set Tactic\\s-+Compat\\s-+Context") + ("Set Tactic Evars Pattern Unification" nil "Set Tactic Evars Pattern Unification" t "Set Tactic\\s-+Evars\\s-+Pattern\\s-+Unification") + ("Set Tactic Pattern Unification" nil "Set Tactic Pattern Unification" t "Set Tactic\\s-+Pattern\\s-+Unification") + ("Set Transparent Obligations" nil "Set Transparent Obligations" t "Set Transparent\\s-+Obligations") + ("Set Typeclass Resolution After Apply" nil "Set Typeclass Resolution After Apply" t "Set Typeclass\\s-+Resolution\\s-+After\\s-+Apply") + ("Set Typeclass Resolution For Conversion" nil "Set Typeclass Resolution For Conversion" t "Set Typeclass\\s-+Resolution\\s-+For\\s-+Conversion") + ("Set Typeclasses Debug" nil "Set Typeclasses Debug" t "Set Typeclasses\\s-+Debug") + ("Set Typeclasses Dependency Order" nil "Set Typeclasses Dependency Order" t "Set Typeclasses\\s-+Dependency\\s-+Order") + ("Set Typeclasses Depth" nil "Set Typeclasses Depth" t "Set Typeclasses\\s-+Depth") + ("Set Typeclasses Modulo Eta" nil "Set Typeclasses Modulo Eta" t "Set Typeclasses\\s-+Modulo\\s-+Eta") + ("Set Typeclasses Strict Resolution" nil "Set Typeclasses Strict Resolution" t "Set Typeclasses\\s-+Strict\\s-+Resolution") + ("Set Typeclasses Unique Instances" nil "Set Typeclasses Unique Instances" t "Set Typeclasses\\s-+Unique\\s-+Instances") + ("Set Typeclasses Unique Solutions" nil "Set Typeclasses Unique Solutions" t "Set Typeclasses\\s-+Unique\\s-+Solutions") + ("Set Universal Lemma Under Conjunction" nil "Set Universal Lemma Under Conjunction" t "Set Universal\\s-+Lemma\\s-+Under\\s-+Conjunction") + ("Set Universe Minimization ToSet" nil "Set Universe Minimization ToSet" t "Set Universe\\s-+Minimization\\s-+ToSet") + ("Set Universe Polymorphism" nil "Set Universe Polymorphism" t "Set Universe\\s-+Polymorphism") + ("Set Verbose Compat Notations" nil "Set Verbose Compat Notations" t "Set Verbose\\s-+Compat\\s-+Notations") + ("Set Function_debug" nil "Set Function_debug" t "Set Function_debug") + ("Set Function_raw_tcc" nil "Set Function_raw_tcc" t "Set Function_raw_tcc") + ("Set Functional Induction Rewrite Dependent" nil "Set Functional Induction Rewrite Dependent" t "Set Functional\\s-+Induction\\s-+Rewrite\\s-+Dependent") + ("Set Hyps Limit" nil "Set Hyps Limit" t "Set Hyps\\s-+Limit") + ("Set Ltac Debug" nil "Set Ltac Debug" t "Set Ltac\\s-+Debug") + ("Set Silent" nil "Set Silent" t "Set Silent") + ("Set Undo" nil "Set Undo" t "Set Undo") + ("Set Search Blacklist" nil "Set Search Blacklist" t "Set Search\\s-+Blacklist") + ("Set Printing Coercion" nil "Set Printing Coercion" t "Set Printing\\s-+Coercion") + ("Set Printing If" nil "Set Printing If" t "Set Printing\\s-+If") + ("Set Printing Let" nil "Set Printing Let" t "Set Printing\\s-+Let") + ("Set Printing Record" nil "Set Printing Record" t "Set Printing\\s-+Record") + ("Set Printing Constructor" nil "Set Printing Constructor" t "Set Printing\\s-+Constructor") + ("Solve Obligations" "oblssolve" "Solve Obligations using #." t "Solve\\s-+Obligations") + ("Local Strategy" nil "Local Strategy # [#]." t "Local\\s-+Strategy") + ("Strategy" nil "Strategy # [#]." t "Strategy") + ("Tactic Notation" nil "Tactic Notation # := #." t "Tactic\\s-+Notation") + ("Transparent" nil "Transparent #." nil "Transparent") + + ("Unfocus" nil "Unfocus." nil "Unfocus") + ("Unset Asymmetric Patterns" nil "Unset Asymmetric Patterns" t "Unset Asymmetric\\s-+Patterns") + ("Unset Atomic Load" nil "Unset Atomic Load" t "Unset Atomic\\s-+Load") + ("Unset Automatic Coercions Import" nil "Unset Automatic Coercions Import" t "Unset Automatic\\s-+Coercions\\s-+Import") + ("Unset Automatic Introduction" nil "Unset Automatic Introduction" t "Unset Automatic\\s-+Introduction") + ("Unset Boolean Equality Schemes" nil "Unset Boolean Equality Schemes" t "Unset Boolean\\s-+Equality\\s-+Schemes") + ("Unset Bracketing Last Introduction Pattern" nil "Unset Bracketing Last Introduction Pattern" t "Unset Bracketing\\s-+Last\\s-+Introduction\\s-+Pattern") + ("Unset Bullet Behavior" nil "Unset Bullet Behavior" t "Unset Bullet\\s-+Behavior") + ("Unset Case Analysis Schemes" nil "Unset Case Analysis Schemes" t "Unset Case\\s-+Analysis\\s-+Schemes") + ("Unset Compat Notations" nil "Unset Compat Notations" t "Unset Compat\\s-+Notations") + ("Unset Congruence Depth" nil "Unset Congruence Depth" t "Unset Congruence\\s-+Depth") + ("Unset Congruence Verbose" nil "Unset Congruence Verbose" t "Unset Congruence\\s-+Verbose") + ("Unset Contextual Implicit" nil "Unset Contextual Implicit" t "Unset Contextual\\s-+Implicit") + ("Unset Debug Auto" nil "Unset Debug Auto" t "Unset Debug\\s-+Auto") + ("Unset Debug Eauto" nil "Unset Debug Eauto" t "Unset Debug\\s-+Eauto") + ("Unset Debug RAKAM" nil "Unset Debug RAKAM" t "Unset Debug\\s-+RAKAM") + ("Unset Debug Tactic Unification" nil "Unset Debug Tactic Unification" t "Unset Debug\\s-+Tactic\\s-+Unification") + ("Unset Debug Trivial" nil "Unset Debug Trivial" t "Unset Debug\\s-+Trivial") + ("Unset Debug Unification" nil "Unset Debug Unification" t "Unset Debug\\s-+Unification") + ("Unset Decidable Equality Schemes" nil "Unset Decidable Equality Schemes" t "Unset Decidable\\s-+Equality\\s-+Schemes") + ("Unset Default Clearing Used Hypotheses" nil "Unset Default Clearing Used Hypotheses" t "Unset Default\\s-+Clearing\\s-+Used\\s-+Hypotheses") + ("Unset Default Goal Selector" nil "Unset Default Goal Selector" t "Unset Default\\s-+Goal\\s-+Selector") + ("Unset Default Proof Mode" nil "Unset Default Proof Mode" t "Unset Default\\s-+Proof\\s-+Mode") + ("Unset Default Proof Using" nil "Unset Default Proof Using" t "Unset Default\\s-+Proof\\s-+Using") + ("Unset Default Timeout" nil "Unset Default Timeout" t "Unset Default\\s-+Timeout") + ("Unset Dependent Propositions Elimination" nil "Unset Dependent Propositions Elimination" t "Unset Dependent\\s-+Propositions\\s-+Elimination") + ("Unset Discriminate Introduction" nil "Unset Discriminate Introduction" t "Unset Discriminate\\s-+Introduction") + ("Unset Dump Bytecode" nil "Unset Dump Bytecode" t "Unset Dump\\s-+Bytecode") + ("Unset Elimination Schemes" nil "Unset Elimination Schemes" t "Unset Elimination\\s-+Schemes") + ("Unset Equality Scheme" nil "Unset Equality Scheme" t "Unset Equality\\s-+Scheme") + ("Unset Extraction AccessOpaque" nil "Unset Extraction AccessOpaque" t "Unset Extraction\\s-+AccessOpaque") + ("Unset Extraction AutoInline" nil "Unset Extraction AutoInline" t "Unset Extraction\\s-+AutoInline") + ("Unset Extraction Conservative Types" nil "Unset Extraction Conservative Types" t "Unset Extraction\\s-+Conservative\\s-+Types") + ("Unset Extraction File Comment" nil "Unset Extraction File Comment" t "Unset Extraction\\s-+File\\s-+Comment") + ("Unset Extraction Flag" nil "Unset Extraction Flag" t "Unset Extraction\\s-+Flag") + ("Unset Extraction KeepSingleton" nil "Unset Extraction KeepSingleton" t "Unset Extraction\\s-+KeepSingleton") + ("Unset Extraction Optimize" nil "Unset Extraction Optimize" t "Unset Extraction\\s-+Optimize") + ("Unset Extraction SafeImplicits" nil "Unset Extraction SafeImplicits" t "Unset Extraction\\s-+SafeImplicits") + ("Unset Extraction TypeExpand" nil "Unset Extraction TypeExpand" t "Unset Extraction\\s-+TypeExpand") + ("Unset Firstorder Depth" nil "Unset Firstorder Depth" t "Unset Firstorder\\s-+Depth") + ("Unset Hide Obligations" nil "Unset Hide Obligations" t "Unset Hide\\s-+Obligations") + ("Unset Implicit Arguments" nil "Unset Implicit Arguments" t "Unset Implicit\\s-+Arguments") + ("Unset Info Auto" nil "Unset Info Auto" t "Unset Info\\s-+Auto") + ("Unset Info Eauto" nil "Unset Info Eauto" t "Unset Info\\s-+Eauto") + ("Unset Info Level" nil "Unset Info Level" t "Unset Info\\s-+Level") + ("Unset Info Trivial" nil "Unset Info Trivial" t "Unset Info\\s-+Trivial") + ("Unset Injection L2R Pattern Order" nil "Unset Injection L2R Pattern Order" t "Unset Injection\\s-+L2R\\s-+Pattern\\s-+Order") + ("Unset Injection On Proofs" nil "Unset Injection On Proofs" t "Unset Injection\\s-+On\\s-+Proofs") + ("Unset Inline Level" nil "Unset Inline Level" t "Unset Inline\\s-+Level") + ("Unset Intuition Iff Unfolding" nil "Unset Intuition Iff Unfolding" t "Unset Intuition\\s-+Iff\\s-+Unfolding") + ("Unset Intuition Negation Unfolding" nil "Unset Intuition Negation Unfolding" t "Unset Intuition\\s-+Negation\\s-+Unfolding") + ("Unset Kernel Term Sharing" nil "Unset Kernel Term Sharing" t "Unset Kernel\\s-+Term\\s-+Sharing") + ("Unset Keyed Unification" nil "Unset Keyed Unification" t "Unset Keyed\\s-+Unification") + ("Unset Loose Hint Behavior" nil "Unset Loose Hint Behavior" t "Unset Loose\\s-+Hint\\s-+Behavior") + ("Unset Maximal Implicit Insertion" nil "Unset Maximal Implicit Insertion" t "Unset Maximal\\s-+Implicit\\s-+Insertion") + ("Unset Nonrecursive Elimination Schemes" nil "Unset Nonrecursive Elimination Schemes" t "Unset Nonrecursive\\s-+Elimination\\s-+Schemes") + ("Unset Parsing Explicit" nil "Unset Parsing Explicit" t "Unset Parsing\\s-+Explicit") + ("Unset Primitive Projections" nil "Unset Primitive Projections" t "Unset Primitive\\s-+Projections") + ("Unset Printing All" nil "Unset Printing All" t "Unset Printing\\s-+All") + ("Unset Printing Coercions" nil "Unset Printing Coercions" t "Unset Printing\\s-+Coercions") + ("Unset Printing Depth" nil "Unset Printing Depth" t "Unset Printing\\s-+Depth") + ("Unset Printing Existential Instances" nil "Unset Printing Existential Instances" t "Unset Printing\\s-+Existential\\s-+Instances") + ("Unset Printing Implicit" nil "Unset Printing Implicit" t "Unset Printing\\s-+Implicit") + ("Unset Printing Implicit Defensive" nil "Unset Printing Implicit Defensive" t "Unset Printing\\s-+Implicit\\s-+Defensive") + ("Unset Printing Matching" nil "Unset Printing Matching" t "Unset Printing\\s-+Matching") + ("Unset Printing Notations" nil "Unset Printing Notations" t "Unset Printing\\s-+Notations") + ("Unset Printing Primitive Projection Compatibility" nil "Unset Printing Primitive Projection Compatibility" t "Unset Printing\\s-+Primitive\\s-+Projection\\s-+Compatibility") + ("Unset Printing Primitive Projection Parameters" nil "Unset Printing Primitive Projection Parameters" t "Unset Printing\\s-+Primitive\\s-+Projection\\s-+Parameters") + ("Unset Printing Projections" nil "Unset Printing Projections" t "Unset Printing\\s-+Projections") + ("Unset Printing Records" nil "Unset Printing Records" t "Unset Printing\\s-+Records") + ("Unset Printing Synth" nil "Unset Printing Synth" t "Unset Printing\\s-+Synth") + ("Unset Printing Universes" nil "Unset Printing Universes" t "Unset Printing\\s-+Universes") + ("Unset Printing Width" nil "Unset Printing Width" t "Unset Printing\\s-+Width") + ("Unset Printing Wildcard" nil "Unset Printing Wildcard" t "Unset Printing\\s-+Wildcard") + ("Unset Program Mode" nil "Unset Program Mode" t "Unset Program\\s-+Mode") + ("Unset Proof Using Clear Unused" nil "Unset Proof Using Clear Unused" t "Unset Proof\\s-+Using\\s-+Clear\\s-+Unused") + ("Unset Record Elimination Schemes" nil "Unset Record Elimination Schemes" t "Unset Record\\s-+Elimination\\s-+Schemes") + ("Unset Refine Instance Mode" nil "Unset Refine Instance Mode" t "Unset Refine\\s-+Instance\\s-+Mode") + ("Unset Regular Subst Tactic" nil "Unset Regular Subst Tactic" t "Unset Regular\\s-+Subst\\s-+Tactic") + ("Unset Reversible Pattern Implicit" nil "Unset Reversible Pattern Implicit" t "Unset Reversible\\s-+Pattern\\s-+Implicit") + ("Unset Rewriting Schemes" nil "Unset Rewriting Schemes" t "Unset Rewriting\\s-+Schemes") + ("Unset Short Module Printing" nil "Unset Short Module Printing" t "Unset Short\\s-+Module\\s-+Printing") + ("Unset Shrink Obligations" nil "Unset Shrink Obligations" t "Unset Shrink\\s-+Obligations") + ("Unset SimplIsCbn" nil "Unset SimplIsCbn" t "Unset SimplIsCbn") + ("Unset Standard Proposition Elimination Names" nil "Unset Standard Proposition Elimination Names" t "Unset Standard\\s-+Proposition\\s-+Elimination\\s-+Names") + ("Unset Strict Proofs" nil "Unset Strict Proofs" t "Unset Strict\\s-+Proofs") + ("Unset Strict Universe Declaration" nil "Unset Strict Universe Declaration" t "Unset Strict\\s-+Universe\\s-+Declaration") + ("Unset Strongly Strict Implicit" nil "Unset Strongly Strict Implicit" t "Unset Strongly\\s-+Strict\\s-+Implicit") + ("Unset Suggest Proof Using" nil "Unset Suggest Proof Using" t "Unset Suggest\\s-+Proof\\s-+Using") + ("Unset Tactic Compat Context" nil "Unset Tactic Compat Context" t "Unset Tactic\\s-+Compat\\s-+Context") + ("Unset Tactic Evars Pattern Unification" nil "Unset Tactic Evars Pattern Unification" t "Unset Tactic\\s-+Evars\\s-+Pattern\\s-+Unification") + ("Unset Tactic Pattern Unification" nil "Unset Tactic Pattern Unification" t "Unset Tactic\\s-+Pattern\\s-+Unification") + ("Unset Transparent Obligations" nil "Unset Transparent Obligations" t "Unset Transparent\\s-+Obligations") + ("Unset Typeclass Resolution After Apply" nil "Unset Typeclass Resolution After Apply" t "Unset Typeclass\\s-+Resolution\\s-+After\\s-+Apply") + ("Unset Typeclass Resolution For Conversion" nil "Unset Typeclass Resolution For Conversion" t "Unset Typeclass\\s-+Resolution\\s-+For\\s-+Conversion") + ("Unset Typeclasses Debug" nil "Unset Typeclasses Debug" t "Unset Typeclasses\\s-+Debug") + ("Unset Typeclasses Dependency Order" nil "Unset Typeclasses Dependency Order" t "Unset Typeclasses\\s-+Dependency\\s-+Order") + ("Unset Typeclasses Depth" nil "Unset Typeclasses Depth" t "Unset Typeclasses\\s-+Depth") + ("Unset Typeclasses Modulo Eta" nil "Unset Typeclasses Modulo Eta" t "Unset Typeclasses\\s-+Modulo\\s-+Eta") + ("Unset Typeclasses Strict Resolution" nil "Unset Typeclasses Strict Resolution" t "Unset Typeclasses\\s-+Strict\\s-+Resolution") + ("Unset Typeclasses Unique Instances" nil "Unset Typeclasses Unique Instances" t "Unset Typeclasses\\s-+Unique\\s-+Instances") + ("Unset Typeclasses Unique Solutions" nil "Unset Typeclasses Unique Solutions" t "Unset Typeclasses\\s-+Unique\\s-+Solutions") + ("Unset Universal Lemma Under Conjunction" nil "Unset Universal Lemma Under Conjunction" t "Unset Universal\\s-+Lemma\\s-+Under\\s-+Conjunction") + ("Unset Universe Minimization ToUnset" nil "Unset Universe Minimization ToUnset" t "Unset Universe\\s-+Minimization\\s-+ToUnset") + ("Unset Universe Polymorphism" nil "Unset Universe Polymorphism" t "Unset Universe\\s-+Polymorphism") + ("Unset Verbose Compat Notations" nil "Unset Verbose Compat Notations" t "Unset Verbose\\s-+Compat\\s-+Notations") + ("Unset Function_debug" nil "Unset Function_debug" t "Unset Function_debug") + ("Unset Function_raw_tcc" nil "Unset Function_raw_tcc" t "Unset Function_raw_tcc") + ("Unset Functional Induction Rewrite Dependent" nil "Unset Functional Induction Rewrite Dependent" t "Unset Functional\\s-+Induction\\s-+Rewrite\\s-+Dependent") + ("Unset Hyps Limit" nil "Unset Hyps Limit" t "Unset Hyps\\s-+Limit") + ("Unset Ltac Debug" nil "Unset Ltac Debug" t "Unset Ltac\\s-+Debug") + ("Unset Silent" nil "Unset Silent" t "Unset Silent") + ("Unset Undo" nil "Unset Undo" t "Unset Undo") + ("Unset Search Blacklist" nil "Unset Search Blacklist" t "Unset Search\\s-+Blacklist") + ("Unset Printing Coercion" nil "Unset Printing Coercion" t "Unset Printing\\s-+Coercion") + ("Unset Printing If" nil "Unset Printing If" t "Unset Printing\\s-+If") + ("Unset Printing Let" nil "Unset Printing Let" t "Unset Printing\\s-+Let") + ("Unset Printing Record" nil "Unset Printing Record" t "Unset Printing\\s-+Record") + ("Unset Printing Constructor" nil "Unset Printing Constructor" t "Unset Printing\\s-+Constructor") + ; ("print" "pr" "print #" "print") + ) "Command that are not declarations, definition or goal starters." ) + (defvar coq-ssreflect-commands-db '(("Unset Strict Implicit" "unsti" nil t "Strict\\s-+Implicit") ("Prenex Implicits" "pi" "Prenex Implicits #" t "Prenex\\s-+Implicits") @@ -876,13 +1114,13 @@ It is used: (coq-build-regexp-list-from-db coq-tacticals-db) "Keywords for tacticals in a Coq script.") -(defvar coq-symbol-binders "\\_<∀\\_>\\|\\_<∃\\_>\\|\\_<λ\\_>") +(defvar coq-symbol-binders "∀\\|∃\\|λ") + ;; From JF Monin: (defvar coq-reserved (append - coq-user-reserved-db '( "False" "True" "after" "as" "cofix" "fix" "forall" "fun" "match" "lazymatch" "multimatch" @@ -890,7 +1128,8 @@ It is used: "using" "with" "beta" "delta" "iota" "zeta" "after" "until" "at" "Sort" "Time" "dest" "where" ;; SSReflect user reserved. - "is" "nosimpl" "of")) + "is" "nosimpl" "of") + coq-user-reserved-db) "Reserved keywords of Coq.") ;; FIXME: ∀ and ∃ should be followed by a space in coq syntax. @@ -950,9 +1189,17 @@ It is used: "++>" "@" "->" - ".") + "." + "∧" + "∨" + "→" + "\\/" + "/\\" + "->") "Punctuation Symbols used by Coq.") +(defvar coq-symbols-regexp (regexp-opt coq-symbols)) + ;; ----- regular expressions (defvar coq-error-regexp "^\\(Error:\\|Discarding pattern\\|Syntax error:\\|System Error:\\|User Error:\\|User error:\\|Anomaly[:.]\\|Toplevel input[,]\\)" "A regexp indicating that the Coq process has identified an error.") @@ -963,7 +1210,7 @@ It is used: (defvar coq-id "\\(@\\|_\\|\\w\\)\\(\\w\\|\\s_\\)*") ;; Coq ca start an id with @ or _ (defvar coq-id-shy "\\(?:@\\|_\\|\\w\\)\\(?:\\w\\|\\s_\\)*") -; do not use proof-ids with a space separator! +; do not use proof-ids with a space separator! (defvar coq-ids (concat coq-id "\\(" "\\s-+" coq-id "\\)*")) (defun coq-first-abstr-regexp (paren end) @@ -974,29 +1221,37 @@ It is used: :type 'boolean :group 'coq) -(defconst coq-lambda-regexp "\\(?:\\_<fun\\_>\\|\\_<λ\\_>\\)") +(defcustom coq-symbol-highlight-enable nil + "Activates partial bound variable highlighting" + :type 'boolean + :group 'coq) + +(defconst coq-lambda-regexp "\\(?:\\_<fun\\_>\\|λ\\)") -(defconst coq-forall-regexp "\\(?:\\_<forall\\_>\\|\\_<∀\\_>\\)") -(defconst coq-exists-regexp "\\(?:\\_<exists\\_>\\|\\_<∃\\_>\\)") +(defconst coq-forall-regexp "\\(?:\\_<forall\\_>\\|∀\\)") +(defconst coq-exists-regexp "\\(?:\\_<exists\\_>\\|∃\\)") (defvar coq-font-lock-terms - (cons - (cons coq-symbol-binders 'coq-symbol-binder-face) - (if coq-variable-highlight-enable - (list - ;; lambda binders - (list (coq-first-abstr-regexp coq-lambda-regexp "\\(?:=>\\|:\\|,\\)") 1 'font-lock-variable-name-face) - ;; forall binder - (list (coq-first-abstr-regexp coq-forall-regexp "\\(?:,\\|:\\)") 1 'font-lock-variable-name-face) - (list (coq-first-abstr-regexp coq-exists-regexp "\\(?:,\\|:\\)") 1 'font-lock-variable-name-face) - ; (list "\\<forall\\>" - ; (list 0 font-lock-type-face) - ; (list (concat "[^ :]\\s-*\\(" coq-ids "\\)\\s-*") nil nil - ; (list 0 font-lock-variable-name-face))) - ;; parenthesized binders - (list (coq-first-abstr-regexp "(" ":[ a-zA-Z]") 1 'font-lock-variable-name-face) - (list (coq-first-abstr-regexp "{" ":[ a-zA-Z]") 1 'font-lock-variable-name-face) - ))) + (append + (list ;; flattened by append above + (cons coq-symbol-binders 'coq-symbol-binder-face)) + (when coq-symbol-highlight-enable + (list (cons coq-symbols-regexp 'coq-symbol-face))) + (when coq-variable-highlight-enable + (list + ;; lambda binders + (list (coq-first-abstr-regexp coq-lambda-regexp "\\(?:=>\\|:\\|,\\)") 1 'font-lock-variable-name-face) + ;; forall binder + (list (coq-first-abstr-regexp coq-forall-regexp "\\(?:,\\|:\\)") 1 'font-lock-variable-name-face) + (list (coq-first-abstr-regexp coq-exists-regexp "\\(?:,\\|:\\)") 1 'font-lock-variable-name-face) + ;; (list "\\<forall\\>" + ;; (list 0 font-lock-type-face) + ;; (list (concat "[^ :]\\s-*\\(" coq-ids "\\)\\s-*") nil nil + ;; (list 0 font-lock-variable-name-face))) + ;; parenthesized binders + (list (coq-first-abstr-regexp "(" ":[ a-zA-Z]") 1 'font-lock-variable-name-face) + (list (coq-first-abstr-regexp "{" ":[ a-zA-Z]") 1 'font-lock-variable-name-face) + ))) "*Font-lock table for Coq terms.") @@ -1050,38 +1305,36 @@ It is used: ;; (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^(.]*:\\|.*)[^(.]*:=\\)")) ;;"\\<Prop\\>\\|\\<Set\\>\\|\\<Type\\>" -;; (defconst coq-require-command-regexp -;; (concat "Require\\s-+\\(" coq-id "\\)") -;; "Regular expression matching Require commands in Coq. -;; Group number 1 matches the name of the library which is required.") + +(defconst coq-context-marker-regexp + (concat (regexp-opt '("ltac" "constr" "uconstr") 'symbols) ":")) ;; ;; font-lock ;; (defvar coq-font-lock-keywords-1 - (append - coq-font-lock-terms - (list - (cons coq-solve-tactics-regexp 'coq-solve-tactics-face) - (cons coq-solve-cheat-tactics-regexp 'coq-cheat-face) - (cons coq-keywords-regexp 'font-lock-keyword-face) - (cons coq-reserved-regexp 'font-lock-type-face) - (cons coq-tactics-regexp 'proof-tactics-name-face) - (cons (proof-regexp-alt-list coq-tacticals) 'proof-tacticals-name-face) - (cons (proof-regexp-alt-list-symb (list "Set" "Type" "Prop")) 'font-lock-type-face) - (cons "============================" 'font-lock-keyword-face) - (list coq-goal-with-hole-regexp 2 'font-lock-function-name-face)) - (if coq-variable-highlight-enable - (list (list coq-decl-with-hole-regexp 2 'font-lock-variable-name-face))) - (list - (list coq-defn-with-hole-regexp 2 'font-lock-function-name-face) - (list coq-with-with-hole-regexp 2 'font-lock-function-name-face) - (list coq-save-with-hole-regexp 2 'font-lock-function-name-face) - ;; Remove spurious variable and function faces on commas. - '(proof-zap-commas)))) - - -;; ", " is for multiple hypothesis diplayed in v8.5. If more than + (append + coq-font-lock-terms + `((,coq-solve-tactics-regexp . 'coq-solve-tactics-face) + (,coq-solve-cheat-tactics-regexp . 'coq-cheat-face) + (,coq-keywords-regexp . 'font-lock-keyword-face) + (,coq-reserved-regexp . 'font-lock-type-face) + (,coq-tactics-regexp . 'proof-tactics-name-face) + (,(proof-regexp-alt-list coq-tacticals) . 'proof-tacticals-name-face) + (,(proof-regexp-alt-list-symb (list "Set" "Type" "Prop")) . 'font-lock-type-face) + ("============================" . 'font-lock-keyword-face) + (,coq-goal-with-hole-regexp 2 'font-lock-function-name-face) + (,coq-context-marker-regexp 1 'coq-context-qualifier-face)) + (if coq-variable-highlight-enable + `((,coq-decl-with-hole-regexp 2 'font-lock-variable-name-face))) + `((,coq-defn-with-hole-regexp 2 'font-lock-function-name-face) + (,coq-with-with-hole-regexp 2 'font-lock-function-name-face) + (,coq-save-with-hole-regexp 2 'font-lock-function-name-face) + ;; Remove spurious variable and function faces on commas. + (proof-zap-commas)))) + + +;; ", " is for multiple hypothesis displayed in v8.5. If more than ;; 1 space this is a hypothesis displayed in the middle of a line (> v8.5) ;; "^ " is for goals in debug mode. (defvar coq-hyp-name-in-goal-or-response-regexp @@ -1128,14 +1381,15 @@ It is used: (modify-syntax-entry ?< ".") (modify-syntax-entry ?> ".") (modify-syntax-entry ?\& ".") - (modify-syntax-entry ?_ "_") - (modify-syntax-entry ?\' "_") - (modify-syntax-entry ?∀ "_") - (modify-syntax-entry ?∃ "_") - (modify-syntax-entry ?λ "_") ;; maybe a bad idea... lambda is a letter + (modify-syntax-entry ?_ "_") ; beware: word consituent EXCEPT in head position + (modify-syntax-entry ?\' "_") ; always word constituent + (modify-syntax-entry ?∀ ".") + (modify-syntax-entry ?∃ ".") + (modify-syntax-entry ?λ ".") ;; maybe a bad idea... lambda is a letter (modify-syntax-entry ?\| ".") ;; should maybe be "_" but it makes coq-find-and-forget (in coq.el) bug + ;; Hence the coq-with-altered-syntax-table below to put "." into "_" class temporarily (modify-syntax-entry ?\. ".") (modify-syntax-entry ?\* ". 23n") @@ -1146,6 +1400,7 @@ It is used: ;; constituent (better behavior for thing-at and maybe font-lock too, ;; for indentation we use ad hoc smie lexers). (defmacro coq-with-altered-syntax-table (&rest code) + (declare (debug t)) (let ((res (make-symbol "res"))) `(unwind-protect (progn (modify-syntax-entry ?\. "_") diff --git a/coq/coq-system.el b/coq/coq-system.el index 963a0985..0b9b6c58 100644 --- a/coq/coq-system.el +++ b/coq/coq-system.el @@ -30,7 +30,8 @@ On Windows you might need something like: :group 'coq) (defcustom coq-prog-name - (proof-locate-executable "coqtop" t '("C:/Program Files/Coq/bin")) + (if (executable-find "coqtop") "coqtop" + (proof-locate-executable "coqtop" t '("C:/Program Files/Coq/bin"))) "*Name of program to run as Coq. See `proof-prog-name', set from this. On Windows with latest Coq package you might need something like: C:/Program Files/Coq/bin/coqtop.opt.exe @@ -42,22 +43,26 @@ See also `coq-prog-env' to adjust the environment." :group 'coq) (defcustom coq-dependency-analyzer - (proof-locate-executable "coqdep" t '("C:/Program Files/Coq/bin")) + (if (executable-find "coqdep") "coqdep" + (proof-locate-executable "coqdep" t '("C:/Program Files/Coq/bin"))) "Command to invoke coqdep." :type 'string :group 'coq) (defcustom coq-compiler - (proof-locate-executable "coqc" t '("C:/Program Files/Coq/bin")) + (if (executable-find "coqc") "coqc" + (proof-locate-executable "coqc" t '("C:/Program Files/Coq/bin"))) "Command to invoke the coq compiler." :type 'string :group 'coq) (defun get-coq-library-directory () - (let ((c (substring (shell-command-to-string (concat coq-prog-name " -where")) 0 -1 ))) - (if (string-match "not found" c) - "/usr/local/lib/coq" - c))) + (let ((default-directory + (if (file-accessible-directory-p default-directory) + default-directory + "/"))) + (or (ignore-errors (car (process-lines coq-prog-name "-where"))) + "/usr/local/lib/coq"))) (defconst coq-library-directory (get-coq-library-directory) ;; FIXME Should be refreshed more often "The coq library directory, as reported by \"coqtop -where\".") @@ -69,14 +74,31 @@ See also `coq-prog-env' to adjust the environment." (defcustom coq-pinned-version nil "Which version of Coq you are using. -There should be no need to set this value; Proof General can -adjust to various releases of Coq automatically." +There should be no need to set this value unless you use the trunk from +the Coq github repository. For Coq versions with decent version numbers +Proof General detects the version automatically and adjusts itself. This +variable should contain nil or a version string." :type 'string :group 'coq) (defvar coq-autodetected-version nil "Version of Coq, as autodetected by `coq-autodetect-version'.") +;;; error symbols + +;; coq-unclassifiable-version +;; +;; This error is signaled with one data item -- the bad version string + +(put 'coq-unclassifiable-version 'error-conditions + '(error coq-unclassifiable-version)) + +(put 'coq-unclassifiable-version 'error-message + "Proof General cannot classify your Coq version") + + +;;; version detection code + (defun coq-version (&optional may-recompute) "Return the precomputed version of the current Coq toolchain. With MAY-RECOMPUTE, try auto-detecting it if it isn't available." @@ -99,19 +121,37 @@ If it doesn't look right, try `coq-autodetect-version'." Interactively (with INTERACTIVE-P), show that number." (interactive '(t)) (setq coq-autodetected-version nil) - (let ((version-string (car (process-lines "coqtop" "-v")))) - (when (and version-string (string-match "version \\([^ ]+\\)" version-string)) - (setq coq-autodetected-version (match-string 1 version-string)))) + (with-temp-buffer + ;; Use `shell-command' via `find-file-name-handler' instead of + ;; `process-line': when the buffer is running TRAMP, PG uses + ;; `start-file-process', loading the binary from the remote server. + (let* ((default-directory + (if (file-accessible-directory-p default-directory) + default-directory + "/")) + (coq-command (shell-quote-argument (or coq-prog-name "coqtop"))) + (shell-command-str (format "%s -v" coq-command)) + (fh (find-file-name-handler default-directory 'shell-command)) + (retv (if fh (funcall fh 'shell-command shell-command-str (current-buffer)) + (shell-command shell-command-str (current-buffer))))) + (when (equal 0 retv) + ;; Fail silently (in that case we'll just assume Coq 8.5) + (goto-char (point-min)) + (when (re-search-forward "version \\([^ ]+\\)" nil t) + (setq coq-autodetected-version (match-string 1)))))) (when interactive-p (coq-show-version)) coq-autodetected-version) -(defun coq--version< (v1 v2) ;; !!! Check availability in 24.3 +(defun coq--version< (v1 v2) "Compare Coq versions V1 and V2." - (let ((version-regexp-alist (cons '("^pl$" . 0) version-regexp-alist))) + ;; -snapshot is only supported by Emacs 24.5, not 24.3 + (let ((version-regexp-alist `(("^[-_+ ]?snapshot$" . -4) + ("^pl$" . 0) + ,@version-regexp-alist))) (version< v1 v2))) -(defcustom coq-pre-v85 nil ;; !!! Mark deprecated +(defcustom coq-pre-v85 nil "Deprecated. Use `coq-pinned-version' if you want to bypass the version detection that Proof General does automatically." @@ -121,7 +161,26 @@ version detection that Proof General does automatically." (defun coq--pre-v85 () "Return non-nil if the auto-detected version of Coq is < 8.5. Returns nil if the version can't be detected." - (coq--version< (or (coq-version t) "8.5") "8.5snapshot")) + (let ((coq-version-to-use (or (coq-version t) "8.5"))) + (condition-case err + (coq--version< coq-version-to-use "8.5snapshot") + (error + (cond + ((equal (substring (cadr err) 0 15) "Invalid version") + (signal 'coq-unclassifiable-version coq-version-to-use)) + (t (signal (car err) (cdr err)))))))) + +(defun coq--post-v86 () + "Return t if the auto-detected version of Coq is >= 8.6. +Return nil if the version cannot be detected." + (let ((coq-version-to-use (or (coq-version t) "8.5"))) + (condition-case err + (not (coq--version< coq-version-to-use "8.6")) + (error + (cond + ((equal (substring (cadr err) 0 15) "Invalid version") + (signal 'coq-unclassifiable-version coq-version-to-use)) + (t (signal (car err) (cdr err)))))))) (defcustom coq-use-makefile nil "Whether to look for a Makefile to attempt to guess the command line. @@ -237,30 +296,32 @@ This setting is only relevant with Coq < 8.5." (make-obsolete-variable 'coq-load-path-include-current "Coq 8.5 does not need it" "4.3") - (defun coq-option-of-load-path-entry (entry &optional pre-v85) - "Translate a single ENTRY from `coq-load-path' into options. +(defun coq-option-of-load-path-entry (entry &optional pre-v85) + "Translate a single ENTRY from `coq-load-path' into options. See `coq-load-path' for the possible forms of ENTRY and to which options they are translated. Use a non-nil PRE-V85 flag to request compatibility handling of flags." - (if pre-v85 ;; !!! Which base directory do we expand against? Should the entries of load-path just always be absolute? - ;; Note that we don't handle 'recnoimport in 8.4, and we don't handle - ;; 'nonrec in 8.5. - (pcase entry - ((or (and (pred stringp) dir) `(ocamlimport ,dir)) - (list "-I" (expand-file-name dir))) - (`(nonrec ,dir ,alias) - (list "-I" (expand-file-name dir) "-as" alias)) - ((or `(rec ,dir ,alias) `(,dir ,alias)) - (list "-R" (expand-file-name dir) alias))) - (pcase entry - ((and (pred stringp) dir) - (list "-Q" (expand-file-name dir) "")) - (`(ocamlimport ,dir) - (list "-I" (expand-file-name dir))) - (`(recnoimport ,dir ,alias) - (list "-Q" (expand-file-name dir) alias)) - ((or `(rec ,dir ,alias) `(,dir ,alias)) - (list "-R" (expand-file-name dir) alias))))) + (if pre-v85 + ;; FIXME Which base directory do we expand against? Should the entries of + ;; load-path just always be absolute? + ;; NOTE we don't handle 'recnoimport in 8.4, and we don't handle 'nonrec + ;; in 8.5. + (pcase entry + ((or (and (pred stringp) dir) `(ocamlimport ,dir)) + (list "-I" (expand-file-name dir))) + (`(nonrec ,dir ,alias) + (list "-I" (expand-file-name dir) "-as" alias)) + ((or `(rec ,dir ,alias) `(,dir ,alias)) + (list "-R" (expand-file-name dir) alias))) + (pcase entry + ((and (pred stringp) dir) + (list "-Q" (expand-file-name dir) "")) + (`(ocamlimport ,dir) + (list "-I" (expand-file-name dir))) + (`(recnoimport ,dir ,alias) + (list "-Q" (expand-file-name dir) alias)) + ((or `(rec ,dir ,alias) `(,dir ,alias)) + (list "-R" (expand-file-name dir) alias))))) (defun coq-include-options (load-path &optional current-directory pre-v85) "Build the base list of include options for coqc, coqdep and coqtop. @@ -319,13 +380,11 @@ options of a few coq-project files does the right thing." LOAD-PATH, CURRENT-DIRECTORY, PRE-V85: see `coq-include-options'." (coq-include-options load-path current-directory pre-v85)) -;;; !!! Fixme handle proof-prog-name-ask - (defun coq-coqc-prog-args (load-path &optional current-directory pre-v85) "Build a list of options for coqc. LOAD-PATH, 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. ;; !!! Check this comment + ;; include it in the -Q options. (append (remove "-emacs" (remove "-emacs-U" coq-prog-args)) (let ((coq-load-path-include-current nil)) ; Not needed in >=8.5beta3 (coq-coqdep-prog-args coq-load-path current-directory pre-v85)))) @@ -336,7 +395,7 @@ LOAD-PATH, CURRENT-DIRECTORY, PRE-V85: see `coq-include-options'." ;; documentation. (defun coq-coqtop-prog-args (load-path &optional current-directory pre-v85) - ;; coqtop always adds the current directory to the LoadPath, so don't ;; !!! Check this comment + ;; 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. LOAD-PATH, CURRENT-DIRECTORY, PRE-V85: see `coq-coqc-prog-args'." @@ -355,8 +414,9 @@ project file (see `coq-project-filename') somewhere in the current directory or its parent directories. If there is one, its contents are read and used to determine the arguments that must be given to coqtop. In particular it sets the load -path (including the -R lib options) (see `coq-load-path') ." +path (including the -R lib options) (see `coq-load-path')." :type 'boolean + :safe 'booleanp :group 'coq) (defcustom coq-project-filename "_CoqProject" @@ -373,6 +433,7 @@ 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 'string + :safe 'stringp :group 'coq) (defun coq-find-project-file () @@ -435,7 +496,7 @@ coqtop." (push opt args)) (`("-arg" ,concatenated-args) (setq args - (append (split-string (cadr opt) coq--project-file-separator) + (append (split-string-and-unquote (cadr opt) coq--project-file-separator) args))))) (cons "-emacs" args))) @@ -24,6 +24,8 @@ (defvar proof-info nil) ; dynamic scope in proof-tree-urgent-action (defvar action nil) ; dynamic scope in coq-insert-as stuff (defvar string nil) ; dynamic scope in coq-insert-as stuff + (defvar old-proof-marker nil) + ; dynamic scoq in coq-proof-tree-enable-evar-callback (defvar coq-auto-insert-as nil) ; defpacustom (defvar coq-time-commands nil) ; defpacustom (defvar coq-use-project-file t) ; defpacustom @@ -81,6 +83,11 @@ These are appended at the end of `coq-shell-init-cmd'." :type '(repeat (cons (string :tag "command"))) :group 'coq) +(defcustom coq-optimise-resp-windows-enable t + "If non-nil (default) resize vertically response windw after each command." + :type 'boolean + :group 'coq) + ;; Default coq is only Private_ and _subproof (defcustom coq-search-blacklist-string ; add this? \"_ind\" \"_rect\" \"_rec\" "\"Private_\" \"_subproof\"" @@ -88,6 +95,11 @@ These are appended at the end of `coq-shell-init-cmd'." :type 'string :group 'coq) +(defcustom coq-prefer-top-of-conclusion nil + "prefer start of the conclusion over its end when displaying goals +that do not fit in the goals window." + :type 'boolean + :group 'coq) ;; this remembers the previous value of coq-search-blacklist-string, so that we ;; can cook a remove+add blacklist command each time the variable is changed. @@ -169,13 +181,14 @@ See also `coq-hide-additional-subgoals'." (defcustom coq-navigation-command-regexp (concat "^\\(\\(Focus\\)\\|\\(Unfocus\\)\\|" + "\\(all\\s-*:\\s-*\\(cycle\\|swap\\|revgoals\\)\\)\\|" "\\(\\+\\)\\|\\(-\\)\\|\\(\\*\\)\\|\\({\\)\\|\\(}\\)\\)") "Regexp for `proof-tree-navigation-command-regexp'." :type 'regexp :group 'coq-proof-tree) (defcustom coq-proof-tree-cheating-regexp - "admit" + "\\(?:admit\\)\\|\\(?:give_up\\)" "Regexp for `proof-tree-cheating-regexp'." :type 'regexp :group 'coq-proof-tree) @@ -187,8 +200,9 @@ See also `coq-hide-additional-subgoals'." :group 'coq-proof-tree) (defcustom coq-proof-tree-current-goal-regexp - (concat "^[0-9]+ \\(?:focused \\)?subgoal\\(?:s\\)?" - "\\(?: (unfocused: [-0-9]+)\\)?\\(?:\\s-*, subgoal 1\\)? " + (concat "^[0-9]+ \\(?:focused \\)?subgoal\\(?:s\\)?\\s-*" + "\\(?:(\\(?:unfocused: [-0-9]+\\)?,?" + "\\s-*\\(?:shelved: [-0-9]+\\)?)\\)?\\(?:\\s-*, subgoal 1\\)? " "(ID \\([0-9]+\\))\n\\s-*\n\\(\\(?: .*\n\\)+\\)\\(?:\n\\|$\\)") "Regexp for `proof-tree-current-goal-regexp'." :type 'regexp @@ -229,13 +243,26 @@ See also `coq-hide-additional-subgoals'." :type 'regexp :group 'coq-proof-tree) -;; pc: <infomsg> now has a newline (better output indentation) +;; 8.4: +;; <infomsg>This subproof is complete, but there are still unfocused goals.</infomsg> +;; +;; 8.5: +;; <infomsg> +;; This subproof is complete, but there are some unfocused goals. +;; Focus next goal with bullet *. +;; </infomsg> +;; +;; <infomsg>No more subgoals, but there are some goals you gave up:</infomsg> +;; +;; <infomsg>All the remaining goals are on the shelf.</infomsg> (defcustom coq-proof-tree-branch-finished-regexp - (concat "^\\(\\(?:Proof completed\\.\\)\\|\\(?:No more subgoals\\.\\)\\|" + (concat "^\\(\\(?:Proof completed\\.\\)\\|" + "\\(?:\\(?:<infomsg>\\)?No more subgoals\\)\\|" "\\(No more subgoals but non-instantiated " "existential variables:\\)\\|" + "\\(?:<infomsg>All the remaining goals are on the shelf\\)\\|" "\\(<infomsg>\\s-*This subproof is complete, but there are " - "still unfocused goals.\\s-*</infomsg>\\)\\)") + "\\(?:still\\|some\\) unfocused goals.\\)\\)") "Regexp for `proof-tree-branch-finished-regexp'." :type 'regexp :group 'coq-proof-tree) @@ -796,6 +823,16 @@ Return nil if S is nil." (substring s 0 (- (length s) 1)) s)) +(defun coq-remove-heading-quote (s) + "Return the string S without its heading \"\'\" if any. +Return nil if S is nil." + (if (and s (string-match "\\`'" s)) + (substring s 1 (length s)) + s)) + +(defun coq-clean-id-at-point (s) + (coq-remove-heading-quote (coq-remove-trailing-dot s))) + (defun coq-is-symbol-or-punct (c) "Return non nil if character C is a punctuation or a symbol constituent. If C is nil, return nil." @@ -840,15 +877,15 @@ Support dot.notation.of.modules." (let* ((symb (cond ((fboundp 'symbol-near-point) (symbol-near-point)) ((fboundp 'symbol-at-point) (symbol-at-point)))) - (symbclean (when symb (coq-remove-trailing-dot (symbol-name symb))))) - (when (and symb (not (zerop (length symbclean))) - (not (coq-string-starts-with-symbol symbclean))) + (symbclean (when symb (coq-clean-id-at-point (symbol-name symb))))) + (when (and symb (not (zerop (length symbclean)))) symbclean)))) (defun coq-id-or-notation-at-point () - (or (coq-id-at-point) (concat "\"" (coq-notation-at-position (point)) "\""))) - + (or (coq-id-at-point) + (let ((notation (coq-notation-at-position (point)))) + (if notation (concat "\"" notation "\"") "")))) (defcustom coq-remap-mouse-1 nil "Wether coq mode should remap mouse button 1 to coq queries. @@ -1194,6 +1231,7 @@ width is synchronized by coq (?!)." :group 'coq :eval (coq-set-auto-adapt-printing-width)) + ;; defpacustom fails to call :eval during inititialization, see trac #456 (coq-set-auto-adapt-printing-width) @@ -1298,11 +1336,10 @@ goal is redisplayed." (let* ((id (coq-id-or-notation-at-point)) (re (regexp-quote (or id "")))) (when coq-highlight-id-last-regexp - (coq-unhighlight-id-in-goals coq-highlight-id-last-regexp) - (if (equal id coq-highlight-id-last-regexp) - (setq coq-highlight-id-last-regexp "") - (coq-highlight-id-in-goals re) - (setq coq-highlight-id-last-regexp re))))) + (coq-unhighlight-id-in-goals coq-highlight-id-last-regexp)) + (coq-highlight-id-in-goals re) + (setq coq-highlight-id-last-regexp re))) + (proof-definvisible coq-PrintHint "Print Hint. ") @@ -1311,14 +1348,16 @@ goal is redisplayed." (proof-definvisible coq-show-proof "Show Proof.") (proof-definvisible coq-show-conjectures "Show Conjectures.") (proof-definvisible coq-show-intros "Show Intros.") ; see coq-insert-intros below -(proof-definvisible coq-set-implicit-arguments "Set Implicit Arguments.") -(proof-definvisible coq-unset-implicit-arguments "Unset Implicit Arguments.") +(proof-definvisible coq-set-printing-implicit "Set Printing Implicit.") +(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-synth "Set Printing Synth.") (proof-definvisible coq-unset-printing-synth "Unset Printing Synth.") (proof-definvisible coq-set-printing-coercions "Set Printing Coercions.") (proof-definvisible coq-unset-printing-coercions "Unset Printing Coercions.") +(proof-definvisible coq-set-printing-universes "Set Printing Universes.") +(proof-definvisible coq-unset-printing-universes "Unset Printing Universes.") (proof-definvisible coq-set-printing-wildcards "Set Printing Wildcard.") (proof-definvisible coq-unset-printing-wildcards "Unset Printing Wildcard.") ; Takes an argument @@ -1398,7 +1437,7 @@ Near here means PT is either inside or just aside of a comment." (cond ((coq-looking-at-comment) (coq-get-comment-region (point))) - ((and (looking-back proof-script-comment-end) + ((and (looking-back proof-script-comment-end nil) (save-excursion (forward-char -1) (coq-looking-at-comment))) (coq-get-comment-region (- (point) 1))) ((and (looking-at proof-script-comment-start) @@ -1465,8 +1504,7 @@ Near here means PT is either inside or just aside of a comment." (set (make-local-variable 'open-paren-in-column-0-is-defun-start) nil) ;; do not break lines in code when filling (set (make-local-variable 'fill-nobreak-predicate) - (lambda () - (not (eq (get-text-property (point) 'face) 'font-lock-comment-face)))) + (lambda () (not (nth 4 (syntax-ppss))))) ;; coq mode specific indentation function (set (make-local-variable 'fill-paragraph-function) 'coq-fill-paragraph-function) @@ -1752,7 +1790,7 @@ Near here means PT is either inside or just aside of a comment." (defpacustom search-blacklist coq-search-blacklist-string "Strings to blacklist in requests to coq environment." :type 'string - :get coq-search-blacklist-string + :get 'coq-get-search-blacklist :setting coq-set-search-blacklist) @@ -1810,27 +1848,45 @@ processing, the sequent text is send to prooftree as a sequent update (see `proof-tree-update-sequent') and the ID of the sequent is registered as known in `proof-tree-sequent-hash'. +Searching for new subgoals must only be done when the proof is +not finished, because Coq 8.5 lists open existential variables +as (new) open subgoals. For this test we assume that +`proof-marker' has not yet been moved. + +The `proof-tree-urgent-action-hook' is also called for undo +commands. For those, nothing is done. + The not yet delayed output is in the region \[proof-shell-delayed-output-start, proof-shell-delayed-output-end]." ;; (message "CPTGNS start %s end %s" ;; proof-shell-delayed-output-start ;; proof-shell-delayed-output-end) - (with-current-buffer proof-shell-buffer - (let ((start proof-shell-delayed-output-start) - (end proof-shell-delayed-output-end)) - (goto-char start) - (while (proof-re-search-forward - coq-proof-tree-additional-subgoal-ID-regexp end t) - (let ((subgoal-id (match-string-no-properties 1))) - (unless (gethash subgoal-id proof-tree-sequent-hash) - (setq proof-action-list - (cons (proof-shell-action-list-item - (coq-show-sequent-command subgoal-id) - (proof-tree-make-show-goal-callback (car proof-info)) - '(no-goals-display - no-response-display - proof-tree-show-subgoal)) - proof-action-list)))))))) + (let ((start proof-shell-delayed-output-start) + (end proof-shell-delayed-output-end) + (state (car proof-info))) + (when (> state proof-tree-last-state) + (with-current-buffer proof-shell-buffer + ;; The message "All the remaining goals are on the shelf" is processed as + ;; urgent message and is therefore before + ;; proof-shell-delayed-output-start. We therefore need to go back to + ;; proof-marker. + (goto-char proof-marker) + (unless (proof-re-search-forward + coq-proof-tree-branch-finished-regexp end t) + (goto-char start) + (while (proof-re-search-forward + coq-proof-tree-additional-subgoal-ID-regexp end t) + (let ((subgoal-id (match-string-no-properties 1))) + (unless (gethash subgoal-id proof-tree-sequent-hash) + ;; (message "CPTGNS new sequent %s found" subgoal-id) + (setq proof-action-list + (cons (proof-shell-action-list-item + (coq-show-sequent-command subgoal-id) + (proof-tree-make-show-goal-callback (car proof-info)) + '(no-goals-display + no-response-display + proof-tree-show-subgoal)) + proof-action-list)))))))))) (add-hook 'proof-tree-urgent-action-hook 'coq-proof-tree-get-new-subgoals) @@ -1867,6 +1923,103 @@ This is the Coq incarnation of `proof-tree-find-undo-position'." (span-start span-res))) +;; In Coq 8.6 the evar line is disabled by default because on some proofs it +;; causes a severe performance hit. The disabled evar line causes prooftree to +;; crash with a parsing error. Proof General must therefore turn on the evar +;; output with the command "Set Printing Dependent Evars Line". Of course, +;; after the proof, the evar line must be set back to what it was before the +;; proof. I therefore look in the urgent action hook if proof display is +;; switched on or off. When switched on, I test the current evar printing +;; status with the undodumented command "Test Printing Dependent Evars Line" to +;; remember if I have to switch evar printing off eventually. + +(defvar coq--proof-tree-must-disable-evars nil + "Remember if evar printing must be disabled when leaving the current proof.") + +(defun coq-proof-tree-enable-evar-callback (span) + "Callback for the evar printing status test. +This is the callback for the command ``Test Printing Dependent +Evars Line''. It checks whether evar printing was off and +remembers that fact in `coq--proof-tree-must-disable-evars'." + (with-current-buffer proof-shell-buffer + (save-excursion + ;; When the callback runs, the next item is sent to Coq already and + ;; therefore proof-marker points to the end of the next command + ;; already. proof-shell-filter-manage-output sets old-proof-marker + ;; before calling proof-shell-exec-loop, this therefore points to the + ;; end of the command of this callback. + (goto-char old-proof-marker) + (when (re-search-forward "The Printing Dependent Evars Line mode is " + nil t) + (if (looking-at "off") + (progn + ;; (message "CPTEEC evar line mode was off") + (setq coq--proof-tree-must-disable-evars t)) + ;; (message "CPTEEC evar line mode was on") + (setq coq--proof-tree-must-disable-evars nil)))))) + +(defun coq-proof-tree-insert-evar-command (cmd &optional callback) + "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) + (list 'invisible)) + proof-action-list)) + +(defun coq-proof-tree-enable-evars () + "Enable the evar status line for Coq >= 8.6. +Test the status of evar printing to be able to set it back +properly after the proof and enable the evar printing." + (when (coq--post-v86) + ;; We push to proof-action-list --- therefore we need to push in reverse + ;; order! + (coq-proof-tree-insert-evar-command "Set") + (coq-proof-tree-insert-evar-command + "Test" + 'coq-proof-tree-enable-evar-callback))) + +(defun coq-proof-tree-disable-evars () + "Disable evar printing if necessary. +This function switches off evar printing after the proof, if it +was off before the proof. For undo commands, we rely on the fact +that Coq itself undos the effect of the evar printing change that +we inserted after the goal statement. We also rely on the fact +that Proof General never backtracks into the middle of a +proof. (If this would happen, Coq would switch evar printing on +and the code here would not switch it off after the proof.) + +Being called from `proof-tree-urgent-action-hook', this function +can rely on `proof-info' being dynamically bound to the last +result of `coq-proof-tree-get-proof-info'." + (when coq--proof-tree-must-disable-evars + (when (> (car proof-info) proof-tree-last-state) + (coq-proof-tree-insert-evar-command "Unset")) + (setq coq--proof-tree-must-disable-evars nil))) + +(defun coq-proof-tree-evar-display-toggle () + "Urgent action hook function for changing the evar printing status in Coq. +This function is for `proof-tree-urgent-action-hook' (which is +called only if external proof disaply is switched on). It checks +whether a proof was started or stopped and inserts commands for +enableing and disabling the evar status line for Coq 8.6 or +later. Without the evar status line being enabled, prooftree +crashes. + +Must only be called via `proof-tree-urgent-action-hook' to ensure +that the dynamic variable `proof-info' is bound to the current +result of `coq-proof-tree-get-proof-info'." + (let ((current-proof-name (cadr proof-info))) + (cond + ((and (null proof-tree-current-proof) current-proof-name) + ;; started a new proof + (coq-proof-tree-enable-evars)) + ((and proof-tree-current-proof (null current-proof-name)) + ;; finished the current proof + (coq-proof-tree-disable-evars))))) + +(add-hook 'proof-tree-urgent-action-hook 'coq-proof-tree-evar-display-toggle) + + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; Pre-processing of input string @@ -1876,11 +2029,17 @@ This is the Coq incarnation of `proof-tree-find-undo-position'." (defconst coq--time-prefix "Time " "Coq command prefix for displaying timing information.") +(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 () - (if coq-time-commands - (with-no-warnings ;; NB: dynamic scoping of `string' - (setq string (concat coq--time-prefix string))))) + (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 + (unless (or (eq action 'proof-done-invisible) + (coq-bullet-p string)) ;; coq does not accept "Time -". + (setq string (concat coq--time-prefix string)))))) (add-hook 'proof-shell-insert-hook 'coq-preprocessing) @@ -2013,20 +2172,28 @@ mouse activation." (progn (end-of-line) (point))))))) (insert (concat "End" section))))) +(defun coq--format-intros (output) + "Create an “intros” form from the OUTPUT of “Show Intros”." + (let* ((shints (replace-regexp-in-string "[\r\n ]*\\'" "" output))) + (if (or (string= "" shints) + (string-match coq-error-regexp shints)) + (error "Don't know what to intro") + (format "intros %s" shints)))) + (defun coq-insert-intros () "Insert an intros command with names given by Show Intros. Based on idea mentioned in Coq reference manual." (interactive) - (let* ((shints (proof-shell-invisible-cmd-get-result "Show Intros.")) - ;; insert a dot before the trailing \n and put intros at begining - (intros (concat "intros " (substring shints 0 (- (length shints) 1)) ".\n"))) - (if (or (< (length shints) 2);; empty response is just NL - (string-match coq-error-regexp shints)) - (error "Don't know what to intro") - (let ((pt (point))) - (insert intros) - (indent-region pt (point)))))) - + (let* ((output (proof-shell-invisible-cmd-get-result "Show Intros."))) + (indent-region (point) + (progn (insert (coq--format-intros output)) + (save-excursion + (insert (if coq-one-command-per-line "\n" " ")) + (point)))) + ;; `proof-electric-terminator' moves the point in all sorts of strange + ;; ways, so we run it last + (let ((last-command-event ?.)) ;; Insert a dot + (proof-electric-terminator)))) (defvar coq-keywords-accepting-as-regex (regexp-opt '("induction" "destruct" "inversion" "injection"))) @@ -2387,6 +2554,7 @@ buffer." (buffer-substring p (point))))))) + (defun coq-show-first-goal () "Scroll the goal buffer so that the first goal is visible. First goal is displayed on the bottom of its window, maximizing the @@ -2403,12 +2571,21 @@ number of hypothesis displayed, without hiding the goal" (let ((goal-win (or (get-buffer-window proof-goals-buffer) (get-buffer-window proof-goals-buffer t)))) (if goal-win (with-selected-window goal-win - ;; find snd goal or buffer end + ;; find snd goal or buffer end, if not found this goes to the + ;; end of buffer (search-forward-regexp "subgoal 2\\|\\'") (beginning-of-line) - ;; find something else than a space + ;; find something backward else than a space: bottom of concl (ignore-errors (search-backward-regexp "\\S-")) - (recenter (- 1)) ; put it at bottom og window + (recenter (- 1)) ; put bot of concl at bottom of window + (beginning-of-line) + ;; if the top of concl is hidden we may want to show it instead + ;; of bottom of concl + (when (and coq-prefer-top-of-conclusion + ;; return nil if === is not visible + (not (save-excursion (re-search-backward "========" (window-start) t)))) + (re-search-backward "========" nil t) + (recenter 0)) (beginning-of-line)))))))) (defvar coq-modeline-string2 ")") @@ -2498,14 +2675,18 @@ Only when three-buffer-mode is enabled." (goto-char (point-min)) (recenter)))))))))) +;; TODO: remove/add hook instead? +(defun coq-optimise-resp-windows-if-option () + (when coq-optimise-resp-windows-enable (coq-optimise-resp-windows))) + ;; TODO: I would rather have a response-insert-hook thant this two hooks ;; Careful: coq-optimise-resp-windows must be called BEFORE proof-show-first-goal, ;; i.e. added in hook AFTER it. ;; Adapt when displaying a normal message -(add-hook 'proof-shell-handle-delayed-output-hook 'coq-optimise-resp-windows) +(add-hook 'proof-shell-handle-delayed-output-hook 'coq-optimise-resp-windows-if-option) ;; Adapt when displaying an error or interrupt -(add-hook 'proof-shell-handle-error-or-interrupt-hook 'coq-optimise-resp-windows) +(add-hook 'proof-shell-handle-error-or-interrupt-hook 'coq-optimise-resp-windows-if-option) ;;; DOUBLE HIT ELECTRIC TERMINATOR ;; Trying to have double hit on colon behave like electric terminator. The "." diff --git a/coq/coqtags b/coq/coqtags index 6d874e9d..6d874e9d 100644..100755 --- a/coq/coqtags +++ b/coq/coqtags |