branch: elpa/proof-general
commit c9689aea0c0d26c5a41ac24c67cf8181ec950dfc
Author: Pierre Courtieu <pierre.court...@cnam.fr>
Commit: Pierre Courtieu <pierre.court...@cnam.fr>
Adapting compile tests to the rocq cli.
---
ci/compile-tests/010-coqdep-errors/runtest.el | 10 +++++++---
coq/coq-par-compile.el | 12 +++++++++---
coq/coq-system.el | 12 +++++++-----
3 files changed, 23 insertions(+), 11 deletions(-)
diff --git a/ci/compile-tests/010-coqdep-errors/runtest.el
b/ci/compile-tests/010-coqdep-errors/runtest.el
index 73800a1b71..3e6f423b9d 100644
--- a/ci/compile-tests/010-coqdep-errors/runtest.el
+++ b/ci/compile-tests/010-coqdep-errors/runtest.el
@@ -33,6 +33,8 @@
;;; Define the tests
+(defvar cct-coqdep-error-prefix "^coqdep \\|^rocq dep ")
+
(ert-deftest cct-coqdep-fail-on-require ()
"coqdep error on missing library in a require command is detected."
;; (setq cct--debug-tests t)
@@ -47,7 +49,7 @@
(with-current-buffer coq--compile-response-buffer
;; (message "|%s|" (buffer-string))
(goto-char (1+ (length coq--compile-response-initial-content)))
- (setq coqdep-errror-in-response (looking-at "^coqdep "))
+ (setq coqdep-errror-in-response (looking-at cct-coqdep-error-prefix))
(setq missing-module-in-response (search-forward "X25XX" nil t)))
(with-current-buffer proof-shell-buffer
(goto-char (point-min))
@@ -78,7 +80,7 @@
(with-current-buffer coq--compile-response-buffer
;; (message "|%s|" (buffer-string))
(goto-char (1+ (length coq--compile-response-initial-content)))
- (setq coqdep-errror-in-response (looking-at "^coqdep "))
+ (setq coqdep-errror-in-response (looking-at cct-coqdep-error-prefix))
(setq syntax-error-in-response (search-forward "Syntax error" nil t)))
(with-current-buffer proof-shell-buffer
(goto-char (point-min))
@@ -90,6 +92,8 @@
(if coqdep-errror-in-response "DOES" "DOES NOT")
(if syntax-error-in-response "DOES" "DOES NOT")
(if dependency-in-coq "IS" "IS NOT"))
+ (message "coqdep-errror-in-response: %S" coqdep-errror-in-response)
+ (message "*** syntax-error-in-response: %S" syntax-error-in-response)
(should (and coqdep-errror-in-response
syntax-error-in-response
(not dependency-in-coq)))))
@@ -107,7 +111,7 @@
(with-current-buffer coq--compile-response-buffer
;; (message "|%s|" (buffer-string))
(goto-char (1+ (length coq--compile-response-initial-content)))
- (setq coqdep-errror-in-response (looking-at "^coqdep "))
+ (setq coqdep-errror-in-response (looking-at cct-coqdep-error-prefix))
(setq missing-module-in-response (search-forward "X25XX" nil t)))
(with-current-buffer proof-shell-buffer
(goto-char (point-min))
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index 19c4d16de6..e0f0bf488f 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -1897,6 +1897,8 @@ Lock the source file and start the coqdep background
process."
(message "%s: TTT start coqdep for file job for file %s"
(get job 'name)
(get job 'src-file)))
+ (if coq--debug-auto-compilation
+ (message "%s: UUU start %s" (get job 'name) (cons
coq-dependency-analyzer (coq-par-coqdep-arguments (get job 'src-file) (get job
'load-path)))))
(coq-par-start-process
coq-dependency-analyzer
(coq-par-coqdep-arguments (get job 'src-file) (get job 'load-path))
@@ -1917,13 +1919,15 @@ used."
(let ((arguments
(coq-par-coqc-arguments (get job 'src-file) (get job 'load-path))))
(cond
- ((eq (get job 'use-quick) 'vos) (push "-vos" arguments))
- ((eq (get job 'use-quick) 'vio) (push "-quick" arguments))
+ ((eq (get job 'use-quick) 'vos) (nconc arguments (list "-vos")))
+ ((eq (get job 'use-quick) 'vio) (nconc arguments (list "-quick")))
(t t))
(when coq--debug-auto-compilation
(message "%s: TTT start coqc compile for file job for file %s"
(get job 'name)
(get job 'src-file)))
+ (if coq--debug-auto-compilation
+ (message "%s: VVV start %S %S" (get job 'name) coq-compiler arguments))
(coq-par-start-process
coq-compiler
arguments
@@ -1944,7 +1948,9 @@ used."
(get job 'src-file)))
(let ((arguments
(coq-par-coqc-arguments (get job 'src-file) (get job 'load-path))))
- (push "-vok" arguments)
+ (nconc arguments (list "-vok"))
+ (if coq--debug-auto-compilation
+ (message "%s: WWW start %S %S" (get job 'name) coq-compiler arguments))
(coq-par-start-process
coq-compiler
arguments
diff --git a/coq/coq-system.el b/coq/coq-system.el
index 7e7bba02b1..6ca50e2c45 100644
--- a/coq/coq-system.el
+++ b/coq/coq-system.el
@@ -53,13 +53,15 @@ On Windows you might need something like:
(setq coq-prog-env '(\"HOME=C:\\Program Files\\Coq\\\"))"
:group 'coq)
+;; We just call "rocq" and look the error message that should mention
+;; subcommands
(defun coq-detect-rocq-cli ()
- "Return non nil if the detected coq/rocq executable obeys the rocq CLI."
- (let* ((coq-command (or proof-prog-name (coq-autodetect-progname)))
- (coq-args (list "c"))
- (process-args (list coq-command nil t nil "c")))
+ "return non nil if the detected coq/rocq executable obeys the rocq CLI."
+ (let* ((coq-command (or proof-prog-name (coq-autodetect-progname))))
(condition-case nil
- (with-temp-buffer (equal (apply 'process-file process-args) 0))
+ (with-temp-buffer
+ (apply 'process-file (list coq-command nil t))
+ (string-match "Supported subcommands:" (buffer-string)))
(error nil))))
(defun coq-detect-coqdep ()
