From 687e008bc80ca6f66ca8920296c2e8dab889c752 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Thu, 8 Dec 2016 16:06:17 +0100 Subject: 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. --- generic/proof-shell.el | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'generic') 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'. -- cgit v1.2.3 From 93a0d1ca16fd30e89e312932008106bc5503386f Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Mon, 12 Dec 2016 10:05:00 +0100 Subject: fix generic interrupt procedure to interrupt parallel background compilation --- coq/coq-abbrev.el | 7 ++++++- coq/coq-par-compile.el | 45 +++++++++++++++++++++++++++------------------ doc/ProofGeneral.texi | 13 +++++++++++-- generic/proof-config.el | 7 ++++++- generic/proof-shell.el | 22 ++++++++++++++-------- 5 files changed, 64 insertions(+), 30 deletions(-) (limited to 'generic') diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index ec8d5e80..87f61df6 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -203,7 +203,12 @@ It was constructed with `proof-defstringset-fn'.") :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'."]) + :help "Confirm external compilation command, see `coq-compile-command'."] + ["Abort Background Compilation" + coq-par-emergency-cleanup + :active (and coq-compile-before-require + coq-compile-parallel-in-background) + :help "Abort background compilation and kill all compilation processes."]) "" ["Print..." coq-Print :help "With prefix arg (C-u): Set Printing All first"] ["Check..." coq-Check :help "With prefix arg (C-u): Set Printing All first"] diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el index d5b84d46..efbb2d3c 100644 --- a/coq/coq-par-compile.el +++ b/coq/coq-par-compile.el @@ -717,7 +717,8 @@ function returns () if MODULE-ID comes from the standard library." ;;; manage background jobs (defun coq-par-kill-all-processes () - "Kill all background coqc, coqdep or vio2vo compilation processes." + "Kill all background coqc, coqdep or vio2vo compilation processes. +Return t if some process was killed." ;; need to first mark processes as killed, because delete process ;; starts running sentinels in the order processes terminated, so ;; after the first delete-process we see sentinentels of non-killed @@ -741,7 +742,8 @@ function returns () if MODULE-ID comes from the standard library." (get (process-get process 'coq-compilation-job) 'name) (process-name process))))) (process-list)) - (setq coq--current-background-jobs 0))) + (setq coq--current-background-jobs 0) + kill-needed)) (defun coq-par-unlock-all-ancestors-on-error () "Unlock ancestors which are not in an asserted span. @@ -758,22 +760,29 @@ Used for unlocking ancestors on compilation errors." "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-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-all-ancestors-on-error) - (proof-release-lock) - (proof-detach-queue) - (setq proof-second-action-list-active nil) - (coq-par-init-compilation-hash)) + (interactive) ; needed for menu + (let (proc-killed was-busy) + (when coq--debug-auto-compilation + (message "emergency cleanup")) + (setq proc-killed (coq-par-kill-all-processes)) + (when (and (boundp 'prover-was-busy) + (or proc-killed coq--last-compilation-job + coq--compile-vio2vo-in-progress + coq--compile-vio2vo-delay-timer)) + (setq prover-was-busy t)) + (setq coq-par-compilation-queue (coq-par-new-queue)) + (setq coq--last-compilation-job nil) + (setq coq-par-vio2vo-queue (coq-par-new-queue)) + (setq coq--compile-vio2vo-in-progress nil) + (when coq--compile-vio2vo-delay-timer + (cancel-timer coq--compile-vio2vo-delay-timer)) + (coq-par-unlock-all-ancestors-on-error) + (when proof-action-list + (setq proof-shell-interrupt-pending t)) + (proof-release-lock) + (proof-detach-queue) + (setq proof-second-action-list-active nil) + (coq-par-init-compilation-hash))) (defun coq-par-process-filter (process output) "Store output from coq background compilation." diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 31594b9d..be29a660 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -4515,6 +4515,12 @@ the number of parallel background jobs and set error. @end itemize +To abort parallel background compilation, use @code{C-c C-c} +(@code{proof-interrupt-process}), the tool bar interrupt icon, +the menu entry @code{Abort Background Compilation} (menu +@code{Coq -> Auto Compilation}) or kill the Coq toplevel via +@code{C-c C-x} (@code{proof-shell-exit}). To abort synchronous +single threaded compilation, simply hit @code{C-g}. @menu @@ -4599,8 +4605,11 @@ 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} equals @code{'all-cpus}). Your Emacs will stay responsive during -compilation. Use @code{C-c C-c} or the tool bar icons for -interrupt or restart to interrupt compilation. +compilation. To abort the background compilation process, use +@code{C-c C-c} (@code{proof-interrupt-process}), the tool bar +interrupt icon, the menu entry @code{Abort Background +Compilation} (menu @code{Coq -> Auto Compilation}) or kill the +Coq toplevel via @code{C-c C-x} (@code{proof-shell-exit}). For the usual case, you have at most `coq-max-background-compilation-jobs' parallel processes diff --git a/generic/proof-config.el b/generic/proof-config.el index b4898a35..8ce53168 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1683,7 +1683,12 @@ tries to interrupt the proof process. It is therefore run earlier than `proof-shell-handle-error-or-interrupt-hook', which runs when the interrupt is acknowledged inside `proof-shell-exec-loop'. -This hook also runs when the proof assistent is killed." +This hook also runs when the proof assistent is killed. + +Hook functions should set the dynamic variable `prover-was-busy' +to t if there might have been a reason to interrupt. Otherwise +the generic interrupt handler might issue a prover-not-busy +error." :type '(repeat function) :group 'proof-shell) diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 7a397a06..51038fa6 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -464,7 +464,9 @@ shell buffer, called by `proof-shell-bail-out' if process exits." (proc (get-buffer-process (current-buffer))) (bufname (buffer-name))) (message "%s, cleaning up and exiting..." bufname) - (run-hooks 'proof-shell-signal-interrupt-hook) + (let (prover-was-busy) + ;; hook functions might set prover-was-busy + (run-hooks 'proof-shell-signal-interrupt-hook)) (redisplay t) (when (and alive proc) @@ -826,14 +828,18 @@ In the first case, PG will terminate the queue of commands at the first available point. In the second case, you may need to press enter inside the prover command buffer (e.g., with Isabelle2009 press RET inside *isabelle*)." (interactive) - (unless (proof-shell-live-buffer) + (let ((prover-was-busy nil)) + (unless (proof-shell-live-buffer) (error "Proof process not started!")) - (unless proof-shell-busy - (error "Proof process not active!")) - (setq proof-shell-interrupt-pending t) - (with-current-buffer proof-shell-buffer - (interrupt-process)) - (run-hooks 'proof-shell-signal-interrupt-hook)) + ;; hook functions might set prover-was-busy + (run-hooks 'proof-shell-signal-interrupt-hook) + (if proof-shell-busy + (progn + (setq proof-shell-interrupt-pending t) + (with-current-buffer proof-shell-buffer + (interrupt-process))) + (unless prover-was-busy + (error "Proof process not active!"))))) -- cgit v1.2.3 From 515026c1a268817075d37f748db303d05b0abb00 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Wed, 28 Dec 2016 13:04:26 +0100 Subject: fix prooftree crash with long evar lines --- generic/proof-tree.el | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'generic') diff --git a/generic/proof-tree.el b/generic/proof-tree.el index 03af645e..77d3cc33 100644 --- a/generic/proof-tree.el +++ b/generic/proof-tree.el @@ -556,7 +556,8 @@ Runs on process status changes and cleans up when prooftree dies." "Start the external prooftree process. Does also initialize the communication channel and some internal variables." - (let ((old-proof-tree (get-process proof-tree-process-name))) + (let ((process-connection-type nil) ; use pipes, see emacs bug #24531 + (old-proof-tree (get-process proof-tree-process-name))) ;; reset output marker (when proof-tree-output-marker (set-marker proof-tree-output-marker nil) -- cgit v1.2.3