option coq-compile-keep-going for parallel compilation

With this option set, compilation continues after the first error
to compile as much as possible and to potentially report more
than one error.

4 files changed, 376 insertions, 130 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 767d2a6e..ec8d5e80 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -161,7 +161,15 @@ It was constructed with `proof-defstringset-fn'.")
       :active coq-compile-before-require
       :help ,(concat "Compile parallel in background or "
 		    "sequentially with blocking ProofGeneral.")]
-     ["no quick"
+     ["Keep going"
+      coq-compile-keep-going-toggle
+      :style toggle
+      :selected coq-compile-keep-going
+      :active (and coq-compile-before-require
+		   coq-compile-parallel-in-background)
+      :help ,(concat "Continue background compilation after "
+		     "the first error as far as possible")]
+    ["no quick"
       (customize-set-variable 'coq-compile-quick 'no-quick)
       :style radio
       :selected (eq coq-compile-quick 'no-quick)
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index 1f31c1d3..40e3a4d7 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -261,6 +261,16 @@ ensure-vo        Ensure that all library dependencies are present as .vo
    (eq coq-compile-quick 'quick-no-vio2vo)
    (eq coq-compile-quick 'quick-and-vio2vo)))
 
+(defcustom coq-compile-keep-going t
+  "Continue compilation after the first error as far as possible.
+Similar to ``make -k'', with this option enabled, the background
+compilation continues after the first error as far as possible.
+With this option disabled, the background compilation is
+immediately stopped after the first error.")
+
+;; define coq-compile-keep-going-toggle
+(proof-deftoggle coq-compile-keep-going)
+
 (defcustom coq-max-background-compilation-jobs 'all-cpus
   "Maximal number of parallel jobs, if parallel compilation is enabled.
 Use the number of available CPU cores if this is set to
@@ -544,7 +554,10 @@ Changes the suffix from .vio to .vo. VO-OBJ-FILE must have a .vo suffix."
 
 (defun coq-unlock-ancestor (ancestor-src)
   "Unlock ANCESTOR-SRC."
-  (let* ((true-ancestor (file-truename ancestor-src)))
+  (let* ((default-directory
+	   (buffer-local-value 'default-directory
+			       (or proof-script-buffer (current-buffer))))
+	 (true-ancestor (file-truename ancestor-src)))
     (setq proof-included-files-list
           (delete true-ancestor proof-included-files-list))
     (proof-restart-buffers (proof-files-to-buffers (list true-ancestor)))))
@@ -561,11 +574,14 @@ Changes the suffix from .vio to .vo. VO-OBJ-FILE must have a .vo suffix."
   "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)
+  (unless (buffer-live-p (get-buffer coq--compile-response-buffer))
     (coq-init-compile-response-buffer))
-  (let ((inhibit-read-only t))
+  (let ((inhibit-read-only t)
+	(deactivate-mark nil))
     (with-current-buffer coq--compile-response-buffer
-      (insert command "\n" error-message)))
+      (save-excursion
+	(goto-char (point-max))
+	(insert command "\n" error-message "\n"))))
   (when display
     (coq-display-compile-response-buffer)))
 
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index 0b297be4..72de6894 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -121,10 +121,27 @@
 ;;
 ;; For 3- error reporting:
 ;;
-;; For now, all compilation jobs are killed on the first error. All
-;; items that are not yet asserted are retract. This is done with
-;; signalling an error and calling `coq-par-emergency-cleanup' in the
-;; sentinel, if there was an error.
+;; Depending on `coq-compile-keep-going' compilation can continue
+;; after an error or stop immediately. For stopping immediately,
+;; processing is aborted with a signal that eventually leads to
+;; `coq-par-emergency-cleanup', which kills all compilation jobs,
+;; retracts the queue region and resets all internal data.
+;;
+;; For `coq-compile-keep-going', the failing job and all dependants
+;; are marked as 'failed. Queue dependants are marked with
+;; 'queue-failed. These marked jobs continue with their normal state
+;; transition, but omit certain steps (eg., running coqc). The first
+;; tricky part is how to unlock ancestors. When marking jobs as
+;; failed, their ancestors (and thereby also the files for the jobs
+;; themselves) are unlocked, unless they are still participating in an
+;; ongoing compilation. If a coqc compilation finishes and all
+;; dependants are marked as failed, ancestors are also unlocked in the
+;; same way. If a top-level job is marked as 'queue-failed, its
+;; ancestors are unlocked when this job finishes coqc compilation.
+;;
+;; The second tricky part is how to delete the queue region. For that
+;; the last top-level job is delayed until proof-action-list is empty.
+;; Then the whole queue is deleted.
 ;;
 ;; For 4- using -quick and the handling of .vo/.vio prerequisites
 ;;
@@ -189,17 +206,21 @@
 ;;   'load-path       - value of coq-load-path, propagated to all
 ;;                      dependencies 
 ;;   'ancestors       - list of ancestor jobs, for real compilation jobs
-;;                      this list includes the job itself
+;;                      this list includes the job itself; may contain
+;;                      duplicates
 ;;   'lock-state      - nil for clone jobs, 'unlocked if the file
 ;;                      corresponding to job is not locked, 'locked if that
 ;;                      file has been locked, 'asserted if it has been
 ;;                      registered in some span in the 'coq-locked-ancestors
 ;;                      property already
-;;   'require-span    - present for top-level jobs only, there it
+;;   'require-span    - present precisely for top-level jobs only, there it
 ;;                      contains the span that must finally store the
 ;;                      ancestors
 ;;   'vio2vo-needed   - t if a subsequent vio2vo process is required to
 ;;                      build the .vo file. Otherwiese nil.
+;;   'failed          - t if coqdep or coqc for the job or one dependee failed.
+;;   'queue-failed    - t if some direct or indirect queue dependee is
+;;                      marked 'failed
 ;;   'visited         - used in the dependency cycle detection to mark
 ;;                      visited jobs
 ;;
@@ -307,6 +328,10 @@ Used to link top-level jobs with queue dependencies.")
   "Increased for every job and process, to get unique job names.
 The names are only used for debugging.")
 
+(defvar coq--par-delayed-last-job nil
+  "Inform the cycle detection that there is a delayed top-level job.
+If t, there is a delayed top-level job (for which the compilation failed).")
+
 
 ;;; utility functions
 
@@ -707,7 +732,7 @@ function returns () if MODULE-ID comes from the standard library."
      (process-list))
     (setq coq--current-background-jobs 0)))
 
-(defun coq-par-unlock-ancestors-on-error ()
+(defun coq-par-unlock-all-ancestors-on-error ()
   "Unlock ancestors which are not in an asserted span.
 Used for unlocking ancestors on compilation errors."
   (when coq--compilation-object-hash
@@ -733,7 +758,7 @@ and resets the internal state."
     (cancel-timer coq--compile-vio2vo-delay-timer))
   (when proof-action-list
     (setq proof-shell-interrupt-pending t))
-  (coq-par-unlock-ancestors-on-error)
+  (coq-par-unlock-all-ancestors-on-error)
   (proof-release-lock)
   (proof-detach-queue)
   (setq proof-second-action-list-active nil)
@@ -828,6 +853,7 @@ errors are reported with an error message."
 	    (setq coq--compile-vio2vo-in-progress nil)
 	    (message "vio2vo compilation finished"))
 	  (when (and
+		 (not coq--par-delayed-last-job)
 		 (eq coq--current-background-jobs 0)
 		 coq--last-compilation-job)
 	    (let ((cycle (coq-par-find-dependency-circle)))
@@ -865,14 +891,28 @@ errors are reported with an error message."
   (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)))
+  "Callback for `proof-action-list' to signal completion of the last require.
+This function ensures that vio2vo compilation starts after
+`coq-compile-vio2vo-delay' seconds after the last module has been
+loaded into Coq. When background compilation is successful, this
+callback is inserted with a dummy item into proof-action-list
+somewhere after the last require command."
+  ;; When the user asserts new stuff while the (previously) last
+  ;; require command is being processed, `coq--last-compilation-job'
+  ;; might get non-nil. In this case there is a new last compilation
+  ;; job that will eventually trigger vio2vo compilation.
+  (unless coq--last-compilation-job
+    (setq coq--compile-vio2vo-delay-timer
+	  (run-at-time coq-compile-vio2vo-delay nil
+		       'coq-par-run-vio2vo-queue))))
+
+(defun coq-par-callback-queue-item (callback)
+  ;; A proof-action-list item has the form of
+  ;;            (SPAN COMMANDS ACTION [DISPLAYFLAGS])
+  ;; If COMMANDS is nil, the item is processed as comment and not sent
+  ;; to the proof assistant, only the callback is called, see
+  ;; proof-shell.el.
+  (list nil nil callback))
 
 
 ;;; background job tasks
@@ -1078,21 +1118,71 @@ therefore delete a file if it might be in the way. Sets the
 	 (signal 'coq-compile-error-rm err))))
     result))
 
+(defun coq-par-retire-top-level-job (job)
+  "Register ancestors and start queue items.
+This function performs the essential tasks for top-level jobs
+when they transition from 'waiting-queue to 'ready:
+- Registering ancestors in the span and recording this fact in
+  the 'lock-state property.
+- Moving queue items back to `proof-action-list' and start their
+  execution.
+- Insert `coq-par-require-processed' as callback if this is the
+  last top-level job, such that vio2vo compilation will start
+  eventually.
+
+This function can safely be called for non-top-level jobs. This
+function must not be called for failed jobs."
+  (assert (not (get job 'failed))
+	  nil "coq-par-retire-top-level-job precondition failed")
+  (let ((span (get job 'require-span))
+	(items (get job 'queueitems)))
+    (when (and span coq-lock-ancestors)
+      (dolist (anc-job (get job 'ancestors))
+	(assert (not (eq (get anc-job 'lock-state) 'unlocked))
+		nil "bad ancestor lock state")
+	(when (eq (get anc-job 'lock-state) 'locked)
+	  (put anc-job 'lock-state 'asserted)
+	  (push (get anc-job 'src-file)
+		(span-property span 'coq-locked-ancestors)))))
+    (when items
+      (when (and (eq coq-compile-quick 'quick-and-vio2vo)
+		 (eq coq--last-compilation-job job))
+	;; Insert a notification callback for when the last require
+	;; queue item has been processed.
+	(setq items
+	      (cons
+	       (car items)		; this is the require
+	       (cons
+		(coq-par-callback-queue-item 'coq-par-require-processed)
+		(cdr items)))))
+      (proof-add-to-queue items 'advancing)
+      (when coq--debug-auto-compilation
+	(message "%s: add %s items to action list"
+		 (get job 'name) (length items)))
+      (put job 'queueitems nil))))
+
 (defun coq-par-kickoff-queue-maybe (job)
   "Try transition 'waiting-queue -> 'ready for job JOB.
 This transition is only possible if JOB is in state
 'waiting-queue and if it has no queue dependee. If this is the
 case, the following actions are taken:
-- for top-level jobs (non-nil 'require-span property), ancestors
+- for successful top-level jobs (non-nil 'require-span property), ancestors
   are registered in the 'queue-span and marked as 'asserted in their
   'lock-state property
-- processing of items in 'queueitems is started
+- processing of items in 'queueitems is started (if JOB is successful)
 - a possible queue dependant gets it's dependency cleared, and,
   if possible the 'waiting-queue -> 'ready transition
   is (recursively) done for the dependant
 - if this job is the last top-level compilation
   job (`coq--last-compilation-job') then the last compilation job
-  and `proof-second-action-list-active' are cleared."
+  and `proof-second-action-list-active' are cleared and vio2vo
+  processing is triggered.
+- If compilation failed, the (failing) last top-level job is
+  delayed until `proof-action-list' is empty, possibly by
+  registering this call as a callback in an empty
+  proof-action-list item. When proof-action-list is empty, the
+  queue span is deleted, remaining spans are cleared and the
+  `proof-shell-busy' lock is freed."
   (if (or (not (eq (get job 'state) 'waiting-queue))
 	  (get job 'queue-dependant-waiting))
       (when coq--debug-auto-compilation
@@ -1104,63 +1194,61 @@ case, the following actions are taken:
 	   (get job 'name))))
     (when 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 (anc-job (get job 'ancestors))
-	  (assert (not (eq (get anc-job 'lock-state) 'unlocked))
-		  nil "bad ancestor lock state")
-	  (when (eq (get anc-job 'lock-state) 'locked)
-	    (put anc-job 'lock-state 'asserted)
-	    (push (get anc-job 'src-file)
-		  (span-property span 'coq-locked-ancestors))))))
-    (when (get job 'queueitems)
-      (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)
-	(when 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)
-    (when coq--debug-auto-compilation
-      (message "%s: ready" (get job 'name)))
-    (let ((dependant (get job 'queue-dependant)))
-      (if dependant
-	  (progn
-	    (assert (not (eq coq--last-compilation-job job))
-		    nil "coq--last-compilation-job invariant error")
-	    (put dependant 'queue-dependant-waiting nil)
-	    (when coq--debug-auto-compilation
-	      (message
-	       "%s -> %s: clear queue dependency, kickoff queue at %s"
-	       (get job 'name) (get dependant 'name) (get dependant 'name)))
-	    (coq-par-kickoff-queue-maybe dependant)
+    (unless (get job 'failed)
+      (coq-par-retire-top-level-job job))
+    (when (and (get job 'failed) (get job 'require-span))
+      (setq coq--par-delayed-last-job nil))
+    (if (and (get job 'failed)
+	     (eq coq--last-compilation-job job)
+	     proof-action-list)
+	(progn
+	  (when coq--debug-auto-compilation
+	    (message "%s: delay queue kickoff until action list is empty"
+		     (get job 'name)))
+	  (setq coq--par-delayed-last-job t)
+	  (proof-add-to-queue
+	   (list (coq-par-callback-queue-item
+		  `(lambda (span) (coq-par-kickoff-queue-maybe ',job))))
+	   'advancing))
+      (put job 'state 'ready)
+      (when coq--debug-auto-compilation
+	(message "%s: ready" (get job 'name)))
+      (let ((dependant (get job 'queue-dependant)))
+	(if dependant
+	    (progn
+	      (assert (not (eq coq--last-compilation-job job))
+		      nil "coq--last-compilation-job invariant error")
+	      (put dependant 'queue-dependant-waiting nil)
+	      (when coq--debug-auto-compilation
+		(message
+		 "%s -> %s: clear queue dependency, kickoff queue at %s"
+		 (get job 'name) (get dependant 'name) (get dependant 'name)))
+	      (coq-par-kickoff-queue-maybe dependant)
+	      (when coq--debug-auto-compilation
+		(message "%s: queue kickoff finished"
+			 (get job 'name))))
+	  (when (eq coq--last-compilation-job job)
+	    (when (get job 'failed)
+	      ;; proof-action-list is empty, see above
+	      ;; variables that hold the queue span are buffer local
+	      (with-current-buffer (or proof-script-buffer (current-buffer))
+		(proof-script-clear-queue-spans-on-error nil))
+	      (proof-release-lock)
+	      (when (eq coq-compile-quick 'quick-and-vio2vo)
+		(assert (not coq--compile-vio2vo-delay-timer)
+			nil "vio2vo timer set before last compilation job")
+		(setq coq--compile-vio2vo-delay-timer
+		      (run-at-time coq-compile-vio2vo-delay nil
+				   'coq-par-run-vio2vo-queue))))
+	    (setq coq--last-compilation-job nil)
+	    (setq proof-second-action-list-active nil)
 	    (when coq--debug-auto-compilation
-	      (message "%s: queue kickoff finished"
-		       (get job 'name))))
-	(when (eq coq--last-compilation-job job)
-	  (setq coq--last-compilation-job nil)
-	  (setq proof-second-action-list-active nil)
+	      (message "clear last compilation job"))
+	    (message "Library compilation %s"
+		     (if (get job 'failed) "failed" "finished successfully")))
 	  (when coq--debug-auto-compilation
-	    (message "clear last compilation job"))
-	  (message "Library compilation finished"))
-	(when coq--debug-auto-compilation
-	  (message "%s: no queue dependant, queue kickoff finished"
-		   (get job 'name)))))))
+	    (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.
@@ -1173,13 +1261,15 @@ 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
+  ;; 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)
+  ;; It also sets the 'vio2vo-needed property if needed.
+  (if (and (not (get job 'failed)) (coq-par-job-needs-compilation job))
       (coq-par-start-or-enqueue job)
     (when coq--debug-auto-compilation
-      (message "%s: up-to-date, no compilation" (get job 'name)))
+      (message "%s: %s, no compilation"
+	       (get job 'name)
+	       (if (get job 'failed) "failed" "up-to-date")))
     (when (get job 'vio2vo-needed)
       (coq-par-vio2vo-enqueue job))
     (coq-par-kickoff-coqc-dependants job (get job 'youngest-coqc-dependency))))
@@ -1232,7 +1322,8 @@ waiting-queue for JOB.
 
 DEP-TIME is either 'just-compiled, when JOB has just finished
 compilation, or the most recent modification time of all
-dependencies of JOB.
+dependencies of JOB. (If compilation for JOB failed, DEP-TIME is
+meaningless but should nevertheless be a non-nil valid argument.)
 
 This function makes the following actions.
 - Clear the dependency from JOB to all its dependants, thereby
@@ -1241,16 +1332,22 @@ This function makes the following actions.
 - save the maximum of DEP-TIME and .vo modification time in
   'youngest-coqc-dependency, in case we later create a clone of this job
 - put JOB into state 'waiting-queue
-- try to trigger the transition 'waiting-queue -> ready for JOB"
-  (let ((ancestors (get job 'ancestors)))
+- try to trigger the transition 'waiting-queue -> ready for JOB
+- If JOB is successful but all dependants have failed, unlock all
+  ancestors in case they are not participating in a still ongoing
+  compilation."
+  (let ((ancestors (get job 'ancestors))
+	(dependant-alive nil))
+    (put job 'state 'waiting-queue)
     ;; take max of dep-time and obj-mod-time
     ;; 
     ;; dep-time is either 'just-compiled or 'youngest-coqc-dependency of
     ;; the dependee, in the latter case obj-mod-time is greater than
     ;; dep-time, because otherwise we would have compiled the file. For
     ;; a clone job the max has already been taken when processing the
-    ;; original file.
-    (unless (or (eq dep-time 'just-compiled) (eq (get job 'type) 'clone))
+    ;; original file. If coqdep failed, 'obj-mod-time is not set.
+    (unless (or (eq dep-time 'just-compiled) (eq (get job 'type) 'clone)
+		(get job 'failed))
       (setq dep-time (get job 'obj-mod-time)))
     (put job 'youngest-coqc-dependency dep-time)
     (when coq--debug-auto-compilation
@@ -1259,12 +1356,29 @@ This function makes the following actions.
 	       (if (eq dep-time 'just-compiled)
 		   'just-compiled
 		 (current-time-string dep-time))))
-    (put job 'state 'waiting-queue)
     (dolist (dependant (get job 'coqc-dependants))
-      (coq-par-decrease-coqc-dependency dependant dep-time ancestors))
+      (coq-par-decrease-coqc-dependency dependant dep-time ancestors)
+      (unless (get dependant 'failed)
+	(setq dependant-alive t)))
     (when coq--debug-auto-compilation
-      (message "%s: coqc kickoff finished, maybe kickoff queue"
-	       (get job 'name)))
+      (message (concat "%s: coqc kickoff finished, %s dependant alive, "
+		       "maybe kickoff queue")
+	       (get job 'name)
+	       (if dependant-alive "some" "no")))
+    (assert (or (not (get job 'failed)) (not dependant-alive))
+	    nil "failed job with non-failing dependant")
+    (when (or (and (not dependant-alive)
+		   (not (get job 'require-span))
+		   (not (get job 'failed)))
+	      (and (get job 'queue-failed) (not (get job 'failed))))
+      ;; job has not failed, but all dependants have 'failed set, or
+      ;; top-level job marked with 'queue-failed changes to 'failed
+      (when (get job 'queue-failed)
+	(when coq--debug-auto-compilation
+	  (message "%s: queue-failed -> failed, unlock ancestors"
+		   (get job 'name)))
+	(put job 'failed t))
+      (coq-par-unlock-job-ancestors-on-error job))
     (coq-par-kickoff-queue-maybe job)))
 
 (defun coq-par-start-coqdep (job)
@@ -1428,20 +1542,115 @@ This function returns the newly created job."
       (coq-par-start-or-enqueue new-job))
     new-job))
 
+(defun coq-par-ongoing-compilation (job)
+  "Determine if the source file for JOB needs to stay looked.
+Return t if job has a direct or indirect dependant that has not
+failed yet and that is in a state before 'waiting-queue. Also,
+return t if JOB has a dependant that is a top-level job which has
+not yet failed."
+  (assert (not (eq (get job 'lock-state) 'asserted))
+	  nil "coq-par-ongoing-compilation precondition failed")
+  (cond
+   ((get job 'failed)
+    nil)
+   ((or (eq (get job 'state) 'waiting-dep)
+	(eq (get job 'state) 'enqueued-coqc)
+	;; top-level job that has compilation finished but has not
+	;; been asserted yet
+	(and (eq (get job 'state) 'waiting-queue) (get job 'require-span))
+	;; Note that job cannot be a top-level in state 'ready,
+	;; because we started from job with 'lock-state property equal
+	;; to 'locked. Top-level job in state 'ready have all
+	;; dependees with 'lock-state equal to 'asserted.
+	)
+    t)
+   ;; Note that non-top-level jobs switch to 'waiting-queue as soon as
+   ;; all dependencies are ready, before they start to deal with the
+   ;; ancestors. We might therefore see here non-top-level jobs in
+   ;; state 'waiting-queue: they have successfully finished their
+   ;; compilation and are about to go to state 'ready.
+   ((or (eq (get job 'state) 'ready)
+	(eq (get job 'state) 'waiting-queue))
+    ;; internal ready job
+    (let ((dependants (get job 'coqc-dependants))
+	  (res nil)
+	  dep)
+      (while (and (not res) (setq dep (pop dependants)))
+	(setq res (coq-par-ongoing-compilation dep)))
+      res))
+   (t
+    (assert nil nil
+	    "impossible ancestor state %s on job %s"
+	    (get job 'state) (get job 'name)))))
+
+(defun coq-par-unlock-job-ancestors-on-error (job)
+  "Unlock those ancestors of JOB that need to be unlocked.
+For a failing job JOB, an ancestor need to stay looked if there
+is still some compilation going on for which this ancestor is a
+dependee or if a top level job with JOB as ancestor has finished
+it's compilation successfully. In all other cases the ancestor
+must be unlocked."
+  (dolist (anc-job (get job 'ancestors))
+    (when (and (eq (get anc-job 'lock-state) 'locked)
+	       (not (coq-par-ongoing-compilation anc-job)))
+      (when coq--debug-auto-compilation
+	(message "%s: %s unlock because no ongoing compilation"
+		 (get anc-job 'name) (get anc-job 'src-file)))
+      (coq-unlock-ancestor (get anc-job 'src-file))
+      (put anc-job 'lock-state 'unlocked))))
+
+(defun coq-par-mark-queue-failing (job)
+  "Mark JOB with 'queue-failed.
+Mark JOB with 'queue-failed, and, if JOB is in state
+'waiting-queue, transition to 'failed and unlock ancestors as
+appropriate."
+  (unless (or (get job 'failed) (get job 'queue-failed))
+    (put job 'queue-failed t)
+    (assert (not (eq (get job 'state) 'ready))
+	    nil "coq-par-mark-queue-failing impossible state")
+    (when coq--debug-auto-compilation
+      (message "%s: mark as queue-failed, %s"
+	       (get job 'name)
+	       (if (eq (get job 'state) 'waiting-queue)
+		   "failed, and unlock ancestors"
+		 "wait")))
+    (when (eq (get job 'state) 'waiting-queue)
+      (put job 'failed t)
+      (coq-par-unlock-job-ancestors-on-error job))
+    (when (get job 'queue-dependant)
+      (coq-par-mark-queue-failing (get job 'queue-dependant)))))
+
+(defun coq-par-mark-job-failing (job)
+  "Mark all dependants of JOB as failing and unlock ancestors as appropriate.
+Set the 'failed property on all direct and indirect dependants of
+JOB. Along the way, unlock ancestors as determined by
+`coq-par-ongoing-compilation'. Mark queue dependants with
+'queue-failed."
+  (unless (get job 'failed)
+    (put job 'failed t)
+    (when coq--debug-auto-compilation
+      (message "%s: mark as failed and unlock free ancestors" (get job 'name)))
+    (coq-par-unlock-job-ancestors-on-error job)
+    (dolist (dependant (get job 'coqc-dependants))
+      (coq-par-mark-job-failing dependant))
+    (when (get job 'queue-dependant)
+      (coq-par-mark-queue-failing (get job 'queue-dependant)))))
+
 (defun coq-par-process-coqdep-result (process exit-status)
   "Coqdep continuation function: Process coqdep output.
-This function analyses the coqdep output of PROCESS and signals
-an error if necessary. If there was no coqdep error, the
-following actions are taken.
+This function analyses the coqdep output of PROCESS. In case of
+error, the job is marked as failed or compilation is aborted via
+a signal (depending on `coq-compile-keep-going'). If there was no
+coqdep error, the following actions are taken.
 - the job that started PROCESS is put into sate 'waiting-dep
 - a new job is created for every dependency. If this new job is
   not immediately ready, a Coq dependency is registered from the
   new job to the current job. For dependencies that are 'ready
   already, the most recent ancestor modification time is
   propagated.
-- if there are no dependencies or all dependencies are ready
-  already, the next transition to 'enqueued-coqc is triggered for
-  the current job
+- if there are no dependencies (especially if coqdep failed) or
+  all dependencies are ready already, the next transition to
+  'enqueued-coqc is triggered for the current job
 - otherwise the current job is left alone until somebody
   decreases its dependency count to 0
 
@@ -1455,13 +1664,14 @@ is directly passed to `coq-par-analyse-coq-dep-exit'."
 	  (process-get process 'coq-process-command)))
 	job-max-time)
     (if (stringp dependencies-or-error)
-	(signal 'coq-compile-error-coqdep (get job 'src-file))
+	(if coq-compile-keep-going
+	    (coq-par-mark-job-failing job)
+	  (signal 'coq-compile-error-coqdep (get job 'src-file)))
 
       ;; no coqdep error -- work on dependencies
       (when 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))
       (dolist (dep-vo-file dependencies-or-error)
 	(unless (coq-compile-ignore-file dep-vo-file)
@@ -1474,34 +1684,45 @@ is directly passed to `coq-par-analyse-coq-dep-exit'."
 	      (setq job-max-time dep-time))
 	    (unless (coq-par-job-coqc-finished dep-job)
 	      (coq-par-add-coqc-dependency dep-job job)))))
-      (put job 'youngest-coqc-dependency job-max-time)
-      (if (coq-par-dependencies-ready job)
-	  (progn
-	    (when coq--debug-auto-compilation
-	      (message "%s: coqc dependencies finished" (get job 'name)))
-	    (coq-par-compile-job-maybe job))
-	(when coq--debug-auto-compilation
-	  (message "%s: wait for %d dependencies"
-		   (get job 'name) (get job 'coqc-dependency-count)))))))
+      (put job 'youngest-coqc-dependency job-max-time))
+    ;; common part for job where coqdep was successful and where
+    ;; coqdep failed (when coq-compile-keep-going)
+    (put job 'state 'waiting-dep)
+    (if (coq-par-dependencies-ready job)
+	(progn
+	  (when coq--debug-auto-compilation
+	    (message "%s: coqc dependencies finished" (get job 'name)))
+	  (coq-par-compile-job-maybe job))
+      (when coq--debug-auto-compilation
+	(message "%s: wait for %d dependencies"
+		 (get job 'name) (get job 'coqc-dependency-count))))))
 
 (defun coq-par-coqc-continuation (process exit-status)
   "Coqc continuation function.
-Signal an error, if coqc failed. Otherwise, trigger the
-transition 'enqueued-coqc -> 'waiting-queue for the job behind
-PROCESS."
-  (if (eq exit-status 0)
-      (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-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))))
+If coqc failed, signal an error or mark the job as 'failed, and
+unlock ancestors as appropriate. If coqc was successful, trigger
+the transition 'enqueued-coqc -> 'waiting-queue for the job
+behind PROCESS."
+  (let ((job (process-get process 'coq-compilation-job)))
+    (if (eq exit-status 0)
+	(progn
+	  ;; coqc success
+	  (when (get job 'vio2vo-needed)
+	    (coq-par-vio2vo-enqueue job))
+	  (coq-par-kickoff-coqc-dependants job 'just-compiled))
+      ;; coqc error
+      (coq-compile-display-error
+       (mapconcat 'identity (process-get process 'coq-process-command) " ")
+       (process-get process 'coq-process-output)
+       t)
+      (if coq-compile-keep-going
+	  (progn
+	    (coq-par-mark-job-failing job)
+	    (coq-par-kickoff-coqc-dependants
+	     job
+	     (get job 'youngest-coqc-dependency)))
+	(signal 'coq-compile-error-coqc
+		(get (process-get process 'coq-compilation-job) 'src-file))))))
 
 (defun coq-par-vio2vo-continuation (process exit-status)
   "vio2vo continuation function."
@@ -1690,9 +1911,8 @@ the maximal number of background compilation jobs is started."
 	(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)))
+      (dolist (require-items (cdr splitted-items))
+	(coq-par-handle-require-list require-items)))
     (when coq--last-compilation-job
       (setq proof-second-action-list-active t))
     (coq-par-start-jobs-until-full)
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 6c0492aa..d9458eb8 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -88,9 +88,11 @@ See the functions `proof-start-queue' and `proof-shell-exec-loop'.")
 
 (defsubst proof-shell-invoke-callback (listitem)
   "From `proof-action-list' LISTITEM, invoke the callback on the span."
-  (condition-case nil
+  (condition-case err
       (funcall (nth 2 listitem) (car listitem))
-    (error nil)))
+    (error
+     (message "error escaping proof-shell-invoke-callback: %s" err)
+     nil)))
 
 (defvar proof-second-action-list-active nil
   "Signals that some items are waiting outside of `proof-action-list'.