aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar hendriktews <hendrik@askra.de>2016-11-30 22:05:48 +0100
committerGravatar GitHub <noreply@github.com>2016-11-30 22:05:48 +0100
commita6dd1c2622f085233b21bebe1ed4c70dedebb182 (patch)
treeb311cc17e5d794bc43cb8eba100da27d4ac2066f
parentc1e06d2c2d67236aeedb59137d155d93d0646596 (diff)
parent60bf4ce887474116a152045296ff849e4fa00402 (diff)
Merge pull request #125 from hendriktews/quick
support for quick compilation
Diffstat
-rw-r--r--CHANGES27
-rw-r--r--coq/coq-abbrev.el48
-rw-r--r--coq/coq-compile-common.el261
-rw-r--r--coq/coq-par-compile.el821
-rw-r--r--coq/coq-par-test.el953
-rw-r--r--coq/coq-seq-compile.el36
-rw-r--r--coq/coq-system.el4
-rw-r--r--doc/ProofGeneral.texi589
8 files changed, 2167 insertions, 572 deletions
diff --git a/CHANGES b/CHANGES
index 10cf0d25..dca879b3 100644
--- a/CHANGES
+++ b/CHANGES
@@ -12,6 +12,33 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac
- Using query-replace (or replace-string) in the processed region
doesn't wrongly jump to the first match anymore.
+** Coq changes
+
+*** new menu Coq -> Auto Compilation for all background compilation options
+
+*** support for 8.5 quick compilation
+
+ See new menu Coq -> Auto Compilation. Select "no quick" as
+ long as you have not switched to "Proof using" to compile
+ without -quick. Select "quick no vio2vo" to use -quick
+ without vio2vo (and guess what "quick and vio2vo" means ;-),
+ select "ensure vo" to ensure a sound development. See the
+ option `coq-compile-quick' or the subsection "11.3.3 Quick
+ compilation and .vio Files" in the Coq reference manual.
+
+*** bug fixes
+ - avoid leaving partial files behind when compilation fails
+ - 123: Parallel background compliation fails to execute some
+ imports
+ - fix error in process filter: Cannot resize window
+ - 54 partially: Buffer coq-compile-response sometimes takes
+ over the whole window
+ - 75: Library more.v is required
+ - 70: Coq trunk + compile before require => « Invalid version
+ syntax: 'trunk' »
+ - 92: Compile before require from current directory failing
+ with 8.5
+
* Changes of Proof General 4.4 from Proof General 4.3
** ProofGeneral has moved to GitHub!
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index f23ac786..767d2a6e 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -148,6 +148,54 @@ 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.")]
+ ["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'."])
""
["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 32e1ae61..4c24a28b 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,84 @@ 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'.
+
+ 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-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 +275,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 +396,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)
@@ -321,11 +454,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")
@@ -333,11 +465,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.
@@ -360,45 +492,52 @@ 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
+ (if coq--debug-auto-compilation
(message "Ignore lib file %s" lib-obj-file))
t)
(if (some
(lambda (dir-regexp) (string-match dir-regexp lib-obj-file))
coq-compile-ignored-directories)
(progn
- (if coq-debug-auto-compilation
+ (if 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-library-src-of-obj-file (lib-obj-file)
+(defun coq-module-of-src-file (src-file)
+ "Return the module name for SRC-FILE.
+SRC-FILE must be a .v file."
+ (let ((file (file-name-nondirectory src-file)))
+ (substring file 0 (max 0 (- (length file) 2)))))
+
+(defun coq-library-src-of-vo-file (lib-obj-file)
"Return source file name for LIB-OBJ-FILE.
Chops off the last character of LIB-OBJ-FILE to convert \"x.vo\" to \"x.v\"."
(substring lib-obj-file 0 (- (length lib-obj-file) 1)))
+(defun coq-library-vio-of-vo-file (vo-obj-file)
+ "Return .vio file name for VO-OBJ-FILE.
+Changes the suffix from .vio to .vo. VO-OBJ-FILE must have a .vo suffix."
+ (concat (coq-library-src-of-vo-file vo-obj-file) "io"))
+
;;; ancestor unlocking
;;; (locking is different for sequential and parallel compilation)
@@ -416,22 +555,34 @@ 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
+;;; manage coq--compile-response-buffer
-(defun coq-init-compile-response-buffer (command)
+(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 coq--compile-response-buffer)
+ (coq-init-compile-response-buffer))
+ (let ((inhibit-read-only t))
+ (with-current-buffer coq--compile-response-buffer
+ (insert command "\n" error-message)))
+ (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
@@ -444,21 +595,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)))
+ (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 19859195..6dbfb109 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:
;;
@@ -101,7 +102,7 @@
;;
;; 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
+;; 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.
@@ -110,7 +111,7 @@
;; 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
+;; 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.
@@ -122,16 +123,42 @@
;; signalling an error and calling `coq-par-emergency-cleanup' in the
;; sentinel, if there was an error.
;;
+;; 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
;;
;; '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
@@ -163,6 +190,8 @@
;; 'require-span - present 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.
;; 'visited - used in the dependency cycle detection to mark
;; visited jobs
;;
@@ -178,9 +207,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
@@ -214,7 +244,7 @@
;; the process is killed
;;
;;
-;; Symbols in the coq-par-ancestor-files hash
+;; 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.
@@ -239,7 +269,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)
@@ -253,7 +283,7 @@
;;; Variables
-(defvar coq-par-ancestor-files nil
+(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.
@@ -269,22 +299,29 @@ asserted region.
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--par-next-id 1
"Increased for every job and process, to get unique job names.
The names are only used for debugging.")
@@ -326,48 +363,84 @@ 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))
+ "(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))
+ (puthash locked-anc 'asserted coq--par-ancestor-files))
proof-included-files-list))
+;;; generic queues
+;; Standard implementation with two lists.
-;;; job queue
+(defun coq-par-new-queue ()
+ "Create a new empty queue."
+ (cons nil nil))
+
+(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
+
+(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-enqueue (job)
+(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
+ (coq-par-enqueue coq-par-compilation-queue job)
+ (if 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
+ (let ((res (coq-par-dequeue coq-par-compilation-queue)))
+ (if 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)
+ (if 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)))
+ (if coq--debug-auto-compilation
+ (if res
+ (message "%s: vio2vo dequeue" (get res 'name))
+ (message "vio2vo queue empty")))
+ res))
+
+
;;; error symbols
;; coq-compile-error-coqdep
@@ -410,6 +483,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
@@ -442,13 +530,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)))
@@ -466,7 +554,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."
@@ -477,21 +565,27 @@ load-path options to coqdep."
"Analyse output OUTPUT of coqdep command COMMAND with exit status STATUS.
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."
- (if coq-debug-auto-compilation
+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."
+ (if 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")
;; 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))
@@ -520,7 +614,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))
@@ -528,10 +625,10 @@ break."
(cons command-intro this-command)
this-command))
coqdep-status coqdep-output)
- (if coq-debug-auto-compilation
+ (if coq--debug-auto-compilation
(message "Run synchronously: %s"
(mapconcat 'identity full-command " ")))
- ;; (if coq-debug-auto-compilation
+ ;; (if coq--debug-auto-compilation
;; (message "CPGLD: call coqdep arg list: %s" coqdep-arguments))
(with-temp-buffer
(setq coqdep-status
@@ -539,13 +636,13 @@ break."
coq-dependency-analyzer nil (current-buffer) nil
coqdep-arguments))
(setq coqdep-output (buffer-string)))
- ;; (if coq-debug-auto-compilation
+ ;; (if 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
@@ -555,6 +652,9 @@ 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
@@ -576,7 +676,7 @@ function returns () if MODULE-ID comes from the standard library."
coq-load-path
(concat "echo \"" coq-string "\" > " temp-require-file ";"))))
(delete-file temp-require-file))
- (if coq-debug-auto-compilation
+ (if 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
@@ -607,7 +707,7 @@ function returns () if MODULE-ID comes from the standard library."
;;; 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."
;; 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
@@ -626,32 +726,38 @@ 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)))
(defun coq-par-unlock-ancestors-on-error ()
"Unlock ancestors which are not in an asserted span.
Used for unlocking ancestors on compilation errors."
- (when coq-par-ancestor-files
+ (when coq--par-ancestor-files
;; nil e.g. when enabling on-the-fly compilation after processing imports.
(maphash
(lambda (ancestor state)
(when (eq state 'locked)
(coq-unlock-ancestor ancestor)
- (puthash ancestor nil coq-par-ancestor-files)))
- coq-par-ancestor-files)))
+ (puthash ancestor nil coq--par-ancestor-files)))
+ coq--par-ancestor-files)))
(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."
+ (when coq--debug-auto-compilation
+ (message "emergency cleanup"))
(coq-par-kill-all-processes)
- (setq coq-par-compilation-queue (coq-par-new-compilation-queue))
- (setq coq-last-compilation-job nil)
+ (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))
(when proof-action-list
(setq proof-shell-interrupt-pending t))
(coq-par-unlock-ancestors-on-error)
@@ -672,13 +778,14 @@ compilation job JOB, making sure that CONTINUATION runs when the
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"
+ (if coq--debug-auto-compilation
+ (message "%s %s: start %s %s in %s"
(get job 'name) process-name
- command (mapconcat 'identity arguments " ")))
+ 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
@@ -693,8 +800,8 @@ file to be deleted when the process is killed."
(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))
@@ -710,7 +817,7 @@ errors are reported with an error message."
(condition-case err
(if (process-get process 'coq-par-process-killed)
(progn
- (if coq-debug-auto-compilation
+ (if coq--debug-auto-compilation
(message "%s %s: skip sentinel, process killed, %s"
(get (process-get process 'coq-compilation-job) 'name)
(process-name process)
@@ -720,9 +827,16 @@ errors are reported with an error message."
"no file removal")))
(if (process-get process 'coq-process-rm)
(ignore-errors
- (delete-file (process-get process 'coq-process-rm)))))
+ (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)
- (if coq-debug-auto-compilation
+ (if coq--debug-auto-compilation
(message "%s %s: process status changed to %s"
(get (process-get process 'coq-compilation-job) 'name)
(process-name process)
@@ -731,14 +845,18 @@ errors are reported with an error message."
((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)
+ (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
@@ -759,6 +877,31 @@ 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 (span)
+ "Callback for `proof-action-list' to start vio2vo compilation.
+This callback is inserted with a dummy item after the last
+require command to start vio2vo compilation after
+`coq-compile-vio2vo-delay' seconds."
+ (assert (not coq--last-compilation-job)
+ nil "normal compilation and vio2vo in parallel 1")
+ (setq coq--compile-vio2vo-delay-timer
+ (run-at-time coq-compile-vio2vo-delay nil 'coq-par-run-vio2vo-queue)))
+
+
;;; background job tasks
(defun coq-par-job-coqc-finished (job)
@@ -779,7 +922,7 @@ 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
+ (if coq--debug-auto-compilation
(message "%s -> %s: add coqc dependency"
(get dependee 'name) (get dependant 'name))))
@@ -790,52 +933,177 @@ errors are reported with an error message."
nil "queue dependency cannot be added")
(put dependant 'queue-dependant-waiting t)
(put dependee 'queue-dependant dependant)
- (if coq-debug-auto-compilation
+ (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))))
-
(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-kickoff-queue-maybe (job)
"Try transition 'waiting-queue -> 'ready for job JOB.
@@ -843,79 +1111,103 @@ 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
+ are registered in `coq--par-ancestor-files' and in the span in
'queue-span
- processing of items in 'queueitems is started
- 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
+ job (`coq--last-compilation-job') then the last compilation job
and `proof-second-action-list-active' are cleared."
(if (or (not (eq (get job 'state) 'waiting-queue))
(get job 'queue-dependant-waiting))
- (if coq-debug-auto-compilation
+ (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
+ (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)
+ (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))
+ (let ((items (get job 'queueitems)))
+ (when (and (eq coq--last-compilation-job job)
+ (eq coq-compile-quick 'quick-and-vio2vo))
+ ;; Insert the vio2vo start notification callback after the
+ ;; require item.
+ (setq items
+ (cons
+ (car items)
+ (cons
+ ;; A proof-action-list item is
+ ;; (SPAN COMMANDS ACTION [DISPLAYFLAGS])
+ ;; If COMMANDS is nil, the item is processed as
+ ;; comment and not sent to the proof assistant, see
+ ;; proof-shell.el.
+ (list nil nil 'coq-par-require-processed)
+ (cdr items)))))
+ (proof-add-to-queue items 'advancing)
+ (if coq--debug-auto-compilation
+ (message "%s: add %s items to action list"
+ (get job 'name) (length items)))
+ (put job 'queueitems nil)))
(put job 'state 'ready)
- (if coq-debug-auto-compilation
+ (if 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))
- nil "coq-last-compilation-job invariant error")
+ (assert (not (eq coq--last-compilation-job job))
+ nil "coq--last-compilation-job invariant error")
(put dependant 'queue-dependant-waiting nil)
- (if coq-debug-auto-compilation
+ (if 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
+ (if 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)
+ (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
+ (if coq--debug-auto-compilation
(message "clear last compilation job"))
(message "Library compilation finished"))
- (if coq-debug-auto-compilation
+ (if coq--debug-auto-compilation
(message "%s: no queue dependant, queue kickoff finished"
(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)
+ ;; 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 puts job into the vio2vo queue, if necessary.
(if (coq-par-job-needs-compilation job)
(coq-par-start-or-enqueue job)
- (if coq-debug-auto-compilation
+ (if coq--debug-auto-compilation
(message "%s: up-to-date, no compilation" (get job 'name)))
+ (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
@@ -943,7 +1235,7 @@ For 'file jobs this is 'waiting-dep -> 'enqueued-coqc and for
(1- (get dependant 'coqc-dependency-count)))
(assert (<= 0 (get dependant 'coqc-dependency-count))
nil "dependency count below zero")
- (if coq-debug-auto-compilation
+ (if 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)
@@ -985,9 +1277,9 @@ This function makes the following actions.
;; 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)))
+ (setq dep-time (get job 'obj-mod-time)))
(put job 'youngest-coqc-dependency dep-time)
- (if coq-debug-auto-compilation
+ (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)
@@ -998,7 +1290,7 @@ This function makes the following actions.
(lambda (dependant)
(coq-par-decrease-coqc-dependency dependant dep-time ancestor-files))
(get job 'coqc-dependants))
- (if coq-debug-auto-compilation
+ (if coq--debug-auto-compilation
(message "%s: coqc kickoff finished, maybe kickoff queue"
(get job 'name)))
(coq-par-kickoff-queue-maybe job)))
@@ -1007,13 +1299,13 @@ This function makes the following actions.
"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'"
+`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)))
+ (unless (gethash true-src coq--par-ancestor-files)
+ (puthash true-src 'locked coq--par-ancestor-files)))
(coq-par-start-process
coq-dependency-analyzer
(coq-par-coqdep-arguments (get job 'src-file) (get job 'load-path))
@@ -1021,6 +1313,24 @@ locked, registered in the 'ancestor-files property of JOB and in
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-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.
JOB was at the head of the compilation queue and now either
@@ -1030,33 +1340,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
- (get job 'obj-file))))))
+ (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
@@ -1085,20 +1407,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
+ (if coq--debug-auto-compilation
(message "%s: create %s compilation job for %s"
- (get new-job 'name) (get new-job 'type) module-obj-file))
+ (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)
@@ -1112,10 +1435,10 @@ This function returns the newly created job."
(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
@@ -1123,10 +1446,10 @@ This function returns the newly created job."
(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
+ (puthash module-vo-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))
+ (get new-job 'name) (get new-job 'type) module-vo-file))
(when queue-dep
(coq-par-add-queue-dependency queue-dep new-job))
(coq-par-start-or-enqueue new-job))
@@ -1162,15 +1485,15 @@ is directly passed to `coq-par-analyse-coq-dep-exit'."
(signal 'coq-compile-error-coqdep (get job 'src-file))
;; no coqdep error -- work on dependencies
- (if coq-debug-auto-compilation
+ (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)
(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
+ (lambda (dep-vo-file)
+ (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)))
@@ -1183,33 +1506,52 @@ is directly passed to `coq-par-analyse-coq-dep-exit'."
(put job 'youngest-coqc-dependency job-max-time)
(if (coq-par-dependencies-ready job)
(progn
- (if coq-debug-auto-compilation
+ (if coq--debug-auto-compilation
(message "%s: coqc dependencies finished" (get job 'name)))
(coq-par-compile-job-maybe job))
- (if coq-debug-auto-compilation
+ (if 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.
+ "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)
+ (let ((job (process-get process 'coq-compilation-job)))
+ ;; coqc success
+ (when (get job 'vio2vo-needed)
+ (coq-par-vio2vo-enqueue job))
+ (coq-par-kickoff-coqc-dependants 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)
+ (coq-compile-display-error
+ (mapconcat 'identity (process-get process 'coq-process-command) " ")
+ (process-get process 'coq-process-output)
+ t)
(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
@@ -1218,36 +1560,36 @@ 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."
- (if coq-debug-auto-compilation
+ (if 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-obj-file
- (coq-par-map-module-id-to-obj-file module-id coq-load-path from))
+ (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
- (if module-obj-file
+ (if coq--debug-auto-compilation
+ (if module-vo-file
(message "check compilation for module %s from object file %s"
- module-id module-obj-file)
+ module-id module-vo-file)
(message "nothing to check for module %s" module-id)))
- ;; coq-par-map-module-id-to-obj-file currently returns () for
+ ;; 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
+ (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))))))
+ (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.
@@ -1261,14 +1603,14 @@ 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)
- (if coq-debug-auto-compilation
+ (if 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.
@@ -1284,22 +1626,22 @@ 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))
+ (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)
+ (put coq--last-compilation-job 'queueitems
+ (nconc (get coq--last-compilation-job 'queueitems)
require-items))
- (if coq-debug-auto-compilation
+ (if coq--debug-auto-compilation
(message "%s: attach %s items (containing now %s items)"
- (get coq-last-compilation-job 'name)
+ (get coq--last-compilation-job 'name)
(length require-items)
- (length (get coq-last-compilation-job 'queueitems)))))
+ (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
+ (if coq--debug-auto-compilation
(message "attach %s items to queueitems (containing now %s items)"
(length require-items)
(length queueitems))))))
@@ -1324,7 +1666,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
@@ -1342,42 +1684,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-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
+ (if 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
+ (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
+ (if coq--debug-auto-compilation
+ (if coq--last-compilation-job
(message "return control, waiting for background jobs")
(message "return control, no background jobs")))))
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..062ef4e1 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,7 +77,7 @@ 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
+ (if coq--debug-auto-compilation
(message "call coqdep arg list: %S" coqdep-arguments))
(with-temp-buffer
(setq coqdep-status
@@ -85,7 +85,7 @@ break."
coq-dependency-analyzer nil (current-buffer) nil
coqdep-arguments))
(setq coqdep-output (buffer-string)))
- (if coq-debug-auto-compilation
+ (if coq--debug-auto-compilation
(message "coqdep status %s, output on %s: %s"
coqdep-status lib-src-file coqdep-output))
(if (or
@@ -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,15 +118,15 @@ 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
+ (if 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
+ 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
+ (with-current-buffer coq--compile-response-buffer
(buffer-string))))
(unless (eq coqc-status 0)
(coq-display-compile-response-buffer)
@@ -178,7 +178,7 @@ OBJ have identical modification times."
(progn
(coq-seq-compile-library src)
'just-compiled)
- (if coq-debug-auto-compilation
+ (if coq--debug-auto-compilation
(message "Skip compilation of %s" src))
obj-time))))
@@ -202,7 +202,7 @@ function."
(let ((result (gethash lib-obj-file coq-obj-hash)))
(if result
(progn
- (if coq-debug-auto-compilation
+ (if coq--debug-auto-compilation
(message "Checked %s already" lib-obj-file))
result)
;; lib-obj-file has not been checked -- do it now
@@ -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-system.el b/coq/coq-system.el
index 997e93d2..2b8c9214 100644
--- a/coq/coq-system.el
+++ b/coq/coq-system.el
@@ -393,8 +393,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"
@@ -411,6 +412,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 ()
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 0ef98d7e..748cf3ac 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -4340,39 +4340,42 @@ Inserts ``End <section-name>.'' (this should work well with nested sections).
@node Using the Coq project file
@section Using the Coq project file
-Before starting the Coq process, one need to set @code{coqtop} options,
-in particular the -I and -R command that set the directories to have in
-the coq load path. You can use file variables (@ref{Using file
-variables}) as it was recommended on previous versions of ProofGeneral
-but there is now a better way. ProofGeneral knows how to extract this
-information from the Coq project file if there is one. The Coq project
-file must be named following variable `coq-project-filename' (default:
-@code{_CoqProject}) and be on the root directory of your development.
-
-It should contain something like:
+The Coq project file is the recommended way to configure the Coq
+load path and the mapping of logical module names to physical
+file path'. The project file is typically named
+@code{_CoqProject} and must be located at the directory root of
+your Coq project. Proof General searches for the Coq project file
+starting at the current directory and walking the directory
+structure upwards. The Coq project file contains the common
+options (especially @code{-R}) and a list of the files of the
+project, see the Coq reference manual, Section 15.3, ``Creating a
+Makefile for Coq modules''.
+
+The Coq project file should contain something like:
@verbatim
-R foo bar
-I foo2
-arg -foo3
+file.v
+bar/other_file.v
+...
@end verbatim
-The intial use of this file is to be given to the @code{coq_makefile}
-tool to generate a Makefile (see Coq documentation for details). It is
-parsed by ProofGeneral to guess the command line option. In this example
-the command line built by Proofgeneral will be @code{coqtop -foo3 -R foo
-bar -I foo2}.
+Proof General only extracts the common options from the Coq
+project file and uses them for @code{coqtop} background
+processes as well as for @code{coqdep} and @code{coqc} when you use
+the auto compilation feature, @ref{Automatic Compilation in
+Detail}. For the example above, Proof General will start
+@code{coqtop -foo3 -R foo bar -I foo2}.
@emph{Remarque:} @code{-arg} must be followed by one and only one option
to pass to coqtop/coqc, use several @code{-arg} to issue several
-options. One per line (limitation of proofgeneral).
-
-This is the recommended way of configuring coqtop options for coq
-compilation, CoqIde and Proofgeneral. Its main advantage is that it
-avoids duplicating informations between these three tools.
+options. One per line (limitation of Proof General).
-For specific (and rare) per file configuration one can still use file
-variables (@ref{Using file variables}).
+For backward compatibility, one can also configure the load path
+with the option @code{coq-load-path}, but this is not compatible
+with @code{CoqIde} or @code{coq_makefile}.
@menu
* Changing the name of the coq project file::
@@ -4382,44 +4385,60 @@ variables (@ref{Using file variables}).
@node Changing the name of the coq project file
@subsection Changing the name of the coq project file
-One can change the name of the project file by:
-
-(setq coq-project-filename "myprojectfile")
+To change the name of the Coq project file, configure
+@code{coq-project-filename} (select menu @code{Proof-General ->
+Advanced -> Customize -> Coq} and scroll down to ``Coq Project
+Filename''). Customizing @code{coq-project-filename} this way
+will change the Coq project file name permanently and globally.
-or:
-
-(setq (make-local-variable 'coq-project-filename) "myprojectfile")
-
-If this is for a project, the best is probably to have a .dir-locals.el
-at the root of the project, as explained in @ref{Using file
-variables}. This file should contain something like:
+If you only want to change the name of the Coq project file for
+one project you can set the option as local file variable,
+@ref{Using file variables}. This can be done either directly in
+every file or once for all files of a directory tree with a
+@code{.dir-local.el} file, @inforef{Directory Variables, ,emacs}.
+For this case, this file should contain
@lisp
((coq-mode . ((coq-project-filename . "myprojectfile"))))
@end lisp
-or equivalently:
+Documentation of the user option @code{coq-project-filename}:
+
+@c TEXI DOCSTRING MAGIC: coq-project-filename
+@defvar coq-project-filename
+The name of coq project file.@*
+The coq project file of a coq developpement (Cf Coq documentation
+on "makefile generation") should contain the arguments given to
+coq_makefile. In particular it contains the -I and -R
+options (preferably one per line). If @samp{coq-use-coqproject} is
+t (default) the content of this file will be used by proofgeneral
+to infer the @samp{@code{coq-load-path}} and the @samp{@code{coq-prog-args}} variables
+that set the coqtop invocation by proofgeneral. This is now the
+recommended way of configuring the coqtop invocation. Local file
+variables may still be used to override the coq project file's
+configuration. .dir-locals.el files also work and override
+project file settings.
+@end defvar
-@lisp
-((coq-mode
- .
- ((eval
- .
- (progn
- (make-local-variable 'coq-project-filename)
- (setq coq-project-filename "myprojectfile"))))))
-@end lisp
@node Disabling the coq project file mechanism
@subsection Disabling the coq project file mechanism
-If the variable `coq-use-project-file' is nil, then Proofgeneral will
-not look at project file. therefore you can put this in your config file
-(.emacs) to disable the use of project file:
-
-@lisp
-(setq coq-use-project-file nil)
-@end lisp
+To disable the Coq project file feature in Proof General, set
+@code{coq-use-project-file} to nil (select menu
+@code{Proof-General -> Advanced -> Customize -> Coq} and scroll
+down to ``Coq Use Project File'').
+
+@c TEXI DOCSTRING MAGIC: coq-use-project-file
+@defvar coq-use-project-file
+If t, when opening a coq file read the dominating _CoqProject.@*
+If t, when a coq file is opened, Proof General will look for a
+project file (see @samp{@code{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 @samp{@code{coq-load-path}}).
+@end defvar
You can also use the .dir-locals.el as above to configure this setting
on a per project basis.
@@ -4457,15 +4476,17 @@ There are actually two implementations of the Recompilation
feature.
@table @asis
-@item Synchronous single threaded compilation (stable)
-With synchronous compilation, coqdep and coqc are called
-synchronously for each Require command. Proof General is locked
-until the compilation finishes
-@item Parallel asynchronous compilation (experimental)
+@item Parallel asynchronous compilation (stable, default)
With parallel compilation, coqdep and coqc are launched in the
background and Proof General stays responsive during compilation.
Up to `coq-max-background-compilation-jobs' coqdep and coqc
-processes may run in parallel.
+processes may run in parallel. Coq 8.5 quick compilation is
+supported with various modes, @ref{Quick compilation and .vio Files}.
+@item Synchronous single threaded compilation (obsolete)
+With synchronous compilation, coqdep and coqc are called
+synchronously for each Require command. Proof General is locked
+until the compilation finishes. Coq 8.5 quick compilation is not
+supported with synchronously compilation.
@end table
To enable the automatic compilation feature, you have to follow
@@ -4474,30 +4495,15 @@ these points:
@itemize @bullet
@item
The option @code{coq-compile-before-require} must be
-turned on (menu @code{Coq -> Settings -> Compile Before Require}).
+turned on (menu @code{Coq -> Auto Compilation -> Compile Before Require}).
@item
-Nonstandard load path elements @emph{must} be configured in the
-option @code{coq-load-path}. @code{-I} options in
+Nonstandard load path elements @emph{must} be configured via a
+Coq project file (this is the recommended option),
+@ref{Using the Coq project file} or via
+option @code{coq-load-path}. @code{-I} or @code{-R} options in
@code{coq-prog-name} or @code{coq-prog-args} must be deleted.
@item
-In @code{coq-load-path} use strings @code{"dir"} for @code{-I}
-options and lists of two strings @code{("dir" "path")} for
-@code{-R "dir" -as "path"} (for more details see the
-documentation of `coq-load-path' or @ref{Customizing Coq Multiple
-File Support}).
-@item
-For a nonstandard compilation procedure and limited ML module
-support, @code{coq-compile-command} can be set to an external
-compilation command. For standard dependency analysis with
-@code{coqdep} and compilation with @code{coqc} the option
-@code{coq-compile-command} can be left empty. In this case Proof
-General calls @code{coqdep} and @code{coqc} as needed.
-@item
-The default compilation method is synchronous compilation. In
-order to experience parallel background compilation on all your
-CPU cores,
-enable `coq-compile-parallel-in-background' (menu @code{Coq ->
-Settings -> Compile Parallel In Background}). Configure
+Configure
@code{coq-max-background-compilation-jobs} if you want to limit
the number of parallel background jobs.
@end itemize
@@ -4507,6 +4513,7 @@ the number of parallel background jobs.
@menu
* Automatic Compilation in Detail::
* Locking Ancestors::
+* Quick compilation and .vio Files::
* Customizing Coq Multiple File Support::
* Current Limitations::
@end menu
@@ -4528,51 +4535,24 @@ compilation finished.
Proof General uses @code{coqdep} in order to translate the
qualified identifiers in @code{Require} commands to coq library
-file names. Therefore, in Coq version prior to @code{8.3pl2},
-@code{Require Arith} works, while
-@code{Require Arith.Le} gives an error. The use of @code{coqdep}
-is also the reason
-why nonstandard load path elements must be configured in
-@code{coq-load-path}.
-
-Once the library file name has been determined, its dependencies
-must be checked and out-of-date files must be compiled. This can
-either be done internally, by Proof General itself, or by an
-external command. If @code{coq-compile-command} is the empty
-string, Proof General does dependency checking and compilation
-itself. Otherwise the command in @code{coq-compile-command} is
-started as an external process after substituting certain keys,
-@ref{Customizing Coq Multiple File Support}.
-
-For an external compilation command Proof General uses the
-general compilation facilities of Emacs
-(@inforef{Compilation,,emacs}) with its own customization variables.
-The compilation command must be customized in
-@code{coq-compile-command} and the flag
-@code{coq-confirm-external-compilation} (menu @code{Coq ->
-Settings -> Confirm External Compilation})
-determines
-whether the user must confirm the compilation command. The output
-of the compilation appears then in the @code{*compilation*}
-buffer.
-
-When Proof General compiles itself, output is only shown in case
+file names and to determine library dependencies. Because Proof
+General cannot know whether files are updated outside of Emacs,
+it checks for every @code{Require} command the complete
+dependency tree and recompiles files as necessary.
+
+Output from the compilation is only shown in case
of errors. It then appears in the buffer
-@code{*coq-compile-response*}. With internal as well as with external
-compilation
-one can use @code{C-x `} (bound to @code{next-error},
+@code{*coq-compile-response*}.
+One can use @code{C-x `} (bound to @code{next-error},
@inforef{Compilation Mode,,emacs}) to jump to error locations.
-Note however, that @code{coqdep} does not produce error messages
-with location information, so @code{C-x `} cannot work for errors
-from @code{coqdep}.
-
-Proof General cannot know if some library files have been updated
-outside of Proof General, therefore, it must perform the
-dependency checking for each @code{Require} command. If the
-continuous confirmation of the external compilation commands
-becomes tedious, disable
-@code{coq-confirm-external-compilation} (see menu @code{Coq ->
-Settings}).
+Sometimes the compilation commands do not produce error messages
+with location information, then @code{C-x `} does only work in a
+limited way.
+
+For Coq version 8.5 or newer, the option @code{coq-compile-quick}
+controls how @code{-quick} and @code{.vio} files are used,
+@ref{Quick compilation and .vio Files}. This can also be
+configured in the menu @code{Coq -> Auto Compilation}.
When a @code{Require} command causes a compilation of some files
one may wish to save some buffers to disk beforehand. The option
@@ -4587,13 +4567,18 @@ between two implementations of internal compilation.
@table @asis
@item Synchronous single threaded compilation
-This is the stable version supported since Proof General version
+This is the old, now outdated version supported since Proof General
4.1. This method starts coqdep and coqc processes one after each
other in synchronous subprocesses. Your Emacs session will be
locked until compilation finishes. Use @code{C-g} to interrupt
-compilation.
+compilation. This method supports compilation via an external
+command (such as @code{make}), see option
+@code{coq-compile-command} in @ref{Customizing Coq Multiple File
+Support} below. Synchronous compilation does not support the
+quick compilation of Coq 8.5.
+
@item Parallel asynchronous compilation
-This is the new version added in Proof General version 4.3. It
+This is the newer and default version added in Proof General version 4.3. It
runs up to @code{coq-max-background-compilation-jobs} coqdep and
coqc jobs in parallel in asynchronous subprocesses (or uses all
your CPU cores if @code{coq-max-background-compilation-jobs}
@@ -4610,6 +4595,14 @@ before the first Require, then you may see Proof General and Coq
running in addition to `coq-max-background-compilation-jobs'
compilation jobs.
+Depending on the setting of @code{coq-compile-quick} (which can
+also be set via menu @code{Coq -> Auto Compilation}) Proof
+General produces @code{.vio} or @code{.vo} files and deletes
+outdated @code{.vio} or @code{.vo} files to ensure Coq does not
+load outdated files. When @code{quick-and-vio2vo} is selected a
+vio2vo compilation starts when the @code{Require} command had
+been processed, @ref{Quick compilation and .vio Files}.
+
Actually, even with this method, not everything runs
asynchronously. To translate module identifiers from the Coq
sources into file names, Proof General runs coqdep on an
@@ -4658,6 +4651,109 @@ benefit, as Require commands are usually on the top of each
file.]
+@node Quick compilation and .vio Files
+@subsection Quick compilation and .vio Files
+
+Proof General supports quick compilation only with the parallel
+asynchronous compilation. There are 4 modes that can be
+configured with @code{coq-compile-quick} or by selecting one of
+the radio buttons in the @code{Coq -> Auto Compilation} menu.
+
+Use the default @code{no-quick}, if you have not yet switched to
+@code{Proof using}. Use @code{quick-no-vio2vo}, if you want quick
+recompilation without producing .vo files. Option
+@code{quick-and-vio2vo} recompiles with @code{-quick} as
+@code{quick-no-vio2vo} does, but schedules a vio2vo compilation
+for missing @code{.vo} files after a certain delay. Finally, use
+@code{ensure-vo} for only importing @code{.vo} files with
+complete universe checks.
+
+Note that with all of @code{no-quick}, @code{quick-no-vio2vo} and
+@code{quick-and-vio2vo} your development might be unsound because
+universe constraints are not fully present in @code{.vio} files.
+
+There are a few peculiarities of quick compilation in Coq 8.5
+that one should be aware of.
+
+@itemize
+@item
+Quick compilation runs noticeably slower when section
+variables are not declared via @code{Proof using}.
+@item
+Even when section variables are declared, quick compilation runs
+slower on very small files, probably because of the
+comparatively big size of the @code{.vio} files. You can speed up
+quick compilation noticeably by running on a RAM disk.
+@item
+If both, the @code{.vo} and the @code{.vio} files are present,
+Coq load the more recent one, regardless of whether
+@code{-quick}, and emits a warning when the @code{.vio} is more
+recent than the @code{.vo}.
+@item
+Under some circumstances, files compiled when only the
+@code{.vio} file of some library was present are not compatible
+with (other) files compiled when also the @code{.vo} file of that
+library was present, see Coq issue #5223 for details. As a rule
+of thumb one should run vio2vo compilation only before or after
+library loading.
+@item
+Apart from the previous point, Coq works fine when libraries are
+present as a mixture of @code{.vio} and @code{.vo} files. While
+@code{make} insists on building all prerequisites as either
+@code{.vio} or @code{.vo} files, Proof General just checks
+whether an up-to-date compiled library file is present.
+@item
+To ensure soundness, all library dependencies must be compiled as
+@code{.vo} files and loaded into one Coq instance.
+@end itemize
+
+Detailed description of the 4 modes:
+
+@table @code
+@item no-quick
+Compile outdated prerequisites without @code{-quick}, producing @code{.vo}
+files, but don't compile prerequisites for which an up-to-date
+@code{.vio} file exists. Delete or overwrite outdated @code{.vo} files.
+
+@item quick-no-vio2vo
+Compile outdated prerequisites with @code{-quick}, producing @code{.vio}
+files, but don't compile prerequisites for which an up-to-date
+@code{.vo} file exists. Delete or overwrite outdated @code{.vio} files.
+
+@item quick-and-vio2vo
+Same as @code{quick-no-vio2vo}, but start vio2vo processes for
+missing @code{.vo} files after a certain delay when library
+complication for the current queue region has finished. 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 controlled
+by option @code{coq-compile-vio2vo-percentage}, @ref{Customizing
+Coq Multiple File Support}.
+
+@emph{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. To mitigate this risk, vio2vo compilation
+only starts after a certain delay after the last require command
+of the current queue region has been processed. This is
+controlled by @code{coq-compile-vio2vo-delay}, @ref{Customizing
+Coq Multiple File Support}.
+
+@item ensure-vo
+Ensure that all library dependencies are present as @code{.vo}
+files and delete outdated @code{.vio} files or @code{.vio} files
+that are more recent than the corresponding @code{.vo} file. This
+setting is the only one that ensures soundness.
+@end table
+
+The options @code{no-quick} and @code{ensure-vo} are compatible
+with Coq 8.4 or older. When Proof General detects such an older
+Coq version, it changes the quick compilation mode automatically.
+For this to work, the option @code{coq-compile-quick} must only
+be set via the customization system or via the menu.
+
+
+
@node Customizing Coq Multiple File Support
@subsection Customizing Coq Multiple File Support
@@ -4677,7 +4773,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
-@samp{Coq -> Settings -> Compile Before Require}.
+@samp{Coq -> Auto Compilation -> Compile Before Require}.
@end defvar
@@ -4697,8 +4793,7 @@ confirmation.
@end defvar
-The following two options are for the parallel compilation
-method.
+The following options configure parallel compilation.
@c TEXI DOCSTRING MAGIC: coq-compile-parallel-in-background
@defvar coq-compile-parallel-in-background
@@ -4713,9 +4808,14 @@ the background. The maximal number of parallel compilation jobs
is set with @samp{@code{coq-max-background-compilation-jobs}}.
This option can be set/reset via menu
-@samp{Coq -> Settings -> Compile Parallel In Background}.
+@samp{Coq -> Auto Compilation -> Compile Parallel In Background}.
@end defvar
+
+The option @code{coq-compile-quick} is described in detail above,
+@ref{Quick compilation and .vio Files}
+
+
@c TEXI DOCSTRING MAGIC: coq-max-background-compilation-jobs
@defvar coq-max-background-compilation-jobs
Maximal number of parallel jobs, if parallel compilation is enabled.@*
@@ -4728,68 +4828,38 @@ is not adapted.
@end defvar
-The following two options deal with the load path. Proof General
-divides the load path into the standard load path (which is
-hardwired in the tools and need not be set explicitly), the
-nonstandard load path (which must always be set explicitly), and
-the current directory (which must be set explicitly for
-@code{coqdep}). The option @code{coq-load-path} determines the
-nonstandard load path and @code{coq-load-path-include-current}
-determines whether the current directory is put into the load
-path of @code{coqdep}.
-
-@c TEXI DOCSTRING MAGIC: coq-load-path
-@defvar coq-load-path
-Non-standard coq library load path.@*
-This list specifies the LoadPath extension for coqdep, coqc and
-coqtop. Usually, the elements of this list are strings (for
-"-I") or lists of two strings (for "-R" dir path and
-"-Q" dir path).
-
-The possible forms of elements of this list correspond to the 4
-forms of include options (@samp{-I} @samp{-Q} and @samp{-R}). An element can be
-@lisp
- - A list of the form @samp{(}ocamlimport dir)', specifying (in 8.5) a
- directory to be added to ocaml path (@samp{-I}).
- - A list of the form @samp{(}rec dir path)' (where dir and path are
- strings) specifying a directory to be recursively mapped to the
- logical path @samp{path} (@samp{-R dir path}).
- - A list of the form @samp{(}recnoimport dir path)' (where dir and
- path are strings) specifying a directory to be recursively
- mapped to the logical path @samp{path} (@samp{-Q dir path}), but not
- imported (modules accessible for import with qualified names
- only). Note that -Q dir "" has a special, nonrecursive meaning.
- - A list of the form (8.4 only) @samp{(}nonrec dir path)', specifying a
- directory to be mapped to the logical path @code{'path'} ('-I dir -as path').
-@end lisp
-For convenience the symbol @samp{rec} can be omitted and entries of
-the form @samp{(dir path)} are interpreted as @samp{(rec dir path)}.
-
-A plain string maps to -Q ... "" in 8.5, and -I ... in 8.4.
+@c TEXI DOCSTRING MAGIC: coq-max-background-vio2vo-percentage
+@defvar coq-max-background-vio2vo-percentage
+Percentage of @samp{@code{coq-max-background-vio2vo-percentage}} for vio2vo jobs.@*
+This setting configures the maximal number of vio2vo background
+jobs (if you set @samp{@code{coq-compile-quick}} to @code{'quick-and-vio2vo}) as
+percentage of @samp{@code{coq-max-background-compilation-jobs}}.
+@end defvar
-Under normal circumstances this list does not need to
-contain the coq standard library or "." for the current
-directory (see @samp{@code{coq-load-path-include-current}}).
-@var{warning}: if you use coq <= 8.4, the meaning of these options is
-not the same (-I is for coq path).
+@c TEXI DOCSTRING MAGIC: coq-compile-vio2vo-delay
+@defvar coq-compile-vio2vo-delay
+Delay in seconds for the vio2vo compilation.@*
+This delay helps to avoid running into a library inconsistency
+with @code{'quick-and-vio2vo}, see Coq issue #@var{5223}.
@end defvar
+Locking ancestors can be disabled with the following option.
-@c TEXI DOCSTRING MAGIC: coq-load-path-include-current
-@defvar coq-load-path-include-current
-If @samp{t} let coqdep search the current directory too.@*
-Should be @samp{t} for normal users. If @samp{t} pass -Q dir "" to coqdep when
-processing files in directory "dir" in addition to any entries
-in @samp{@code{coq-load-path}}.
-
-This setting is only relevant with Coq < 8.5.
+@c TEXI DOCSTRING MAGIC: coq-lock-ancestors
+@defvar coq-lock-ancestors
+If non-nil, lock ancestor module files.@*
+If external compilation is used (via @samp{@code{coq-compile-command}}) then
+only the direct ancestors are locked. Otherwise all ancestors are
+locked when the "Require" command is processed.
@end defvar
-The following two options configure an external compilation
-process.
-
+The sequential compilation setting supports an external
+compilation command (which could be a parallel running
+@code{make}). For this set
+@code{coq-compile-parallel-in-background} to @code{nil} and
+configure the compilation command in @code{coq-compile-command}.
@c TEXI DOCSTRING MAGIC: coq-compile-command
@defvar coq-compile-command
@@ -4829,39 +4899,65 @@ This option can be set/reset via menu
@end defvar
-Locking ancestors can be disabled with the following option.
+The preferred way to configure the load path and the mapping of
+logical library names to physical file path is the Coq project
+file, @ref{Using the Coq project file}. Alternatively one can
+configure these things with the following options.
-@c TEXI DOCSTRING MAGIC: coq-lock-ancestors
-@defvar coq-lock-ancestors
-If non-nil, lock ancestor module files.@*
-If external compilation is used (via @samp{@code{coq-compile-command}}) then
-only the direct ancestors are locked. Otherwise all ancestors are
-locked when the "Require" command is processed.
-@end defvar
+@c TEXI DOCSTRING MAGIC: coq-load-path
+@defvar coq-load-path
+Non-standard coq library load path.@*
+This list specifies the LoadPath extension for coqdep, coqc and
+coqtop. Usually, the elements of this list are strings (for
+"-I") or lists of two strings (for "-R" dir path and
+"-Q" dir path).
+
+The possible forms of elements of this list correspond to the 4
+forms of include options (@samp{-I} @samp{-Q} and @samp{-R}). An element can be
+@lisp
+ - A list of the form @samp{(}ocamlimport dir)', specifying (in 8.5) a
+ directory to be added to ocaml path (@samp{-I}).
+ - A list of the form @samp{(}rec dir path)' (where dir and path are
+ strings) specifying a directory to be recursively mapped to the
+ logical path @samp{path} (@samp{-R dir path}).
+ - A list of the form @samp{(}recnoimport dir path)' (where dir and
+ path are strings) specifying a directory to be recursively
+ mapped to the logical path @samp{path} (@samp{-Q dir path}), but not
+ imported (modules accessible for import with qualified names
+ only). Note that -Q dir "" has a special, nonrecursive meaning.
+ - A list of the form (8.4 only) @samp{(}nonrec dir path)', specifying a
+ directory to be mapped to the logical path @code{'path'} ('-I dir -as path').
+@end lisp
+For convenience the symbol @samp{rec} can be omitted and entries of
+the form @samp{(dir path)} are interpreted as @samp{(rec dir path)}.
+A plain string maps to -Q ... "" in 8.5, and -I ... in 8.4.
-The following option controls which warnings of @code{coqdep}
-are treated as errors.
-
-@c TEXI DOCSTRING MAGIC: coq-coqdep-error-regexp
-@defvar coq-coqdep-error-regexp
-Regexp to match errors in the output of coqdep.@*
-coqdep indicates errors not always via a non-zero exit status,
-but sometimes only via printing warnings. This regular expression
-is used for recognizing error conditions in the output of
-coqdep (when coqdep terminates with exit status 0). Its default
-value matches the warning that some required library cannot be
-found on the load path and ignores the warning for finding a
-library at multiple places in the load path. If you want to turn
-the latter condition into an error, then set this variable to
-"^\*\*\* Warning".
+Under normal circumstances this list does not need to
+contain the coq standard library or "." for the current
+directory (see @samp{@code{coq-load-path-include-current}}).
+
+@var{warning}: if you use coq <= 8.4, the meaning of these options is
+not the same (-I is for coq path).
@end defvar
-The following two options do only influence the behaviour if
-Proof General does dependency checking and compilation itself.
-These options determine whether Proof General should descend into
-other Coq libraries and into the Coq standard library.
+@c TEXI DOCSTRING MAGIC: coq-load-path-include-current
+@defvar coq-load-path-include-current
+If @samp{t} let coqdep search the current directory too.@*
+Should be @samp{t} for normal users. If @samp{t} pass -Q dir "" to coqdep when
+processing files in directory "dir" in addition to any entries
+in @samp{@code{coq-load-path}}.
+
+This setting is only relevant with Coq < 8.5.
+@end defvar
+
+During library dependency checking Proof General does not dive
+into the Coq standard library or into libraries that are
+installed as user contributions. This stems from @code{coqdep},
+which does not output dependencies to these directories.
+The internal dependency check can also ignore additional
+libraries.
@c TEXI DOCSTRING MAGIC: coq-compile-ignored-directories
@defvar coq-compile-ignored-directories
@@ -4872,84 +4968,25 @@ 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.
-@end defvar
-
-
-@c TEXI DOCSTRING MAGIC: coq-compile-ignore-library-directory
-@defvar coq-compile-ignore-library-directory
-If non-nil, ProofGeneral does not compile modules from the coq library.@*
-Should be @samp{t} for normal coq users. If @samp{nil} library modules are
-compiled if their sources are newer.
-
-This option has currently no effect, because Proof General uses
-coqdep to translate qualified identifiers into library file names
-and coqdep does not output dependencies in the standard library.
-@end defvar
-
-
-The last three Emacs constants are internal parameters. They only
-need to be changed under very special, unforeseen circumstances.
-They can only be set in Emacs lisp code because they are no
-customizable user options.
-
-@c TEXI DOCSTRING MAGIC: coq-compile-substitution-list
-@defvar coq-compile-substitution-list
-Substitutions for @samp{@code{coq-compile-command}}.@*
-Value must be a list of substitutions, where each substitution is
-a 2-element list. The first element of a substitution is the
-regexp to substitute, the second the replacement. The replacement
-is evaluated before passing it to @samp{@code{replace-regexp-in-string}}, so
-it might be a string, or one of the symbols @code{'physical-dir},
-@code{'module-object}, @code{'module-source}, @code{'qualified-id} and
-@code{'requiring-file}, which are bound to, respectively, the physical
-directory containing the source file, the Coq object file in
-@code{'physical-dir} that will be loaded, the Coq source file in
-@code{'physical-dir} whose object will be loaded, the qualified module
-identifier that occurs in the "Require" command, and the file
-that contains the "Require".
-@end defvar
-
-
-@c TEXI DOCSTRING MAGIC: coq-require-command-regexp
-@defvar coq-require-command-regexp
-Regular expression matching Require commands in Coq.@*
-Should match "Require" with its import and export variants up to (but not
-including) the first character of the first required module. The required
-modules are matched separately with @samp{@code{coq-require-id-regexp}}
+that dependency checking takes noticeable time. The regular
+expressions in here are always matched against the .vo file name,
+regardless whether @samp{`-quick}' would be used to compile the file
+or not.
@end defvar
-@c TEXI DOCSTRING MAGIC: coq-require-id-regexp
-@defvar coq-require-id-regexp
-Regular expression matching one Coq module identifier.@*
-Should match precisely one complete module identifier and surrounding
-white space. The module identifier must be matched with group number 1.
-Note that the trailing dot in "Require A." is not part of the module
-identifier and should therefore not be matched by this regexp.
-@end defvar
-
-
-
@node Current Limitations
@subsection Current Limitations
-In the current release some aspects of multiple file support have
-not been implemented. The following points will hopefully
-be addressed at some stage.
-
@itemize
@item
-Support @code{Declare ML Module} commands.
+No support @code{Declare ML Module} commands.
@item
-Increase precision when comparing modification times. Because of
-an Emacs limitation, modification time stamps of files have only a
-precision of 1 second. If several compiled Coq object files have
-been created in the same second, Proof General is optimistic and
-does not recompile. (Note that GNU make behaves the same on file
-systems that record time stamps only with a precision of 1
-second.) Emacs version 24.3 implements high precision time stamps
-on files.
+When a compiled library has the same time stamp as the source
+file, it is considered outdated. Some old file systems (for
+instance ext3) or Emacs before version 24.3 support only time
+stamps with one second granularity. On such configurations Proof
+General will perform some unnecessary compilations.
@end itemize
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-24 03:28:19 +0000