diff options
Diffstat (limited to 'coq/coq-compile-common.el')
| -rw-r--r-- | coq/coq-compile-common.el | 67 |
1 files changed, 34 insertions, 33 deletions
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index 1f31c1d3..af3e70a4 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -234,6 +234,9 @@ quick-and-vio2vo Same as `quick-no-vio2vo', but start vio2vo processes 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'. + When `coq-compile-keep-going' is set, vio2vo compilation + is scheduled for those files for which coqc compilation + was successful. Warning: This mode does only work when you process require commands in batches. Slowly single-stepping through require's @@ -261,6 +264,19 @@ 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, background compilation is +immediately stopped after the first error. + +This option can be set/reset via menu +`Coq -> Auto Compilation -> Keep going'.") + +;; 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 @@ -404,18 +420,6 @@ or not." :safe (lambda (v) (every 'stringp v)) :group 'coq-auto-compile) -(defcustom coq-compile-ignore-library-directory t - "If non-nil, ProofGeneral does not compile modules from the coq library. -Should be `t' for normal coq users. If `nil' library modules are -compiled if their sources are newer. - -This option has currently no effect, because Proof General uses -coqdep to translate qualified identifiers into library file names -and coqdep does not output dependencies in the standard library." - :type 'boolean - :safe 'booleanp - :group 'coq-auto-compile) - (defcustom coq-coqdep-error-regexp (concat "^\\*\\*\\* Warning: in file .*, library .* is required " "and has not been found") @@ -502,23 +506,14 @@ for instance, not make sense to let ProofGeneral check if the coq standard library is up-to-date. This function is always invoked on the .vo file name, regardless whether the file would be compiled with ``-quick'' or not." - (or - (and - coq-compile-ignore-library-directory - (eq (compare-strings coq-library-directory 0 nil - lib-obj-file 0 (length coq-library-directory)) - t) - (when coq--debug-auto-compilation - (message "Ignore lib file %s" lib-obj-file)) - t) - (if (some - (lambda (dir-regexp) (string-match dir-regexp lib-obj-file)) - coq-compile-ignored-directories) - (progn - (when coq--debug-auto-compilation - (message "Ignore %s" lib-obj-file)) - t) - nil))) + (if (some + (lambda (dir-regexp) (string-match dir-regexp lib-obj-file)) + coq-compile-ignored-directories) + (progn + (when coq--debug-auto-compilation + (message "Ignore %s" lib-obj-file)) + t) + nil)) ;;; convert .vo files to .v files and module names @@ -544,7 +539,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 +559,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))) |