diff options
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-abbrev.el | 61 | ||||
| -rw-r--r-- | coq/coq-compile-common.el | 297 | ||||
| -rw-r--r-- | coq/coq-par-compile.el | 1475 | ||||
| -rw-r--r-- | coq/coq-par-test.el | 953 | ||||
| -rw-r--r-- | coq/coq-seq-compile.el | 54 | ||||
| -rw-r--r-- | coq/coq-syntax.el | 4 | ||||
| -rw-r--r-- | coq/coq-system.el | 47 | ||||
| -rw-r--r-- | coq/coq.el | 2 | ||||
| -rwxr-xr-x[-rw-r--r--] | coq/coqtags | 0 |
9 files changed, 2376 insertions, 517 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 9432bd1b..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"] diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index 8ce4b0c2..92614e7a 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,7 +412,10 @@ 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) @@ -310,7 +459,9 @@ 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 - "\\(?:^From[ \t\n]+\\(?1:[A-Za-z0-9_']+\\(?:\\.[A-Za-z0-9_']+\\)*\\)[ \t\n]*\\)?\\(?2:Require[ \t\n]+\\(?:Import\\|Export\\)?\\)[ \t\n]*" + (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 @@ -319,11 +470,10 @@ 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") @@ -331,11 +481,11 @@ modules are matched separately with `coq-require-id-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. @@ -358,52 +508,62 @@ 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." +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." (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)) + (when 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)) + (when coq--debug-auto-compilation + (message "Ignore %s" lib-obj-file)) t) nil))) -;;; convert .vo files to .v files +;;; 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-obj-file (lib-obj-file) +(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))))) @@ -414,22 +574,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 @@ -442,17 +617,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-par-compile.el b/coq/coq-par-compile.el index aac7447e..efbb2d3c 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-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)) -(defun coq-par-new-compilation-queue () - "Create a new empty queue for `coq-par-compilation-queue'" - (cons nil nil)) -(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.") +;;; job queue -(defun coq-par-enqueue (job) +(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,23 +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") - (when (string-match "\\`.*: " 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)) - (cdr-safe (split-string (substring output (match-end 0)))))))) + (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) @@ -514,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)) @@ -522,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 &optional from) - "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 @@ -546,10 +662,13 @@ 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) @@ -565,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 @@ -589,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 @@ -615,58 +737,73 @@ 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)) + (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 @@ -681,12 +818,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. @@ -696,28 +834,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 @@ -738,6 +896,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) @@ -758,145 +956,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. @@ -909,18 +1313,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) @@ -941,7 +1347,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 @@ -950,50 +1357,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. @@ -1004,32 +1448,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 @@ -1058,20 +1515,21 @@ 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) @@ -1081,44 +1539,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 @@ -1132,56 +1689,85 @@ 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 @@ -1191,29 +1777,35 @@ PROCESS." 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 from)) + (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. @@ -1227,13 +1819,15 @@ 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)) 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) @@ -1248,19 +1842,25 @@ there is no last compilation job." (setq start (match-end 0)) (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) @@ -1282,7 +1882,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 @@ -1300,44 +1900,51 @@ 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)) + (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. @@ -1352,6 +1959,14 @@ 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)))) (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 da85ad9f..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,7 +282,7 @@ 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 &optional from) "Map MODULE-ID to the appropriate coq object file. @@ -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)) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 195636a5..5aa41292 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1304,10 +1304,6 @@ 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) ":")) diff --git a/coq/coq-system.el b/coq/coq-system.el index 8e0f9034..48757be5 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,13 +43,15 @@ 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) @@ -69,14 +72,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." @@ -135,7 +155,14 @@ 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)))))))) (defcustom coq-use-makefile nil "Whether to look for a Makefile to attempt to guess the command line. @@ -270,7 +297,7 @@ request compatibility handling of flags." (list "-R" (expand-file-name dir) alias))) (pcase entry ((and (pred stringp) dir) - (list "-Q" (expand-file-name dir) "\"\"")) + (list "-Q" (expand-file-name dir) "")) (`(ocamlimport ,dir) (list "-I" (expand-file-name dir))) (`(recnoimport ,dir ,alias) @@ -369,8 +396,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" @@ -387,6 +415,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 () @@ -449,7 +478,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))) @@ -1788,7 +1788,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-search-blacklist-string :setting coq-set-search-blacklist) diff --git a/coq/coqtags b/coq/coqtags index 6d874e9d..6d874e9d 100644..100755 --- a/coq/coqtags +++ b/coq/coqtags |