branch: elpa/proof-general
commit 5eed5eb87fb3c9ad63387db3cd4cd8ae719c1c2c
Author: Pierre Courtieu <pierre.court...@cnam.fr>
Commit: Pierre Courtieu <pierre.court...@cnam.fr>
Trying to support the rocq CLI.
Also support _RocqProject files.
---
coq/coq-mode.el | 16 +++-
coq/coq-par-compile.el | 15 ++-
coq/coq-system.el | 239 +++++++++++++++++++++++++++---------------------
coq/coq.el | 1 -
generic/proof-config.el | 2 +-
5 files changed, 154 insertions(+), 119 deletions(-)
diff --git a/coq/coq-mode.el b/coq/coq-mode.el
index cdb0ef19ec..2bc1ec39e9 100644
--- a/coq/coq-mode.el
+++ b/coq/coq-mode.el
@@ -36,18 +36,24 @@
;; FIXME: this should probably be done like for smie above.
(defvar coq-may-use-prettify (fboundp 'prettify-symbols-mode))
-(defcustom coq-prog-name
- (or (if (executable-find "coqtop") "coqtop")
+(defun coq-detect-prog-gen (default &rest others)
+ (or (cl-find-if #'executable-find (cons default others))
(let ((exec-path (append exec-path '("C:/Program Files/Coq/bin"))))
- (executable-find "coqtop"))
- "coqtop")
+ (cl-find-if #'executable-find (cons default others)))
+ default))
+
+(defun coq-autodetect-progname ()
+ (coq-detect-prog-gen "coqtop" "rocq"))
+
+(defcustom coq-prog-name (coq-autodetect-progname)
"Name of program to run as Coq.
On Windows with latest Coq package you might need something like:
C:/Program Files/Coq/bin/coqtop.opt.exe
instead of just \"coqtop\".
This must be a single program name with no arguments. See option
`coq-prog-args' to manually adjust the arguments to the Coq process.
-See also `coq-prog-env' to adjust the environment."
+See also `coq-prog-env' to adjust the environment.
+With then 2025 new CLI 'rocq', this command only return 'rocq'."
:type 'string
:group 'coq
:group 'coq-mode)
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index b67612a381..19c4d16de6 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -768,22 +768,21 @@ earlier than 8.19."
Argument CLPATH must be `coq-load-path' from the buffer
that triggered the compilation, in order to provide correct
load-path options to coqdep."
- (nconc (copy-sequence coq-compile-extra-coqdep-arguments) ; copy for nconc
- (coq-par-coqdep-warning-arguments)
- (coq-coqdep-prog-args clpath
- (file-name-directory lib-src-file)
- (coq--pre-v85))
- (list lib-src-file)))
+ (nconc
+ (coq-coqdep-prog-args clpath (file-name-directory lib-src-file)
(coq--pre-v85))
+ (copy-sequence coq-compile-extra-coqdep-arguments) ; copy for nconc
+ (coq-par-coqdep-warning-arguments)
+ (list lib-src-file)))
(defun coq-par-coqc-arguments (lib-src-file clpath)
"Compute the command line arguments for invoking coqc on LIB-SRC-FILE.
Argument CLPATH must be `coq-load-path' from the buffer
that triggered the compilation, in order to provide correct
load-path options to coqdep."
- (nconc (copy-sequence coq-compile-extra-coqc-arguments) ; copy for nconc
- (coq-coqc-prog-args clpath
+ (nconc (coq-coqc-prog-args clpath
(file-name-directory lib-src-file)
(coq--pre-v85))
+ (copy-sequence coq-compile-extra-coqc-arguments) ; copy for nconc
(list lib-src-file)))
(defun coq-par-analyse-coq-dep-exit (status output command)
diff --git a/coq/coq-system.el b/coq/coq-system.el
index 56178c2e25..8ded6f4d7c 100644
--- a/coq/coq-system.el
+++ b/coq/coq-system.el
@@ -29,6 +29,14 @@
(defvar coq-prog-args)
(defvar coq-debug)
+;; Regular files should be of the form "valid_modulename.v" coq
+;; accepts lots of things as letter, this is probably much stricter.
+;; In practice it should be OK though, except maybe for non latin
+;; characters.
+(defun coq-regular-filename-p (s)
+ (let ((noext (file-name-base s)))
+ (string-match-p "\\`[[:alpha:]_][[:alnum:]_]*\\'" noext)))
+
;; Arbitrary arguments can already be passed through _CoqProject.
;; However this is not true for all assistants, so we don't modify the
;; (defpgcustom prog-args) declaration.
@@ -38,23 +46,26 @@
(put 'coq-prog-args 'safe-local-variable #'coq--string-list-p)
+;; DEAD CODE?
(defcustom coq-prog-env nil
"List of environment settings to pass to Coq process.
On Windows you might need something like:
(setq coq-prog-env '(\"HOME=C:\\Program Files\\Coq\\\"))"
:group 'coq)
-(defcustom coq-dependency-analyzer
- (if (executable-find "coqdep") "coqdep"
- (proof-locate-executable "coqdep" t '("C:/Program Files/Coq/bin")))
+(defun coq-detect-coqdep () (coq-detect-prog-gen "coqdep" "rocq"))
+(defun coq-detect-coqc () (coq-detect-prog-gen "coqc" "rocq"))
+
+;; We return the executable coqtop or rocq. But not the rocq option
+;; (dep, c, top)) triggering the particular tool.
+(defcustom coq-dependency-analyzer (coq-detect-coqdep)
"Command to invoke coqdep."
:type 'string
:safe 'stringp
:group 'coq)
-(defcustom coq-compiler
- (if (executable-find "coqc") "coqc"
- (proof-locate-executable "coqc" t '("C:/Program Files/Coq/bin")))
+(defcustom coq-compiler (coq-detect-coqc)
+ ;FIXME
"Command to invoke the coq compiler."
:type 'string
:safe 'stringp
@@ -114,16 +125,16 @@ The given option should make coqtop return immediately.
Optionally check the return code and return nil if the check
fails. Return also nil on other kinds of errors (e.g., `coq-prog-name'
not found).
-This function supports calling coqtop via tramp."
- (let ((coq-command (or coq-prog-name "coqtop"))
- retv)
+This function supports calling coqtop via tramp.
+This function must not rely on coq-autodetect-version, it would be a cycle."
+ (let* ((coq-command (or coq-prog-name (coq-autodetect-progname)))
+ (coq-args (if (string-match "rocq" coq-command) (list "top" option)
(list option)))
+ (process-args (append (list coq-command nil t nil) coq-args))
+ retv)
(condition-case nil
(with-temp-buffer
- (setq retv (if option
- (process-file coq-command nil t nil option)
- (process-file coq-command nil t nil)))
- (if (or (not expectedretv) (equal retv expectedretv))
- (buffer-string)))
+ (setq retv (apply 'process-file process-args))
+ (if (or (not expectedretv) (equal retv expectedretv))
(buffer-string)))
(error nil))))
(defun coq-autodetect-version (&optional interactive-p)
@@ -172,6 +183,18 @@ Returns nil if the version can't be detected."
(signal 'coq-unclassifiable-version coq-version-to-use))
(t (signal (car err) (cdr err))))))))
+(defun coq--post-v9 ()
+ "Return t if the auto-detected version of Coq (or rocs) is >= 9.
+Return nil if the version cannot be detected."
+ (let ((coq-version-to-use (or (coq-version t) "8.20")))
+ (condition-case err
+ (not (coq--version< coq-version-to-use "9"))
+ (error
+ (cond
+ ((equal (substring (cadr err) 0 15) "Invalid version")
+ (signal 'coq-unclassifiable-version coq-version-to-use))
+ (t (signal (car err) (cdr err))))))))
+
(defun coq--post-v86 ()
"Return t if the auto-detected version of Coq is >= 8.6.
Return nil if the version cannot be detected."
@@ -443,65 +466,76 @@ options of a few coq-project files does the right thing."
(coq--options-test-roundtrip "-R /test Test")
(coq--options-test-roundtrip "-I /test")))
-(defun coq-coqdep-prog-args (loadpath &optional current-directory pre-v85)
+;; it is better to inform coqtop of the name of the current module
+;; using the -topfile option, so that coqtop understands references
+;; to it. But don't insist if this would fail (because of wrong
+;; file name): Some people want to script .v files without ever
+;; compiling them.
+(defun coq-topfile-prog-arg ()
+ (when (and (coq--supports-topfile) buffer-file-name)
+ (if (coq-regular-filename-p buffer-file-name)
+ (cons "-topfile" (cons buffer-file-name nil))
+ (message "Warning: buffer %s seems not compilable," buffer-file-name)
+ (message "probably because of its name, no -topfile option set.")
+ nil)))
+
+
+(defun coq-include-prog-args (loadpath &optional current-directory pre-v85)
"Build a list of options for coqdep.
LOADPATH, CURRENT-DIRECTORY, PRE-V85: see `coq-include-options'."
(coq-include-options loadpath current-directory pre-v85))
(defun coq--clean-prog-args (args)
- "Return ARGS without the entries added by `coq-coqtop-prog-args'.
+ "Return ARGS without the entries added by `coq-coqtop-prog-args' and such.
Such entries are currently -emacs and -topfile."
(pcase args
- ((or `("-emacs" . ,rest)
+ ((or `("-emacs" . ,rest) `("top" . ,rest) `("c" . ,rest) `("dep" . ,rest)
`("-topfile" . (,(pred (apply-partially #'equal buffer-file-name)) .
,rest)))
(coq--clean-prog-args rest))
(`(,car . ,cdr)
(cons car (coq--clean-prog-args cdr)))
(_ args)))
+
+(defun coq-common-prog-args (loadpath &optional current-directory pre-v85)
+ "Build a list of options common for coqc and coqtop and coqdep.
+LOADPATH, CURRENT-DIRECTORY, PRE-V85: see `coq-include-options'."
+;; coqtop always adds the current directory to the LoadPath, so don't
+ ;; include it in the -Q options.
+ (append (coq--clean-prog-args coq-prog-args)
+ (let* ((coq-load-path-include-current nil)
+ (cmd (coq-include-prog-args loadpath current-directory
pre-v85)))
+ cmd)))
+
+(defun coq-coqdep-prog-args (loadpath &optional current-directory pre-v85)
+ "Build a list of option for coqdep."
+ (append
+ (if (coq--post-v9) (list "dep") nil)
+ (coq-include-prog-args loadpath current-directory pre-v85)))
+
(defun coq-coqc-prog-args (loadpath &optional current-directory pre-v85)
"Build a list of options for coqc.
LOADPATH, CURRENT-DIRECTORY, PRE-V85: see `coq-include-options'."
;; coqtop always adds the current directory to the LoadPath, so don't
;; include it in the -Q options.
- (append (coq--clean-prog-args coq-prog-args)
- (let ((coq-load-path-include-current nil)) ; Not needed in >=8.5beta3
- (coq-coqdep-prog-args loadpath current-directory pre-v85))))
+ (append (if (coq--post-v9) (list "c") nil)
+ (coq-common-prog-args loadpath current-directory pre-v85)))
-;;XXXXXXXXXXXXXX
;; coq-coqtop-prog-args is the user-set list of arguments to pass to
;; Coq process, see 'defpacustom prog-args' in pg-custom.el for
;; documentation.
-;; Regular files should be of the form "valid_modulename.v" coq
-;; accepts lots of things as letter, this is probably much stricter.
-;; In practice it should be OK though, except maybe for non latin
-;; characters.
-(defun coq-regular-filename-p (s)
- (let ((noext (file-name-base s)))
- (string-match-p "\\`[[:alpha:]_][[:alnum:]_]*\\'" noext)))
-
(defun coq-coqtop-prog-args (loadpath &optional current-directory pre-v85)
;; coqtop always adds the current directory to the LoadPath, so don't
;; include it in the -Q options. This is not true for coqdep.
"Build a list of options for coqc.
LOADPATH, CURRENT-DIRECTORY, PRE-V85: see `coq-coqc-prog-args'."
- (let ((topfile-supported (coq--supports-topfile)))
- (append
- ;; it is better to inform coqtop of the name of the current module
- ;; using the -topfile option, so that coqtop understands references
- ;; to it. But don't insist if this would fail (because of wrong
- ;; file name): Some people want to script .v files without ever
- ;; compiling them.
- (if (and topfile-supported buffer-file-name
- (coq-regular-filename-p buffer-file-name))
- (cons "-topfile" (cons buffer-file-name nil))
- (if (and topfile-supported buffer-file-name)
- (message "Warning: this Coq buffer is probably not compilable \
-because of its name, no -topfile option set."))
- nil)
- (cons "-emacs" (coq-coqc-prog-args loadpath current-directory pre-v85)))))
+ (append
+ (if (coq--post-v9) (list "top") nil)
+ (list "-emacs")
+ (coq-topfile-prog-arg)
+ (coq-common-prog-args loadpath current-directory pre-v85)))
(defun coq-prog-args ()
"Recompute `coq-load-path' before calling `coq-coqtop-prog-args'."
@@ -522,29 +556,61 @@ path (including the -R lib options) (see
`coq-load-path')."
:safe 'booleanp
:group 'coq)
-(defcustom coq-project-filename "_CoqProject"
- "The name of coq project file.
-The coq project file of a coq development (cf. Coq documentation on
-\"makefile generation\") should contain the arguments given to
-coq_makefile. In particular it contains the -I and -R
-options (preferably one per line). If `coq-use-coqproject' is
+;; FIXME: should we add "Make" as a valid project name? Maybe only if
+;; _xxProject is not present? And/Or if its content seems ok?
+(defun coq-default-project-find-file (dir)
+ "Default function for `coq-project-filename'.
+
+If DIR contains an acceptable coq/rocq project file, return it. Return
+nil otherwise. See `coq-project-filename'.
+"
+ (let* ((case-fold-search t)
+ (files (directory-files dir)))
+ ;; \\` and \\' avoid matching "_CoqProject~" and such
+ (cl-find-if
+ (lambda (s) (string-match "\\`\\(_coqproject\\|_rocqproject\\)\\'" s nil
t))
+ files)))
+
+(defcustom coq-project-filename #'coq-default-project-file-p
+ "Variable containing the function detecting a project file.
+
+See it default value `coq-default-project-find-file' for an example.
+
+The function takes one argument, the name of a directory, and returns
+the name of a coq/rocq project file it contains if there is one. Return
+nil otherwise.
+
+This is used to detect the coq project file (using
+`locate-dominating-file'). By default we accept _CoqProject and
+_RocqProject (and any case-variant of these) without checking coq/rocq
+version. If you want something smarter please redefine
+`coq-project-filename' directly by using:
+
+(setq coq-project-filename #'my-own-predicate)
+
+About the coq/rocq project file (cf. Coq documentation on project files
+and \"makefile generation\"):
+
+The coq project file of a coq development should contain the arguments
+given to coq_makefile. In particular it contains the -I and -R
+options (preferably one per line). If `coq-use-coqproject' is
t (default) the content of this file will be used by Proof General to
-infer the `coq-load-path' and the `coq-prog-args' variables that set
-the coqtop invocation by Proof General. This is now the recommended
-way of configuring the coqtop invocation. Local file variables may
-still be used to override the coq project file's configuration.
-.dir-locals.el files also work and override project file settings."
- :type 'string
- :safe 'stringp
+infer the `coq-load-path' and the `coq-prog-args' variables that set the
+coqtop invocation by Proof General. This is now the recommended way of
+configuring the coqtop invocation. Local file variables may still be
+used to override the coq project file's configuration. .dir-locals.el
+files also work and override project file settings.
+"
+ :type 'function
:group 'coq)
(defun coq-find-project-file ()
"Return '(buf alreadyopen) where buf is the buffer visiting coq project file.
alreadyopen is t if buffer already existed."
(when buffer-file-name
- (let* ((projectfiledir (locate-dominating-file buffer-file-name
coq-project-filename)))
+ (let* ((projectfiledir (locate-dominating-file buffer-file-name
#'coq-default-project-find-file)))
(when projectfiledir
- (let* ((projectfile (expand-file-name coq-project-filename
projectfiledir))
+ (let* ((projectfile (expand-file-name (coq-default-project-find-file
projectfiledir) projectfiledir))
;; we store this intermediate result to know if we have to kill
;; the coq project buffer at the end
(projectbufferalreadyopen (find-buffer-visiting projectfile))
@@ -603,7 +669,7 @@ coqtop. But -arg \"'a b'\" means to pass a and b together."
(setq args
(append args
(split-string-and-unquote concatenated-args
coq--project-file-separator)))))))
- (cons "-emacs" args)))
+ args))
(defun coq--extract-load-path-1 (option base-directory)
"Convert one _CoqProject OPTION, relative to BASE-DIRECTORY."
@@ -686,6 +752,11 @@ Does nothing if `coq-use-project-file' is nil."
;; avoid adding for other modes , the setting is performed inside
;; coq-mode-hook. This is described in www.emacswiki.org/emacs/LocalVariables
+;; NOTE: the coq-prog-arg variable is local to the buffer, and it is
+;; re-populated each time coq is launched on this buffer. In other
+;; words: this hook is useful for coq files on which coq will not be
+;; run.
+
;; TODO: also read COQBIN somewhere?
;; Note: this does not need to be at a particular place in the hook, but we
;; need to make this hook local.
@@ -703,6 +774,10 @@ Does nothing if `coq-use-project-file' is nil."
(lambda ()
;; It seems coq-prog-name and proof-prog-name are not correctly
linked
;; so let us make sure they are the same before computing options
+ ;; coq < 9 needs "coqtop",
+ (setq proof-prog-name (coq-autodetect-progname))
+ (setq coq-compiler (coq-detect-coqc))
+ (setq coq-dependency-analyzer (coq-detect-coqdep))
(setq coq-prog-name proof-prog-name)
(setq coq-prog-args (coq-prog-args))))
@@ -729,48 +804,4 @@ Does nothing if `coq-use-project-file' is nil."
(provide 'coq-system)
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; To guess the command line options ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; OBSOLETE, should take _CoqProject into account.
-(defun coq-guess-command-line (filename)
- "Guess the right command line options to compile FILENAME using `make -n'.
-This function is obsolete, the recommended way of setting the coqtop
-options is to use a _Coqproject file as described in coq
-documentation. ProofGeneral reads this file and sets compilation
-options according to its contents. See `coq-project-filename'. Per
-file configuration may then be set using local file variables."
- (if (local-variable-p 'coq-prog-name (current-buffer))
- coq-prog-name
- (let* ((dir (or (file-name-directory filename) "."))
- (makedir
- (cond
- ((file-exists-p (concat dir "Makefile")) ".")
- ;; ((file-exists-p (concat dir "../Makefile")) "..")
- ;; ((file-exists-p (concat dir "../../Makefile")) "../..")
- (t nil))))
- (if (and coq-use-makefile makedir)
- (let*
- ;;TODO, add dir name when makefile is in .. or ../..
- ;;
- ;; da: FIXME: this code causes problems if the make
- ;; command fails. It should not be used by default
- ;; and should be made more robust.
- ;;
- ((compiled-file (concat (substring
- filename 0
- (string-match ".v$" filename)) ".vo"))
- (command (shell-command-to-string
- (concat "cd " dir ";"
- "make -n -W " filename " " compiled-file
- "| sed s/coqc/coqtop/"))))
- (message command)
- (setq coq-prog-args nil)
- (concat
- (substring command 0 (string-match " [^ ]*$" command))
- "-emacs"))
- coq-prog-name))))
-
;;; coq-system.el ends here
diff --git a/coq/coq.el b/coq/coq.el
index 2b83a1ddd4..2e4951f836 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1899,7 +1899,6 @@ at `proof-assistant-settings-cmds' evaluation time.")
(setq proof-assistant-home-page coq-www-home-page)
(setq proof-prog-name coq-prog-name)
- (setq proof-guess-command-line #'coq-guess-command-line)
(setq proof-prog-name-guess t)
;; We manage file saveing via coq-compile-auto-save and for coq
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 07e338599a..ed0703c106 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -107,7 +107,7 @@
The function could take a filename as argument, run `make -n' to see
how to compile the file non-interactively, then translate the result
into an interactive invocation of the proof assistant with the same
-command line options. For an example, see coq/coq.el."
+command line options."
:type 'function
:group 'prover-config)
