coq auto-compile and spaces in directory names lead to failure

[coquser]

Proof general in emacs and with coq-compile-before-require set to t does not work when trying to import modules from directories with spaces in names and where those modules have not yet been compiled.

To reproduce create a directory with a space in the name, like "foo bar" with, say two files, Test.v and Test2.v and try to Require Import Test. in the files Test2. The command fails with

Assertion failed: (<= (length result) 1), 2

I have traced the problem to the function coq-seq-get-library-dependencies in coq-seq-compile. The problem is at the end in

(if (string-match ": \\(.*\\)$" coqdep-output)
          (cdr-safe (split-string (match-string 1 coqdep-output)))
        ())

at least in my case. The output of coqdep correctly has spaces in names escaped, but split-string doesn't care and just splits the filename at each space and then the assertion mentioned above fails in the function coq-seq-map-module-id-to-obj-file.

I have fixed it in my case by replacing the offending if statement with

(if (string-match ": \\(.*\\)$" coqdep-output)
          (mapcar (lambda (x)
                    (replace-regexp-in-string "\\\\ " " " x))
                  (cdr-safe (split-string (match-string 1 coqdep-output) "\\($\\|[^\\]\\) ")))
        ())

but I don't know whether this breaks something else. The outer mapcar is there to "unescape" the spaces since emacs functions do not expect escaped spaces in filenames.