first version for quick compilation

Select "Quick compilation mode" in the Coq menu. See also
documentation of coq-compile-quick, the and-vio2vo stuff is not yet
there.

5 files changed, 899 insertions, 99 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index f23ac786..5be98c32 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -148,6 +148,27 @@ It was constructed with `proof-defstringset-fn'.")
      :style toggle
      :selected coq-double-hit-enable
      :help "Automatically send commands when terminator typed twiced quickly."]
+    ("Quick compilation mode"
+     ["no quick"
+      (customize-set-variable 'coq-compile-quick 'no-quick)
+      :style radio
+      :selected (eq coq-compile-quick 'no-quick)
+      :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)
+      :help "Compile with -quick, accept existing .vo's"]
+     ["quick and vio2vo"
+      (customize-set-variable 'coq-compile-quick 'quick-and-vio2vo)
+      :style radio
+      :selected (eq coq-compile-quick 'quick-and-vio2vo)
+      :help "Compile with -quick, accept existing .vo's, run vio2vo"]
+     ["ensure vo"
+      (customize-set-variable 'coq-compile-quick 'ensure-vo)
+      :style radio
+      :selected (eq coq-compile-quick 'ensure-vo)
+      :help "Ensure only vo's are used for consistency"])
     ""
     ["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..a6b5abb3 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -149,6 +149,59 @@ 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.
+
+Note that ``-quick'' can be noticebly slower when your sources do not
+declare section variables with ``Proof using''. 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 when the
+quick recompilation finished (see also `coq-compile-vio2vo-percentage').
+Note that all the previously described modes might load .vio files and
+that you therefore might not notice certain universe inconsitencies.
+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 Not yet supported, currently the same as `quick-no-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'.
+ensure-vo        Delete all .vio files for prerequisites and recompile
+                 without ``-quick'' as necessary. This setting is the
+                 only one that esures 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)))
+  :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
@@ -266,7 +319,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)
@@ -360,20 +416,16 @@ 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
@@ -394,11 +446,16 @@ is up-to-date."
 
 ;;; convert .vo files to .v files
 
-(defun coq-library-src-of-obj-file (lib-obj-file)
+(defun coq-library-src-of-vo-file (lib-obj-file)
   "Return source file name for LIB-OBJ-FILE.
 Chops off the last character of LIB-OBJ-FILE to convert \"x.vo\" to \"x.v\"."
   (substring lib-obj-file 0 (- (length lib-obj-file) 1)))
 
+(defun coq-library-vio-of-vo-file (vo-obj-file)
+  "Return .vio file name for VO-OBJ-FILE.
+Changes the suffix from .vio to .vo. VO-OBJ-FILE must have a .vo suffix."
+  (concat (coq-library-src-of-vo-file vo-obj-file) "io"))
+
 
 ;;; ancestor unlocking
 ;;; (locking is different for sequential and parallel compilation)
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index 19859195..167c0869 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:
 ;;
@@ -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
@@ -274,11 +301,12 @@ property).")
 
 (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
   "Pointer to the last top-level compilation job.
@@ -410,6 +438,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
 
@@ -466,7 +509,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,7 +520,11 @@ 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."
+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
@@ -492,6 +539,11 @@ this buffer visible and returns a string."
 	"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 +572,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))
@@ -544,8 +599,8 @@ break."
     ;;              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 +610,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
@@ -794,48 +852,142 @@ errors are reported with an error message."
       (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."
+  (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 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-p 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-p 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
+	    (time-less-p max-obj-time src-time) ; src is younger than any obj
+	    (time-less-p max-obj-time dep-time)) ; dep is younger than any obj
+	;; 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)))
+	    (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
+		;; need to ensure no .vio is laying around
+		(progn
+		  (put job 'obj-mod-time vo-obj-time)
+		  (when vio-obj-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)
+	      (when vio-obj-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.
+	(if vio-is-newer
+	    (progn
+	      (put job 'required-obj-file vio-file)
+	      (put job 'obj-mod-time vio-obj-time)
+	      (when (and vo-obj-time
+			 (or (time-less-p vo-obj-time src-time)
+			     ;; dep-time is neither nil nor 'just-compiled here
+			     (time-less-p vo-obj-time dep-time)))
+		(setq file-to-delete vo-file))
+	      (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 (and vio-obj-time
+		     (or (time-less-p vio-obj-time src-time)
+			 ;; dep-time is neither nil nor 'just-compiled here
+			 (time-less-p vio-obj-time dep-time)))
+	    (setq file-to-delete vio-file))
+	  (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.
@@ -906,12 +1058,17 @@ case, the following actions are taken:
 
 (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.
   (if (coq-par-job-needs-compilation job)
       (coq-par-start-or-enqueue job)
     (if coq-debug-auto-compilation
@@ -985,7 +1142,7 @@ 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
 	(message "%s: kickoff %d coqc dependencies with time %s"
@@ -1030,13 +1187,19 @@ 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)))))))
 
 (defun coq-par-start-jobs-until-full ()
   "Start background jobs until the limit is reached."
@@ -1056,7 +1219,7 @@ room for Proof General."
       (coq-par-start-task new-job)
     (coq-par-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 +1248,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 'vo-file module-vo-file)
     (put new-job 'coqc-dependency-count 0)
     (put new-job 'require-span require-span)
+    ;; fields 'required-obj-file and obj-mod-time are implicitely set to nil
     (if orig-job
-	;; there is already a compilation job for module-obj-file
+	;; there is already a compilation job for module-vo-file
 	(progn
 	  (put new-job 'type 'clone)
 	  (if coq-debug-auto-compilation
 	      (message "%s: create %s compilation job for %s"
-		       (get new-job 'name) (get new-job 'type) module-obj-file))
+		       (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 +1276,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 +1287,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)
+      (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))
@@ -1168,9 +1332,9 @@ is directly passed to `coq-par-analyse-coq-dep-exit'."
       (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)))
@@ -1228,20 +1392,20 @@ might be used."
 	  (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 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-par-create-library-job module-vo-file coq-load-path
 					coq-last-compilation-job span
 					"scripting buffer"))
       (setq coq-last-compilation-job module-job)
diff --git a/coq/coq-par-test.el b/coq/coq-par-test.el
new file mode 100644
index 00000000..9ebd775c
--- /dev/null
+++ b/coq/coq-par-test.el
@@ -0,0 +1,558 @@
+;; 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
+;; - add tests for files with identical time stamps
+
+
+(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 | 'obj-mod-t
+    ;; ====================================================================
+    ;; all of src dep vo vio present
+    ((src dep vo vio)
+     (no-quick           nil            nil       vio            vio)
+     (quick              nil            nil       vio            vio)
+     (ensure-vo          nil            vio       vo             vo))
+
+    ((src dep vio vo)
+     (no-quick           nil            nil       vo             vo  )
+     (quick              nil            nil       vo             vo  )
+     (ensure-vo          nil            vio       vo             vo  ))
+
+    ((src vo dep vio)    
+     (no-quick           nil            vo        vio            vio )
+     (quick              nil            vo        vio            vio )
+     (ensure-vo          t              vio       vo             nil ))
+
+    ((src vo vio dep)
+     (no-quick           t              vio       vo             nil )
+     (quick              t              vo        vio            nil )
+     (ensure-vo          t              vio       vo             nil ))
+
+    ((src vio dep vo)
+     (no-quick           nil            vio       vo             vo  )
+     (quick              nil            vio       vo             vo  )
+     (ensure-vo          nil            vio       vo             vo  ))
+
+    ((src vio vo dep)
+     (no-quick           t              vio       vo             nil )
+     (quick              t              vo        vio            nil )
+     (ensure-vo          t              vio       vo             nil ))
+
+    ;; present files   | compilation? | delete | 'req-obj-file | 'obj-mod-t
+    ((dep src vio vo)
+     (no-quick           nil            nil       vo             vo  )
+     (quick              nil            nil       vo             vo  )
+     (ensure-vo          nil            vio       vo             vo  ))
+
+    ((dep src vo vio)
+     (no-quick           nil            nil       vio            vio )
+     (quick              nil            nil       vio            vio )
+     (ensure-vo          nil            vio       vo             vo  ))
+
+    ((dep vo vio src)
+     (no-quick           t              vio       vo             nil )
+     (quick              t              vo        vio            nil )
+     (ensure-vo          t              vio       vo             nil ))
+
+    ((dep vo src vio)
+     (no-quick           nil            vo        vio            vio )
+     (quick              nil            vo        vio            vio )
+     (ensure-vo          t              vio       vo             nil ))
+
+    ((dep vio vo src)
+     (no-quick           t              vio       vo             nil )
+     (quick              t              vo        vio            nil )
+     (ensure-vo          t              vio       vo             nil  ))
+
+    ((dep vio src vo)
+     (no-quick           nil            vio       vo             vo  )
+     (quick              nil            vio       vo             vo  )
+     (ensure-vo          nil            vio       vo             vo  ))
+
+    ((vo src dep vio)
+     (no-quick           nil            vo        vio            vio )
+     (quick              nil            vo        vio            vio )
+     (ensure-vo          t              vio       vo             nil ))
+
+    ;; present files   | compilation? | delete | 'req-obj-file | 'obj-mod-t
+    ((vo src vio dep)
+     (no-quick           t              vio       vo             nil )
+     (quick              t              vo        vio            nil )
+     (ensure-vo          t              vio       vo             nil ))
+
+    ((vo dep src vio)
+     (no-quick           nil            vo       vio             vio )
+     (quick              nil            vo       vio             vio )
+     (ensure-vo          t              vio       vo             nil ))
+
+    ((vo dep vio src)
+     (no-quick           t              vio       vo             nil )
+     (quick              t              vo        vio            nil )
+     (ensure-vo          t              vio       vo             nil ))
+
+    ((vo vio src dep)
+     (no-quick           t              vio      vo              nil )
+     (quick              t              vo       vio             nil )
+     (ensure-vo          t              vio       vo             nil ))
+
+    ((vo vio dep src)
+     (no-quick           t              vio      vo              nil )
+     (quick              t              vo       vio             nil )
+     (ensure-vo          t              vio       vo             nil ))
+
+    ((vio src vo dep)
+     (no-quick           t              vio      vo              nil )
+     (quick              t              vo       vio             nil )
+     (ensure-vo          t              vio       vo             nil ))
+
+    ((vio src dep vo)
+     (no-quick           nil            vio      vo              vo  )
+     (quick              nil            vio      vo              vo  )
+     (ensure-vo          nil            vio       vo             vo  ))
+
+    ((vio dep vo src)
+     (no-quick           t              vio      vo              nil )
+     (quick              t              vo       vio             nil )
+     (ensure-vo          t              vio       vo             nil ))
+
+    ;; present files   | compilation? | delete | 'req-obj-file | 'obj-mod-t
+    ((vio dep src vo)
+     (no-quick           nil            vio      vo              vo  )
+     (quick              nil            vio      vo              vo  )
+     (ensure-vo          nil            vio       vo             vo  ))
+
+    ((vio vo dep src)
+     (no-quick           t              vio      vo              nil )
+     (quick              t              vo       vio             nil )
+     (ensure-vo          t              vio       vo             nil ))
+
+    ((vio vo src dep)
+     (no-quick           t              vio      vo              nil )
+     (quick              t              vo       vio             nil )
+     (ensure-vo          t              vio       vo             nil ))
+
+
+    ;; only src dep vo present
+    ((src dep vo)
+     (no-quick           nil            nil      vo              vo  )
+     (quick              nil            nil      vo              vo  )
+     (ensure-vo          nil            nil      vo              vo  ))
+
+    ((src vo dep)
+     (no-quick           t              nil      vo              nil )
+     (quick              t              vo       vio             nil )
+     (ensure-vo          t              nil      vo              nil ))
+
+    ((dep src vo)
+     (no-quick           nil            nil      vo              vo  )
+     (quick              nil            nil      vo              vo  )
+     (ensure-vo          nil            nil      vo              vo  ))
+
+    ((dep vo src)
+     (no-quick           t              nil      vo              nil )
+     (quick              t              vo       vio             nil )
+     (ensure-vo          t              nil      vo              nil ))
+
+    ((vo src dep)
+     (no-quick           t              nil      vo              nil )
+     (quick              t              vo       vio             nil )
+     (ensure-vo          t              nil      vo              nil ))
+
+    ((vo dep src)
+     (no-quick           t              nil      vo              nil )
+     (quick              t              vo       vio             nil )
+     (ensure-vo          t              nil      vo              nil ))
+
+
+    ;; present files   | compilation? | delete | 'req-obj-file | 'obj-mod-t
+    ;; only src dep vio present
+    ((src dep vio)
+     (no-quick           nil            nil      vio             vio )
+     (quick              nil            nil      vio             vio )
+     (ensure-vo          t              vio       vo             nil ))
+
+    ((src vio dep)
+     (no-quick           t             vio       vo              nil )
+     (quick              t             nil       vio             nil )
+     (ensure-vo          t              vio       vo             nil ))
+
+    ((dep src vio)
+     (no-quick           nil           nil       vio             vio )
+     (quick              nil           nil       vio             vio )
+     (ensure-vo          t              vio       vo             nil ))
+
+    ((dep vio src)
+     (no-quick           t             vio       vo              nil )
+     (quick              t             nil       vio             nil )
+     (ensure-vo          t              vio       vo             nil ))
+
+    ((vio src dep)
+     (no-quick           t             vio       vo              nil )
+     (quick              t             nil       vio             nil )
+     (ensure-vo          t              vio       vo             nil ))
+
+    ((vio dep src)
+     (no-quick           t             vio       vo              nil )
+     (quick              t             nil       vio             nil )
+     (ensure-vo          t              vio       vo             nil ))
+
+
+    ;; present files   | compilation? | delete | 'req-obj-file | 'obj-mod-t
+    ;; only src vo vio present
+    ((src vo vio)
+     (no-quick           nil            nil      vio             vio )
+     (quick              nil            nil      vio             vio )
+     (ensure-vo          nil            vio       vo             vo  ))
+
+    ((src vio vo)
+     (no-quick           nil            nil      vo              vo  )
+     (quick              nil            nil      vo              vo  )
+     (ensure-vo          nil            vio       vo             vo  ))
+
+    ((vo src vio)
+     (no-quick           nil            vo       vio             vio )
+     (quick              nil            vo       vio             vio )
+     (ensure-vo          t              vio       vo             nil ))
+
+    ((vo vio src)
+     (no-quick           t              vio      vo              nil )
+     (quick              t              vo       vio             nil )
+     (ensure-vo          t              vio       vo             nil ))
+
+    ((vio src vo)
+     (no-quick           nil            vio      vo              vo  )
+     (quick              nil            vio      vo              vo  )
+     (ensure-vo          nil            vio      vo              vo  ))
+
+    ((vio vo src)
+     (no-quick           t              vio      vo              nil )
+     (quick              t              vo       vio             nil )
+     (ensure-vo          t              vio       vo             nil ))
+
+
+    ;; present files   | compilation? | delete | 'req-obj-file | 'obj-mod-t
+    ;; only src dep present
+    ((src dep)
+     (no-quick           t              nil      vo              nil )
+     (quick              t              nil      vio             nil )
+     (ensure-vo          t              nil      vo              nil ))
+
+    ((dep src)
+     (no-quick           t              nil      vo              nil )
+     (quick              t              nil      vio             nil )
+     (ensure-vo          t              nil      vo              nil ))
+
+
+    ;; only src vo present
+    ((src vo)
+     (no-quick           nil            nil      vo              vo  )
+     (quick              nil            nil      vo              vo  )
+     (ensure-vo          nil            nil      vo              vo  ))
+
+    ((vo src)
+     (no-quick           t              nil      vo              nil )
+     (quick              t              vo       vio             nil )
+     (ensure-vo          t              nil      vo              nil ))
+
+
+    ;; only src vio present
+    ((src vio)
+     (no-quick           nil            nil      vio             vio )
+     (quick              nil            nil      vio             vio )
+     (ensure-vo          t              vio       vo             nil ))
+
+    ((vio src)
+     (no-quick           t              vio      vo              nil )
+     (quick              t              nil      vio             nil )
+     (ensure-vo          t              vio       vo             nil ))
+
+
+    ;; only src present
+    ((src)
+     (no-quick           t              nil      vo              nil )
+     (quick              t              nil      vio             nil )
+     (ensure-vo          t              nil      vo              nil ))
+    )
+  "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.
+
+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 5 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. Element 5 specifies the file whose time stamp must
+be stored in the `obj-mod-time' property of the job. A value of
+nil there specifies that the `obj-mod-time' property should
+contain nil. Element 5 is a bit superfluous, because it must be
+set precisely when no compilation is needed (element 2 equals
+nil) and then it must equal element 4.
+
+This list contains 1 test for all possible file configuration and
+relative ages.")
+
+;; missing test cases for some objects with identical time stamp
+;;
+;; src-vo-dep-vio
+;; 
+;; src-vo-dep vio
+;; vio src-vo-dep
+;; src-vo-vio dep
+;; dep src-vo-vio
+;; src-dep-vio vo
+;; vo src-dep-vio
+;; vo-dep-vio src
+;; src vo-dep-vio
+;; 
+;; src-vo dep-vio
+;; dep-vio src-vo
+;; src-dep vo-vio
+;; vo-vio src-dep
+;; src-vio vo-dep
+;; vo-dep src-vio
+;; 
+;; src-vo dep vio
+;; src-vo vio dep
+;; dep src-vo vio
+;; dep vio src-vo
+;; vio src-vo dep
+;; vio dep src-vo
+;; 
+;; src-dep vo vio
+;; src-dep vio vo
+;; vo src-dep vio
+;; vo vio src-dep
+;; vio src-dep vo
+;; vio vo src-dep
+;; 
+;; src-vio vo dep
+;; src-vio dep vo
+;; vo src-vio dep
+;; vo dep src-vio
+;; dep src-vio vo
+;; dep vo src-vio
+;; 
+;; vo-dep src vio
+;; vo-dep vio src
+;; src vo-dep vio
+;; src vio vo-dep
+;; vio vo-dep src
+;; vio src vo-dep
+;; 
+;; vo-vio src dep
+;; vo-vio dep src
+;; src vo-vio dep
+;; src dep vo-vio
+;; dep vo-vio src
+;; dep src vo-vio
+;; 
+;; dep-vio src vo
+;; dep-vio vo src
+;; src dep-vio vo
+;; src vo dep-vio
+;; vo dep-vio src
+;; vo src dep-vio
+
+(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 5 elements
+	  (assert (eq (length variant) 5) nil (concat test-id " 2"))
+	  (let ((compilation-result (nth 1 variant))
+		(delete-result (nth 2 variant))
+		(req-obj-result (nth 3 variant))
+		(obj-mod-result (nth 4 variant)))
+	    ;; when the obj-mod-time field is set, it must be equal to
+	    ;; the required-obj-file field
+	    (assert (or (not obj-mod-result)
+			(eq req-obj-result obj-mod-result))
+		    nil (concat test-id " 3"))
+	    (if compilation-result
+		;; when compilation is t, obj-mod-time must be set
+		(assert (not obj-mod-result) nil (concat test-id " 4"))
+	      ;; when compilation? is nil, obj-mod-result must be nil
+	      (assert obj-mod-result nil (concat test-id " 5")))
+	    ;; the delete field, when set, must be a member of the files list
+	    (assert (or (not delete-result)
+			(member delete-result (car test)))
+		    nil (concat test-id " 6"))))
+	  (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 files 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) files
+		    (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))
+	(obj-mod-result (nth 4 variant))
+	result non-deleted-files)
+    (message "test case %s" id)
+    (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
+    (mapc
+     (lambda (sym)
+       (let ((file (test-coq-par-sym-to-file dir sym)))
+	 ;;(message "file create for %s: %s" sym file)
+	 (with-temp-file file t)
+	 (when (eq sym 'dep)
+	   (put job 'youngest-coqc-dependency (nth 5 (file-attributes file))))
+	 (unless (eq sym delete-result)
+	   (push file non-deleted-files))
+	 (sleep-for 0 10)
+	 ))
+     files)
+    (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
+    (mapc
+     (lambda (f)
+       (assert (file-attributes f)
+	       nil (concat id " non del file " f)))
+     non-deleted-files)
+    ;; 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"))))
+
+(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 date 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..031fc492 100644
--- a/coq/coq-seq-compile.el
+++ b/coq/coq-seq-compile.el
@@ -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.