Adjust _RocqProject parsing to rocq makefile changes

CHANGES

@@ -26,6 +26,10 @@ the Git ChangeLog, the GitHub repo https://github.com/ProofGeneral/PG
     reduce splash screen time to make it less annoying
 
 ** Coq changes
+*** Align _CoqProject/_RocqProject parsing with rocq makefile (fixing
+    #113, #392 and #589). There is no escape character any more, in any
+    argument: write -arg "-w 'a b'" instead of -arg "-w \"a b\"", and
+    -R "C:\dev\lib" Top instead of -R "C:\\dev\\lib" Top.
 *** support Coq 8.19
 **** New option coq-compile-coqdep-warnings to configure the warning
      command line argument (-w) of coqdep. The default of this option

ci/simple-tests/coq-test-coqproject-args.el

@@ -0,0 +1,74 @@
+;;; coq-test-coqproject-args.el --- Test _RocqProject parsing -*- lexical-binding: t; -*-
+;;
+;; This file is part of Proof General.
+;;
+;; SPDX-License-Identifier: GPL-3.0-or-later
+
+;;; Code:
+
+(require 'proof-site)
+(proof-ready-for-assistant 'coq)
+(require 'coq-system)
+(require 'ert)
+
+(defconst coq-test-project-file-args
+  '(("-arg -w\n-arg -foo"                            ("-w" "-foo"))
+    ("-arg -w -arg -foo -arg -bar"                   ("-w" "-foo" "-bar"))
+    ("-arg\t-w\n-arg\t-foo"                          ("-w" "-foo"))
+    ("-arg\r-w\r-arg\r-foo"                          ("-w" "-foo"))
+    ("-arg \"-w all\""                               ("-w" "all"))
+    ("-arg \"-w -notation-overriden\""               ("-w" "-notation-overriden"))
+    ("-arg \"-w -a,-b\""                             ("-w" "-a,-b"))
+    ("-arg \"-w -a\"\n-arg -w -arg -b"               ("-w" "-a" "-w" "-b"))
+    ("-arg \"-w '-a -b'\""                           ("-w" "-a -b"))
+    ("-arg \"-set 'Default Goal Selector=!'\""       ("-set" "Default Goal Selector=!"))
+    ("-arg -set\n-arg \"'Default Goal Selector=!'\"" ("-set" "Default Goal Selector=!"))
+    ("-arg \"'a b'\""                                ("a b"))
+    ("-arg \"'a b' c\""                              ("a b" "c"))
+    ("-arg \"c 'a b'\""                              ("c" "a b"))
+    ("-arg \"'a b' 'c d'\""                          ("a b" "c d"))
+    ("-arg \"'a' 'b'\""                              ("a" "b"))
+    ("-arg \"a'b c'd\""                              ("ab cd"))
+    ("-arg \"-Q '' Foo\""                            ("-Q" "" "Foo"))
+    ("-arg \"''\""                                   (""))
+    ("-arg \"\""                                     nil)
+    ("-arg \"   \""                                  nil)
+    ("-arg \"-w\tall\""                              ("-w\tall"))
+    ("-arg \"a\\\\b\"\n-arg -w"                      ("a\\\\b" "-w"))
+    ("# why\n-arg -w"                                ("-w"))
+    ("-arg \"-w all\" # why"                         ("-w" "all"))
+    ("-arg -w#why\n-arg -foo"                        ("-w" "-foo"))
+    ("# an unbalanced \" is just text\n-arg -w"      ("-w"))
+    ("# a carriage return does not end a comment\r-arg -w" nil)
+    ("-arg \"-w #foo\""                              ("-w" "#foo"))))
+
+(ert-deftest coq-project-file-prog-args ()
+  (dolist (case coq-test-project-file-args)
+    (pcase-let ((`(,contents ,expected) case))
+      (should (equal (cons contents (coq--extract-prog-args
+                                     (coq--read-options-from-project-file contents)))
+                     (cons contents expected))))))
+
+(ert-deftest coq-project-file-unpaired-quote ()
+  (dolist (contents '("-arg \"'\""
+                      "-arg \"a 'b c' d 'e\""
+                      "-arg \"-w 'all\""
+                      "-arg 'val -arg val'"))
+    (should-error (coq--extract-prog-args
+                   (coq--read-options-from-project-file contents)))))
+
+(ert-deftest coq-project-file-unterminated-string ()
+  (should-error (coq--read-options-from-project-file "-arg \"-w all\n-arg -foo")))
+
+(ert-deftest coq-project-file-load-path ()
+  (should (equal (coq--extract-load-path
+                  (coq--read-options-from-project-file
+                   "# not a -R\n-R theories Top\n-Q \"my dir\" \"\"\n-I src")
+                  "/p/")
+                 '((rec "/p/theories" "Top")
+                   (recnoimport "/p/my dir" "")
+                   (ocamlimport "/p/src")))))
+
+(provide 'coq-test-coqproject-args)
+
+;;; coq-test-coqproject-args.el ends here

ci/simple-tests/coq-test-par-job-needs-compilation-quick.el

@@ -783,6 +783,11 @@ relative ages.")
 	  (cdr test))))
    coq--par-job-needs-compilation-tests))
 
+(defconst test-coq-par-time-step 1.5
+  "Seconds between the time stamps of two successive groups of test files.
+Fractional to also compare sub-second parts, above 1 to stay ordered on
+file systems with whole-second time stamps.")
+
 (defun test-coq-par-sym-to-file (dir sym)
   "Convert a test file symbol SYM to a file name in directory DIR."
   (let ((file (cond
@@ -807,13 +812,11 @@ test the result and side effects with `assert'."
 	(compilation-result (nth 1 variant))
 	(delete-result (nth 2 variant))
 	(req-obj-result (nth 3 variant))
-	(different-counter 5)
-	(same-counter 5)
-	(different-not-ok t)
-	(same-not-ok t)
-	(last-different-time-stamp '(0 0))
 	(file-descr-flattened (coq-par-test-flatten-files file-descr))
-	same-time-stamp file-list
+	(time-stamp (time-subtract (current-time)
+				   (seconds-to-time
+				    (* test-coq-par-time-step
+				       (length file-descr)))))
 	obj-mod-result result)
     (message "test case %d/576: %s %s just-compiled: %s"
              counter (car variant) file-descr dep-just-compiled)
@@ -828,50 +831,18 @@ test the result and side effects with `assert'."
     (put job 'youngest-coqc-dependency '(0 0))
     (put job 'name id)
     ;; create files in order
-    (while different-not-ok
-      ;; (message "enter different loop %s at %s"
-      ;; 	       different-counter (current-time))
-      (setq different-not-ok nil)
-      (setq different-counter (1- different-counter))
-      (cl-assert (> different-counter 0)
-	      nil "create files with different time stamps failed")
-      (dolist (same-descr file-descr)
-	(when (symbolp same-descr)
-	  (setq same-descr (list same-descr)))
-	(setq file-list
-	      (mapcar (lambda (sym) (test-coq-par-sym-to-file dir sym))
-		      same-descr))
-	;; (message "try %s files %s" same-descr file-list)
-	(setq same-counter 8)
-	(setq same-not-ok t)
-	(while same-not-ok
-	  (setq same-counter (1- same-counter))
-	  (cl-assert (> same-counter 0)
-		  nil "create files with same time stamp failed")
-	  (dolist (file file-list)
-	    (with-temp-file file t))
-	  ;; check now that all the files in file-list have the same time stamp
-	  (setq same-not-ok nil)
-	  (setq same-time-stamp (nth 5 (file-attributes (car file-list))))
-	  ;; (message "got first time stamp %s" same-time-stamp)
-	  (dolist (file (cdr file-list))
-	    (let ((ots (nth 5 (file-attributes file))))
-	      ;; (message "got other time stamp %s" ots)
-	      (unless (equal same-time-stamp ots)
-		(setq same-not-ok t)))))
-	;; (message "successful finished %s" same-descr)
-	(when (member 'dep same-descr)
-	  (put job 'youngest-coqc-dependency
-	       (nth 5 (file-attributes (test-coq-par-sym-to-file dir 'dep)))))
-	;; (message "XX %s < %s = %s"
-	;; 	 last-different-time-stamp same-time-stamp
-	;; 	 (time-less-p last-different-time-stamp same-time-stamp))
-	(unless (time-less-p last-different-time-stamp same-time-stamp)
-	  ;; error - got the same time stamp
-	  ;; (message "unsuccsessful - need different retry")
-	  (setq different-not-ok t))
-	(setq last-different-time-stamp same-time-stamp)
-	(sleep-for 0 15)))
+    (dolist (same-descr file-descr)
+      (when (symbolp same-descr)
+	(setq same-descr (list same-descr)))
+      (dolist (sym same-descr)
+	(let ((file (test-coq-par-sym-to-file dir sym)))
+	  (with-temp-file file t)
+	  (should (set-file-times file time-stamp))))
+      (when (member 'dep same-descr)
+	(put job 'youngest-coqc-dependency
+	     (nth 5 (file-attributes (test-coq-par-sym-to-file dir 'dep)))))
+      (setq time-stamp
+	    (time-add time-stamp (seconds-to-time test-coq-par-time-step))))
     (when dep-just-compiled
       (put job 'youngest-coqc-dependency 'just-compiled))
     (setq result (coq-par-job-needs-compilation-quick job))

coq/coq-system.el

@@ -23,6 +23,7 @@
 
 ;;; Code:
 
+(require 'cl-lib)
 (require 'proof)
 (require 'coq-mode)                     ;for coq-prog-name
 
@@ -653,7 +654,37 @@ ALREADYOPEN is t if buffer already existed."
 				  (find-file-noselect projectfile t t))))
 	  (list projectbuffer projectbufferalreadyopen))))))
 
-(defconst coq--project-file-separator "[\r\t\n[:space:]]+")
+;; The syntax of project files is that of `rocq makefile'; see "The grammar of
+;; _RocqProject" in the Rocq reference manual and lib/coqProject_file.ml.
+
+(defconst coq--project-file-token-regexp
+  "[ \t\n\r]+\\|#.*$\\|\"\\(?1:[^\"]*\\)\"\\|\\(?1:[^ \t\n\r#\"][^ \t\n\r#]*\\)\\|\\(?2:\"\\)"
+  "Regexp matching one blank, comment or token of a project file.
+Group 1 holds the token, group 2 an unterminated string.")
+
+(defconst coq--arg-value-token-regexp "\\(?:[^ ']+\\|'[^']*'?\\)+"
+  "Regexp matching one argument, quotes included, in a -arg value.")
+
+(defun coq--project-file-tokenize (contents)
+  "Split CONTENTS of a project file into tokens.
+A double quote at the start of a token protects blanks and \"#\" up to
+the next double quote; there is no escape character."
+  (let ((pos 0) (tokens nil))
+    (while (string-match coq--project-file-token-regexp contents pos)
+      (setq pos (match-end 0))
+      (when (match-beginning 2) (error "Unterminated string in project file"))
+      (when (match-beginning 1) (push (match-string 1 contents) tokens)))
+    (nreverse tokens)))
+
+(defun coq--split-arg-value (value)
+  "Split VALUE, the argument of a -arg option, into coqtop arguments."
+  (when (cl-oddp (cl-count ?' value))
+    (error "Unpaired single quote in -arg value: %S" value))
+  (let ((pos 0) (args nil))
+    (while (string-match coq--arg-value-token-regexp value pos)
+      (setq pos (match-end 0))
+      (push (replace-regexp-in-string "'" "" (match-string 0 value) t t) args))
+    (nreverse args)))
 
 (defconst coq--makefile-switch-arities
   '(("-R" . 2)
@@ -678,7 +709,7 @@ If ARITY is nil, return SWITCH."
 (defun coq--read-options-from-project-file (contents)
   "Read options from CONTENTS of _CoqProject.
 Returns a mixed list of option-value pairs and strings."
-  (let ((raw-args (split-string-and-unquote contents coq--project-file-separator))
+  (let ((raw-args (coq--project-file-tokenize contents))
         (options nil))
     (while raw-args
       (let* ((switch (pop raw-args))
@@ -699,11 +730,7 @@ coqtop.  But -arg \"\\='a b\\='\" means to pass a and b together."
         ((or "-byte" "-op")
          (push opt args))
         (`("-arg" ,concatenated-args)
-	 (if (and (string-prefix-p "'" concatenated-args) (string-suffix-p "'" concatenated-args))
-	     (setq args (append args (list (substring concatenated-args 1 -1))))
-           (setq args
-		 (append args
-			 (split-string-and-unquote concatenated-args coq--project-file-separator)))))))
+         (setq args (append args (coq--split-arg-value concatenated-args))))))
     args))
 
 (defun coq--extract-load-path-1 (option base-directory)

doc/ProofGeneral.texi

@@ -4473,9 +4473,13 @@ Detail}. For the example above, Proof General will start
 @code{coqtop -emacs -foo3 -R foo bar -I foo2} (remark:
 @code{-emacs} is always added to the options).
 
-@emph{NOTE:} @code{-arg} must be followed by one and only one option
-to pass to coqtop/coqc, use several @code{-arg} to issue several
-options. One per line (limitation of Proof General).
+@emph{NOTE:} @code{-arg} must be followed by exactly one token, which may
+denote several options: it is split on spaces, unless single quotes
+prevent it, and the quotes are then removed. So @code{-arg "-set 'Default
+Goal Selector=!'"} passes @code{-set} and @code{Default Goal Selector=!}.
+There is no escape character. See Rocq Documentation, section
+@coqrefman{practical-tools/utilities.html#quoting-arguments-to-rocq-c,
+Quoting arguments to rocq c}.
 
 For backward compatibility, one can also configure the load path
 with the option @code{coq-load-path}, but this is not compatible