diff options
| -rw-r--r-- | coq/coq-compile-common.el | 37 | ||||
| -rw-r--r-- | coq/coq-par-compile.el | 3 | ||||
| -rw-r--r-- | coq/coq-system.el | 16 |
3 files changed, 22 insertions, 34 deletions
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index 92614e7a..af3e70a4 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -420,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") @@ -518,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 diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el index efbb2d3c..6378f573 100644 --- a/coq/coq-par-compile.el +++ b/coq/coq-par-compile.el @@ -1967,6 +1967,9 @@ does the error checking/reporting for "Proof General; please customize coq-pinned-version")) (message "%s \"%s\"; consider customizing coq-pinned-version" (get (car err) 'error-message) (cdr err)))) + (file-error + (coq-par-emergency-cleanup) + (message "Error: %s" (mapconcat 'identity (cdr err) ": "))) (error (message "unexpected error during parallel compilation: %s" err) diff --git a/coq/coq-system.el b/coq/coq-system.el index 48757be5..88ce06be 100644 --- a/coq/coq-system.el +++ b/coq/coq-system.el @@ -57,10 +57,12 @@ See also `coq-prog-env' to adjust the environment." :group 'coq) (defun get-coq-library-directory () - (let ((c (substring (shell-command-to-string (concat coq-prog-name " -where")) 0 -1 ))) - (if (string-match "not found" c) - "/usr/local/lib/coq" - c))) + (let ((default-directory + (if (file-accessible-directory-p default-directory) + default-directory + "/"))) + (or (ignore-errors (car (process-lines coq-prog-name "-where"))) + "/usr/local/lib/coq"))) (defconst coq-library-directory (get-coq-library-directory) ;; FIXME Should be refreshed more often "The coq library directory, as reported by \"coqtop -where\".") @@ -123,7 +125,11 @@ Interactively (with INTERACTIVE-P), show that number." ;; Use `shell-command' via `find-file-name-handler' instead of ;; `process-line': when the buffer is running TRAMP, PG uses ;; `start-file-process', loading the binary from the remote server. - (let* ((coq-command (shell-quote-argument (or coq-prog-name "coqtop"))) + (let* ((default-directory + (if (file-accessible-directory-p default-directory) + default-directory + "/")) + (coq-command (shell-quote-argument (or coq-prog-name "coqtop"))) (shell-command-str (format "%s -v" coq-command)) (fh (find-file-name-handler default-directory 'shell-command)) (retv (if fh (funcall fh 'shell-command shell-command-str (current-buffer)) |