diff --git a/CHANGES b/CHANGES index 63500e7be..e3f4f5985 100644 --- a/CHANGES +++ b/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 diff --git a/ci/simple-tests/coq-test-coqproject-args.el b/ci/simple-tests/coq-test-coqproject-args.el new file mode 100644 index 000000000..b67e27cf3 --- /dev/null +++ b/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 diff --git a/ci/simple-tests/coq-test-par-job-needs-compilation-quick.el b/ci/simple-tests/coq-test-par-job-needs-compilation-quick.el index 9a4a7b9c2..a9fce9ddc 100644 --- a/ci/simple-tests/coq-test-par-job-needs-compilation-quick.el +++ b/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)) diff --git a/coq/coq-system.el b/coq/coq-system.el index e9b3acd7f..2a929a6a3 100644 --- a/coq/coq-system.el +++ b/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) diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 5c26bf413..9048dd76b 100644 --- a/doc/ProofGeneral.texi +++ b/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