From b0553954a4324efd873f7caae85f0ebc0665883c Mon Sep 17 00:00:00 2001
From: Hendrik Tews <hendrik@askra.de>
Date: Thu, 15 Dec 2016 09:39:00 +0100
Subject: die gracefully when visiting files in nonexisting directories

---
 coq/coq-compile-common.el | 37 ++++++++-----------------------------
 coq/coq-par-compile.el    |  3 +++
 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))
-- 
cgit v1.2.3