coq-compile-before-require should allow non-source installations

[coquser]

The attached patch makes coq-compile-before-require accept modules which have been installed (for example, system-wide) that do not offer source files. In effect, it will simply ignore whatever dependencies those module might have.

[coquser]

I'm unable to attach files, so here is the literal diff:

--- coq/coq-seq-compile.el	13 Nov 2012 22:05:11 -0000	11.12
+++ coq/coq-seq-compile.el	11 Oct 2014 21:09:46 -0000
@@ -87,9 +87,12 @@
     (if coq-debug-auto-compilation
         (message "coqdep status %s, output on %s: %s"
                  coqdep-status lib-src-file coqdep-output))
-    (if (or
-         (not (eq coqdep-status 0))
-         (string-match coq-coqdep-error-regexp coqdep-output))
+    (if (string-match coq-coqdep-error-regexp coqdep-output)
+        ()
+      (if (eq coqdep-status 0)
+          (if (string-match ": \\(.*\\)$" coqdep-output)
+              (cdr-safe (split-string (match-string 1 coqdep-output)))
+            ())
         (let* ((this-command (cons coq-dependency-analyzer coqdep-arguments))
                (full-command (if command-intro
                                  (cons command-intro this-command)
@@ -101,10 +104,7 @@
             (with-current-buffer coq-compile-response-buffer
               (insert coqdep-output)))
           (coq-display-compile-response-buffer)
-          "unsatisfied dependencies")
-      (if (string-match ": \\(.*\\)$" coqdep-output)
-          (cdr-safe (split-string (match-string 1 coqdep-output)))
-        ()))))
+          "unsatisfied dependencies")))))

 (defun coq-seq-compile-library (src-file)
   "Recompile coq library SRC-FILE.

[courtieu]

Hi thanks for submitting.

Can you provide an example of the problem please? I can't reproduce the initial problem.

I tried the following:

I put one .v file in a lib directory and two others in a foo directory, together with a _CoqProject file for compiling in foo.

---

/tmp/pgtestcompile$ ls *

foo: _CoqProject main2.v main.v

lib: other.v

/tmp/pgtestcompile$ more lib/other.v

Definition y:nat := 0.

/tmp/pgtestcompile$ more foo/main.v

Require Import lib.other. Definition x := lib.other.y.

/tmp/pgtestcompile$ more foo/main2.v

Require Import foo.main.

/tmp/pgtestcompile/foo$ more foo/_CoqProject

-R /home/courtieu/tmp/pgtestcompile/lib lib -R . foo main.v main2.v

/tmp/pgtestcompile$ cd lib

/tmp/pgtestcompile/lib$ coqc -R . lib other.v

/tmp/pgtestcompile/lib$ rm other.v

/tmp/pgtestcompile/lib$ cd ../foo

/tmp/pgtestcompile/foo$ emacs main2.v

---

then pg succeeds in Recompiling main.v succeeds, without complaining about missing other.v.