diff options
-rw-r--r-- | coq/coq-compile-common.el | 8 | ||||
-rw-r--r-- | coq/coq-par-compile.el | 31 |
2 files changed, 31 insertions, 8 deletions
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index 3522a8f0..57581af3 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -275,6 +275,14 @@ percentage of `coq-max-background-compilation-jobs'." :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 diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el index dab1cf42..00ddedbc 100644 --- a/coq/coq-par-compile.el +++ b/coq/coq-par-compile.el @@ -318,6 +318,9 @@ Used to link top-level jobs with queue dependencies.") (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.") @@ -416,7 +419,6 @@ queue.") ;;; vio2vo queue -;; (defvar coq-par-vio2vo-queue (coq-par-new-queue) "Queue of jobs that need a vio2vo process. @@ -754,6 +756,8 @@ and resets the internal state." (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) @@ -875,18 +879,28 @@ errors are reported with an error message." ;;; vio2vo compilation -(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." +(defun coq-par-run-vio2vo-queue () + "Start delayed vio2vo compilation." (assert (not coq-last-compilation-job) - nil "normal compilation and vio2vo in parallel 1") + 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 (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 @@ -1697,12 +1711,13 @@ the maximal number of background compilation jobs is started." ;; 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-par-vio2vo-queue (coq-par-new-queue)) (setq coq-compile-vio2vo-in-progress nil)) ;; save buffers before invoking the first coqdep (coq-compile-save-some-buffers) |