diff options
| -rw-r--r-- | CHANGES | 22 | ||||
| -rw-r--r-- | COMPATIBILITY | 31 | ||||
| -rw-r--r-- | INSTALL | 15 | ||||
| -rw-r--r-- | Makefile.devel | 6 | ||||
| -rw-r--r-- | README.md (renamed from README) | 52 | ||||
| -rw-r--r-- | coq/coq-indent.el | 119 | ||||
| -rw-r--r-- | coq/coq-par-compile.el | 17 | ||||
| -rw-r--r-- | coq/coq-seq-compile.el | 9 | ||||
| -rw-r--r-- | coq/coq-smie.el | 17 | ||||
| -rw-r--r-- | coq/coq-syntax.el | 1 | ||||
| -rw-r--r-- | coq/coq-system.el | 541 | ||||
| -rw-r--r-- | coq/coq.el | 68 | ||||
| -rw-r--r-- | doc/Makefile.doc | 2 | ||||
| -rw-r--r-- | etc/ProofGeneral.spec | 2 | ||||
| -rw-r--r-- | generic/proof-site.el | 4 |
15 files changed, 521 insertions, 385 deletions
@@ -75,14 +75,6 @@ the GIT ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. tac2; tac3. -*** indentation now supports { at end of line: - example: - - assert (h:n = k). { - apply foo. - reflexivity. } - apply h. - *** Default indentation of forall and exists is not boxed anymore For instance, this is now indented like this: @@ -99,20 +91,6 @@ the GIT ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. Lemma foo: forall x y, x = 0 -> ... . -*** Default indentation cases of "match with" are now indented by 2 instead of 4. - "|" is indented by zero: - - match n with - 0 => ... - | S n => ... - end - instead of: - match n with - 0 => ... - | S n => ... - end - do this: (setq coq-match-indent 4) to bring old behaviour back. - *** Support for bullets, braces and Grab Existential Variables for Prooftree. *** Support for _Coqproject files diff --git a/COMPATIBILITY b/COMPATIBILITY index 6af37517..4bf5de0b 100644 --- a/COMPATIBILITY +++ b/COMPATIBILITY @@ -4,21 +4,17 @@ Compatibility of Proof General This version of Proof General has been tested with these Emacs versions on recent Linux systems: - Emacs 23.4 -- recommended and supported - Emacs 23.3,23.2 -- previous versions, should work - Emacs 24 (development) -- next version, should work - Emacs 23.1, earlier -- obsolete versions, do NOT work + Emacs 24.5 -- recommended and supported + Emacs 24.3, 24.4 -- previous versions, should work + Emacs 25 (dev) -- next version, should work + Emacs 23.2, earlier -- obsolete versions, do NOT work -and (main) prover versions: Coq 8.3, Isabelle2011[-1] +and (main) prover versions: Coq 8.4, Coq 8.5 See below for notes about other operating systems. -Maintaining compatibility across proof assistant versions, Emacs -versions and operating systems is virtually impossible. - In the major 4.0 release ** XEmacs compatibility was dropped ** - Running on Mac OS X ------------------- @@ -26,14 +22,14 @@ For tips, please see here: http://proofgeneral.inf.ed.ac.uk/wiki/PGEmacsOnMacOSX -We recommend the 23.2 build of GNU Emacs, which builds natively on Mac +We recommend the 24.5 build of GNU Emacs, which builds natively on Mac OS X (based on the NextStep port). Binaries are available at various websites (e.g., http://emacsformacosx.com), or you can build your own by compiling from the FSF CVS. See the Emacs Wiki at http://www.emacswiki.org/emacs/EmacsForMacOS for more. Note that Mac compatibility isn't thoroughly tested. If you discover -problems, please send a report and/or fix to the PG trac. Please +problems, please send a report and/or fix to the PG tracker. Please add tips to the wiki page above. @@ -44,19 +40,6 @@ For tips, please see here: http://proofgeneral.inf.ed.ac.uk/wiki/PGEmacsOnWindows -We recommend EmacsW32 available at: - - http://www.ourcomments.org/Emacs/EmacsW32.html - -Unpack the Proof General tar or zip file, and rename the folder to -"ProofGeneral" to remove the version number. Put a line like this: - - (load-file "c:\\ProofGeneral\\generic\\proof-site.el") - -into .emacs. You should put .emacs in value of HOME if you set that, -or else in directory you installled Emacs in, e.g. -c:\Program Files\Emacs\.emacs - Note that Windows compatibility isn't tested by the maintainers. If you discover problems, please add notes on the Wiki page above, and submit patches to http://proofgeneral.inf.ed.ac.uk/trac @@ -1,3 +1,18 @@ +From GitHub +=========== + +Download and install Proof General from GitHub: + + git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG + make -C ~/.emacs.d/lisp/PG + +Then add the following to your .emacs: + + ;; Open .v files with Proof General's Coq mode + (require 'proof-site "~/.emacs.d/lisp/PG/generic/proof-site") + +This should be enough. Instructions for previous releases are below. + Short Instructions for installing Proof General (details below) =============================================================== diff --git a/Makefile.devel b/Makefile.devel index a201231b..64d5b53c 100644 --- a/Makefile.devel +++ b/Makefile.devel @@ -91,8 +91,8 @@ DEVELOPERS=\ # The prereltag.txt is kept as a record in the distrib area # of the current pre-release version (currently not used explicitly # anywhere for web pages/whatever). -PRERELEASE_PREFIX=4\.3pre -PRERELEASE_TAG=4.3pre$(shell date "+%y%m%d") +PRERELEASE_PREFIX=4\.4pre +PRERELEASE_TAG=4.4pre$(shell date "+%y%m%d") PREREL_TAG_FILE=prereltag.txt # Path to web pages in repository, used for automatically @@ -320,7 +320,7 @@ tag: # Update the sources, this is almost always what we want to do. if [ -z "$(NOCVS)" ] && [ -n "`cvs -n -q update -Pd | grep '^[MC] '`" ]; then cvs update -Pd; exit 1; fi # Update version in proof-site.el - (cd generic; mv $(VERSIONFILE) $(VERSIONFILE).old; sed -e 's/defconst $(VERSIONVARIABLE) \".*\"/defconst $(VERSIONVARIABLE) \"Proof General Version $(FULLVERSION). Released by da$(DATEMSG).\"/g' $(VERSIONFILE).old > $(VERSIONFILE); rm $(VERSIONFILE).old) + (cd generic; mv $(VERSIONFILE) $(VERSIONFILE).old; sed -e 's/defconst $(VERSIONVARIABLE) \".*\"/defconst $(VERSIONVARIABLE) \"Proof General Version $(FULLVERSION).\"/g' $(VERSIONFILE).old > $(VERSIONFILE); rm $(VERSIONFILE).old) # Tag ProofGeneral.spec (cd etc; mv ProofGeneral.spec ProofGeneral.spec.old; sed -e 's/Version:.*$$/Version: $(VERSION)/g' ProofGeneral.spec.old > ProofGeneral.spec; rm ProofGeneral.spec.old) # Edit $(DOWNLOADHTMLS) only for prereleases. @@ -1,35 +1,54 @@ - Proof General --- Organize your proofs! +# Proof General — Organize your proofs! Proof General is a generic Emacs interface for proof assistants. The aim of the Proof General project is to provide a powerful, generic environment for using interactive proof assistants. -This is version 4.2 (prerelease) of Proof General. See About for exact version. -It is built for Emacs 23.3. +This is version 4.4pre of Proof General. -The code *may* also work with previous emacs versions, back as far as -Emacs 22.3. But you will need to regenerated the byte-compiled files -with "make clean; make compile". Backward compatibility cannot be -guaranteed. +## Setup + +Remove old versions of Proof General, then download and install the new release from GitHub: + +``` +git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG +cd ~/.emacs.d/lisp/PG +make +``` + +Then add the following to your `.emacs`: + +``` +;; Open .v files with Proof General's Coq mode +(require 'proof-site "~/.emacs.d/lisp/PG/generic/proof-site") +``` + +If Proof General complains about a version mismatch, make sure that the shell's `emacs` is indeed your usual Emacs. If not, run the Makefile again with an explicit path to Emacs. On Mac in particular you'll probably need something like + +``` +make clean; make EMACS=/Applications/Emacs.app/Contents/MacOS/Emacs +``` + +## More info See + INSTALL for installation details. COPYING for license details. COMPATIBILITY for version compatibility information. REGISTER for registration information (please register). FAQ, doc/ for documentation of Proof General. - + <prover>/README for additional prover-specific notes Links: - Bug/feature reports: http://proofgeneral.inf.ed.ac.uk/trac Wiki: http://proofgeneral.inf.ed.ac.uk/wiki Lists: http://proofgeneral.inf.ed.ac.uk/mailinglist -Supported proof assistants: Coq, Isabelle, LEGO, PhoX -Experimental (less useful): CCC,ACL2,HOL98,Hol-Light,Lambda-Clam,Shell,Twelf - Obsolete instances: Demoisa,Lambda-Clam,Plastic +* Supported proof assistants: Coq, Isabelle, LEGO, PhoX +* Experimental (less useful): CCC,ACL2,HOL98,Hol-Light,Lambda-Clam,Shell,Twelf +* Obsolete instances: Demoisa,Lambda-Clam,Plastic A few example proofs are included in each prover subdirectory. The "root2" proofs of the irrationality of the square root of 2 were @@ -37,12 +56,3 @@ proofs written for Freek Wiedijk's challenge in his comparison of different theorem provers, see http://www.cs.kun.nl/~freek/comparison/. Those proof scripts are copyright by their named authors. (NB: most of these have rusted) - -Check BUGS files for some static problems and issues. Please report -new bugs on the Trac site at http://proofgeneral.inf.ed.ac.uk/trac. - -For the latest news and downloads, visit Proof General on the web -at: http://proofgeneral.inf.ed.ac.uk - -David Aspinall <da+pg-feedback@inf.ed.ac.uk> -October 2011. diff --git a/coq/coq-indent.el b/coq/coq-indent.el index 406fc673..fddfc373 100644 --- a/coq/coq-indent.el +++ b/coq/coq-indent.el @@ -96,77 +96,116 @@ detect if they start something or not." (not (proof-string-match "{\\s-*\\(wf\\|measure\\)" str))))))) +(defconst coq-simple-cmd-ender-regexp "[^.]\\|\\=\\|\\.\\." + "Used internally. Matches the allow prefix of the coq \".\" command ending.") + +(defconst coq-bullet-regexp-nospace "\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+" + "Matches single bullet, WARNING: Lots of false positive. + +No context checking.") + +;; We can detect precisely bullets (and curlies) by looking at there +;; prefix: the prefix should be a real "." then spaces then only +;; bullets and curlys and spaces). This is used when search backward. +;; This variable is the regexp of possible prefixes +(defconst coq-bullet-prefix-regexp + (concat "\\(?:\\(?:" coq-simple-cmd-ender-regexp "\\)" + "\\(?:\\.\\)\\(?:\\s-\\)\\(?:\\s-\\|{\\|}\\|-\\|+\\|\\*\\)*\\)")) + ;; matches regular command end (. and ... followed by a space or buffer end) ;; ". " and "... " are command endings, ".. " is not, same as in ;; proof-script-command-end-regexp in coq.el (defconst coq-period-end-command - "\\(?:\\(?2:[^.]\\|\\=\\|\\.\\.\\)\\(?1:\\.\\)\\(?3:\\s-\\|\\'\\)\\)") + (concat "\\(?:\\(?2:" coq-simple-cmd-ender-regexp "\\)\\(?1:\\.\\)\\(?3:\\s-\\|\\'\\)\\)") + "Matches coq regular syntax for ending a command (except bullets and curlies). -;; matches curly bracket but not {| and |} WARNING this matches more -;; than the script parenthesizing '{' and '}' as curly bracket may -;; match this when used in regular expressions -(defconst coq-curlybracket-end-command - "\\(?:\\(?1:{\\)\\(?3:[^|]\\)\\|\\(?2:[^|]\\|\\=\\)\\(?1:}\\)\\)") +This should match EXACTLY command ending syntax. No false +positive should be accepted. \"...\" is matched as \".\" with a +left context \"..\". - - -;; bullets must be preceded by a space but since we usually -;; search for this expression from the first non white char of the -;; command, so we give two versions of this regexp - -;; matches bullets. WARNING this matches more than real bullets as - + -;; and * may match this when used in regular expressions -;(defconst coq-bullet-end-command -; "\\(?2:\\s-\\|\\=\\)\\(?:\\(?1:-\\)\\|\\(?1:+\\)\\|\\(?1:\\*\\)\\)") -;; Allowing - -- --- and + ++ +++ ... +There are 3 substrings (2 and 3 may be nil): +* number 1 is the real bullet string, +* number 2 is the left context matched that is not part of the bullet +* number 3 is the right context matched that is not part of the bullet +") ;; captures a lot of false bullets, need to check that the commaand is ;; empty. When searching forward (typically when splitting the buffer ;; into commands commands) we can't do better than that. -;; For backward searching see `coq-bullet-end-command-backward' below. (defconst coq-bullet-end-command - "\\(?:\\(?2:\\s-\\|\\=\\)\\(?1:\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+\\)\\)") + (concat "\\(?:\\(?2:\\s-\\|\\=\\)" "\\(?1:" coq-bullet-regexp-nospace "\\)\\)") + "Matches ltac bullets. WARNING: lots of false positive. -(defconst coq-bullet-regexp-nospace - "\\(?1:\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+\\)") +This matches more than real bullets as - + and * may match this +when used in regular expressions. See +`coq-bullet-end-command-backward' for a more precise regexp (but +only when searching backward).") -;; Trying to capture precisely bullets when search backward (forward -;; is harder since we need to look backward if a dot is eventually -;; there) +;; Context aware detecting regexp, usefull when search backward. (defconst coq-bullet-end-command-backward -"\\(?:\\(?2:\\(?:[^.]\\|\\=\\|\\.\\.\\)\\(?:\\.\\)\\(?:\\s-\\)\\(?:\\s-\\|{\\|}\\|-\\|+\\|\\*\\)*\\)\\(?1:\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+\\)\\)" -) + (concat "\\(?:\\(?2:" coq-bullet-prefix-regexp "\\)\\(?1:\\(-\\)+\\|\\(+\\)+\\|\\(\\*\\)+\\)\\)") + "Matches ltac bullets when searching backward. + +This should match EXACTLY bullets. No false positive should be accepted. +There are 2 substrings: +* number 1 is the real bullet string, +* number 2 is the left context matched that is not part of the bullet" ) + +(defconst coq-curlybracket-end-command + "\\(?:\\(?1:{\\)\\(?3:[^|]\\)\\|\\(?2:[^|]\\|\\=\\)\\(?1:}\\)\\)" + "Matches ltac curlies when searching backward. Warning: False positive. + +There are 3 substrings (2 and 3 may be nil): +* number 1 is the real bullet string, +* number 2 is the left context matched that is not part of the bullet +* number 3 is the right context matched that is not part of the bullet + +This matches more than real ltac curlies. See +`coq-bullet-end-command-backward' for a more precise regexp (but +only when searching backward).") + +(defconst coq-curlybracket-end-command-backward + (concat "\\(?:\\(?2:" coq-bullet-prefix-regexp "\\)\\(?:\\(?:\\(?1:{\\)\\(?3:[^|]\\)\\)\\|\\(?1:}\\)\\)\\)") + "Matches ltac curly brackets when searching backward. + +This should match EXACTLY script structuring curlies. No false +positive should be accepted. +There are 3 substrings (2 and 3 may be nil): +* number 1 is the real bullet string, +* number 2 is the left context matched that is not part of the bullet +* number 3 is the right context matched that is not part of the bullet") -;; order matter here, since bullet regexp contains period regexp (defconst coq-end-command-regexp (concat coq-period-end-command "\\|" coq-bullet-end-command "\\|" coq-curlybracket-end-command) -; "\\(?2:[^.]\\|\\.\\.\\)\\(?1:\\.\\)\\(?3:\\s-\\|\\'\\)" - "Regexp matching end of a command. There are 3 substrings: + "Matches end of commands (and ltac bullets and curlies). WARNING: False positive. + +There are 3 substrings: * number 1 is the real coq ending string, * number 2 is the left context matched that is not part of the ending string * number 3 is the right context matched that is not part of the ending string -WARNING: this regexp accepts curly brackets (if not preceded by -'|') and bullets (+ - *) (if preceded by a space or at cursor). -This is of course not correct and some more check is needed to -distinguish between the different uses of this characters. -Currently bullets are always ending an empty command, so we just -need to check that the command ended by the bullet-like regexp is empty. -This is done below and also in coq-smie.el.") +WARNING: this regexp accepts some curly brackets and bullets (+ - +*) with no sufficient context verification. Lots of false +positive are matched. Currently bullets and curlies are always +ending an empty command, so we just need to check that the +command ended by the bullet-like regexp is empty. This is done in +coq-smie.el, and see `coq-end-command-regexp-backward' for a more +precise regexp (but only when searching backward).") (defconst coq-end-command-regexp-backward (concat coq-bullet-end-command-backward "\\|" coq-period-end-command "\\|" - coq-curlybracket-end-command) -; "\\(?2:[^.]\\|\\.\\.\\)\\(?1:\\.\\)\\(?3:\\s-\\|\\'\\)" - "Regexp matching end of a command. There are 3 substrings: + coq-curlybracket-end-command-backward) + "Matches end of commands, including bullets and curlies. + +There are 3 substrings (2 and 3 may be nil): * number 1 is the real coq ending string, * number 2 is the left context matched that is not part of the ending string * number 3 is the right context matched that is not part of the ending string -This regexp is much more precise than `coq-end-command-regexp' but only +Remqrk: This regexp is much more precise than `coq-end-command-regexp' but only works when searching backward.") diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el index fac1ff35..5c37c382 100644 --- a/coq/coq-par-compile.el +++ b/coq/coq-par-compile.el @@ -19,7 +19,10 @@ ;; - add option coq-par-keep-compilation-going ;; - check what happens if coq-par-coq-arguments gets a bad load path ;; - on error, try to put location info into the error message -;; +;; +;; Note that all argument computations inherit `coq-autodetected-version': when +;; changing compilers, all compilation jobs must be terminated. This is +;; consistent with the fact that the _CoqProject file is not reparsed. (eval-when-compile (require 'proof-compat)) @@ -450,25 +453,23 @@ belonging to the circle." (nreverse result))) -;;; map coq module names to files, using synchronously running coqdep +;;; map coq module names to files, using synchronously running coqdep (defun coq-par-coqdep-arguments (lib-src-file coq-load-path) "Compute the command line arguments for invoking coqdep on LIB-SRC-FILE. Argument COQ-LOAD-PATH must be `coq-load-path' from the buffer that triggered the compilation, in order to provide correct load-path options to coqdep." - (nconc ;(coq-include-options lib-src-file coq-load-path) - (coq-coqdep-prog-args lib-src-file coq-load-path) - (list lib-src-file))) + (nconc (coq-coqdep-prog-args coq-load-path (file-name-directory lib-src-file) (coq--pre-v85)) + (list lib-src-file))) (defun coq-par-coqc-arguments (lib-src-file coq-load-path) "Compute the command line arguments for invoking coqdep on LIB-SRC-FILE. Argument COQ-LOAD-PATH must be `coq-load-path' from the buffer that triggered the compilation, in order to provide correct load-path options to coqdep." - (nconc ;(coq-include-options lib-src-file coq-load-path) - (coq-coqc-prog-args lib-src-file coq-load-path) - (list lib-src-file))) + (nconc (coq-coqc-prog-args coq-load-path (file-name-directory lib-src-file) (coq--pre-v85)) + (list lib-src-file))) (defun coq-par-analyse-coq-dep-exit (status output command) "Analyse output OUTPUT of coqdep command COMMAND with exit status STATUS. diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el index 0c1beae3..e00a2793 100644 --- a/coq/coq-seq-compile.el +++ b/coq/coq-seq-compile.el @@ -73,7 +73,8 @@ dependencies are absolute too and the simplified treatment of `coq-load-path-include-current' in `coq-include-options' won't break." (let ((coqdep-arguments - (nconc (coq-include-options lib-src-file coq-load-path) + ;; FIXME should this use coq-coqdep-prog-args? + (nconc (coq-include-options coq-load-path (file-name-directory lib-src-file) (coq--pre-v85)) (list lib-src-file))) coqdep-status coqdep-output) (if coq-debug-auto-compilation @@ -111,8 +112,8 @@ break." Display errors in buffer `coq-compile-response-buffer'." (message "Recompile %s" src-file) (let ((coqc-arguments - (nconc ;(coq-include-options src-file coq-load-path) - (coq-coqc-prog-args src-file coq-load-path) + (nconc + (coq-coqc-prog-args coq-load-path (file-name-directory src-file) (coq--pre-v85)) (list src-file))) coqc-status) (coq-init-compile-response-buffer @@ -121,7 +122,7 @@ Display errors in buffer `coq-compile-response-buffer'." (message "call coqc arg list: %s" coqc-arguments)) (setq coqc-status (apply 'call-process - coq-compiler nil coq-compile-response-buffer t coqc-arguments)) + coq-compiler nil coq-compile-response-buffer t coqc-arguments)) (if coq-debug-auto-compilation (message "compilation %s exited with %s, output |%s|" src-file coqc-status diff --git a/coq/coq-smie.el b/coq/coq-smie.el index 403dc4a8..a609727a 100644 --- a/coq/coq-smie.el +++ b/coq/coq-smie.el @@ -958,6 +958,7 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies." ;; tac1 ; <-- no indentation here ;; now ( tac3 ; <- neither here ;; tac5) ; + ;; ] ((and (equal token "; tactic") coq-indent-semicolon-tactical (not (coq-smie-is-ltacdef)) @@ -974,13 +975,19 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies." ((equal token "} subproof") (smie-rule-parent)) - ; using user customized variable to set indentation of modules, - ; section and proofs. + ;; proofstart is a special hack, since "." should be used as a + ;; separator between commands, here it is recognized as an open + ;; parenthesis, hence the current command (C) ending with "." + ;; is not recognized as correctly terminated. The "parent" + ;; computed by smie is therefore wrong and default indetation + ;; is broken. We fix this by indenting from the real-start of + ;; the command terminated by ". proofstart". ((equal token ". proofstart") - (smie-rule-parent coq-indent-proofstart)) + (save-excursion (forward-char -1) (coq-find-real-start) + `(column . ,(+ coq-indent-modulestart (current-column))))) ((equal token ". modulestart") - (smie-rule-parent coq-indent-modulestart)) - )) + (save-excursion (forward-char -1) (coq-find-real-start) + `(column . ,(+ coq-indent-modulestart (current-column))))))) (:before (cond diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 3b4ad3cc..37867dca 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -189,6 +189,7 @@ so for the following reasons: ("elim using" "elu" "elim # using #" t) ("elim" "e" "elim #" t "elim") ("elimtype" "elt" "elimtype" "elimtype") + ("erewrite" "er" "erewrite #" t "erewrite") ("eright" "erig" "eright" "eright") ("esplit" "esp" "esplit" t "esplit") ;; ("exact" "exa" "exact" t "exact") diff --git a/coq/coq-system.el b/coq/coq-system.el index a8e2f1af..0d09e0f2 100644 --- a/coq/coq-system.el +++ b/coq/coq-system.el @@ -23,16 +23,6 @@ (defvar coq-prog-args nil) (defvar coq-debug nil)) -(eval-when (compile) - (defvar coq-pre-v85 nil)) - -(defun get-coq-version () - (let ((c (shell-command-to-string "coqtop -v"))) - (if (string-match "version \\([^ ]+\\)\\s-" c) - (match-string 1 c) - c))) - - (defcustom coq-prog-env nil "List of environment settings d to pass to Coq process. On Windows you might need something like: @@ -41,15 +31,15 @@ On Windows you might need something like: (defcustom coq-prog-name (proof-locate-executable "coqtop" t '("C:/Program Files/Coq/bin")) - "*Name of program to run as Coq. See `proof-prog-name', set from this. + "*Name of program to run as Coq. See `proof-prog-name', set from this. 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 `coq-prog-args' to manually adjust the arguments to the Coq process. See also `coq-prog-env' to adjust the environment." - :type 'string - :group 'coq) + :type 'string + :group 'coq) (defcustom coq-dependency-analyzer (proof-locate-executable "coqdep" t '("C:/Program Files/Coq/bin")) @@ -69,7 +59,7 @@ See also `coq-prog-env' to adjust the environment." "/usr/local/lib/coq" c))) -(defconst coq-library-directory (get-coq-library-directory) +(defconst coq-library-directory (get-coq-library-directory) ;; FIXME Should be refreshed more often "The coq library directory, as reported by \"coqtop -where\".") (defcustom coq-tags (concat coq-library-directory "/theories/TAGS") @@ -77,16 +67,68 @@ See also `coq-prog-env' to adjust the environment." :type 'string :group 'coq) +(defcustom coq-pinned-version nil + "Which version of Coq you are using. +There should be no need to set this value; Proof General can +adjust to various releases of Coq automatically." + :type 'string + :group 'coq) + +(defvar coq-autodetected-version nil + "Version of Coq, as autodetected by `coq-autodetect-version'.") + +(defun coq-version (&optional may-recompute) + "Return the precomputed version of the current Coq toolchain. +With MAY-RECOMPUTE, try auto-detecting it if it isn't available." + (or coq-pinned-version + coq-autodetected-version + (when may-recompute + (coq-autodetect-version)))) + +(defun coq-show-version () + "Show the version of Coq currently in use. +If it doesn't look right, try `coq-autodetect-version'." + (interactive) + (let ((version (coq-version nil))) + (if version + (message "Using Coq v%s" coq-autodetected-version) + (message "Coq version unknown at this time. Use `coq-autodetect-version' to autodetect.")))) + +(defun coq-autodetect-version (&optional interactive-p) + "Detect and record the version of Coq currently in use. +Interactively (with INTERACTIVE-P), show that number." + (interactive '(t)) + (setq coq-autodetected-version nil) + (let ((version-string (car (process-lines (or coq-prog-name "coqtop") "-v")))) + (when (and version-string (string-match "version \\([^ ]+\\)" version-string)) + (setq coq-autodetected-version (match-string 1 version-string)))) + (when interactive-p + (coq-show-version)) + coq-autodetected-version) + +(defun coq--version< (v1 v2) + "Compare Coq versions V1 and V2." + ;; -snapshot is only supported by Emacs 24.5, not 24.3 + (let ((version-regexp-alist `(("^[-_+ ]?snapshot$" . -4) + ("^pl$" . 0) + ,@version-regexp-alist))) + (version< v1 v2))) + (defcustom coq-pre-v85 nil - "Whether to use <= coq-8.4 config (nil by default). -Mainly to deal with command line options that changed between 8.4 -and 8.5 (-Q foo bar replace -I foo)." + "Deprecated. +Use `coq-pinned-version' if you want to bypass the +version detection that Proof General does automatically." :type 'boolean :group 'coq) +(defun coq--pre-v85 () + "Return non-nil if the auto-detected version of Coq is < 8.5. +Returns nil if the version can't be detected." + (coq--version< (or (coq-version t) "8.5") "8.5snapshot")) + (defcustom coq-use-makefile nil "Whether to look for a Makefile to attempt to guess the command line. -Set to t if you want this feature." +Set to t if you want this feature, but note that it is deprecated." :type 'string :group 'coq) @@ -101,27 +143,27 @@ Set to t if you want this feature." "Check if PATH is a safe value for `coq-load-path'." (and (listp path) - (every + (cl-every (lambda (entry) (or (stringp entry) (and (listp entry) (eq (car entry) 'rec) - (every 'stringp (cdr entry)) + (cl-every 'stringp (cdr entry)) (equal (length entry) 3)) (and (listp entry) (eq (car entry) 'nonrec) - (every 'stringp (cdr entry)) + (cl-every 'stringp (cdr entry)) (equal (length entry) 3)) (and (listp entry) (eq (car entry) 'recnoimport) - (every 'stringp (cdr entry)) + (cl-every 'stringp (cdr entry)) (equal (length entry) 3)) (and (listp entry) (eq (car entry) 'ocamlimport) - (every 'stringp (cdr entry)) + (cl-every 'stringp (cdr entry)) (equal (length entry) 2)) (and (listp entry) - (every 'stringp entry) + (cl-every 'stringp entry) (equal (length entry) 2)))) path))) @@ -133,44 +175,45 @@ coqtop. Usually, the elements of this list are strings (for \"-Q\" dir path). The possible forms of elements of this list correspond to the 4 -forms of include options ('-I' '-Q' and '-R'). An element can be +forms of include options (`-I' `-Q' and `-R'). An element can be - - A list of the form '(ocamlimport dir)', specifying a - directory to be added to ocaml path ('-I'). - - A list of the form '(rec dir path)' (where dir and path are + - A list of the form `(\\='ocamlimport dir)', specifying (in 8.5) a + directory to be added to ocaml path (`-I'). + - A list of the form `(\\='rec dir path)' (where dir and path are strings) specifying a directory to be recursively mapped to the - logical path 'path' ('-R dir path'). - - A list of the form '(recnoimport dir path)' (where dir and + logical path `path' (`-R dir path'). + - A list of the form `(\\='recnoimport dir path)' (where dir and path are strings) specifying a directory to be recursively - mapped to the logical path 'path' ('-Q dir path'), but not + mapped to the logical path `path' (`-Q dir path'), but not imported (modules accessible for import with qualified names - only). - - A list of the form '(norec dir)', specifying a directory - to be mapped to the empty logical path ('-Q dir \"\"'). + only). Note that -Q dir \"\" has a special, nonrecursive meaning. + - A list of the form (8.4 only) `(\\='nonrec dir path)', specifying a + directory to be mapped to the logical path 'path' ('-I dir -as path'). -For convenience the symbol 'rec' can be omitted and entries of -the form '(dir path)' are interpreted as '(rec dir path)'. +For convenience the symbol `rec' can be omitted and entries of +the form `(dir path)' are interpreted as `(rec dir path)'. + +A plain string maps to -Q ... \"\" in 8.5, and -I ... in 8.4. Under normal circumstances this list does not need to contain the coq standard library or \".\" for the current directory (see `coq-load-path-include-current'). WARNING: if you use coq <= 8.4, the meaning of these options is -not the same (-I is for coq path). -" - :type '(repeat (choice (string :tag "simple directory without path (-Q \"\")") ; is this really useful? +not the same (-I is for coq path)." + :type '(repeat (choice (string :tag "simple directory without path (-Q \"\") in 8.5, -I in 8.4") (list :tag - "recursive directory with path (-R ... -as ...)" + "recursive directory with path (-R ... ...)" (const rec) (string :tag "directory") (string :tag "log path")) - (list :tag - "recursive directory without recursive inport with path (-Q ... ...)" + (list :tag + "recursive directory without recursive import with path (-Q ... ...)" (const recnoimport) (string :tag "directory") (string :tag "log path")) (list :tag - "directory with empty logical path (-Q ... "" in coq>=8.5, -I ... in coq<=8.4)" + "compatibility for of -I (-I ... -as ... in coq<=8.4)" (const nonrec) (string :tag "directory") (string :tag "log path")) @@ -188,103 +231,136 @@ not the same (-I is for coq path). "If `t' let coqdep search the current directory too. Should be `t' for normal users. If `t' pass -Q dir \"\" to coqdep when processing files in directory \"dir\" in addition to any entries -in `coq-load-path'." +in `coq-load-path'. + +This setting is only relevant with Coq < 8.5." :type 'boolean :safe 'booleanp :group 'coq-auto-compile) -(defun coq-option-of-load-path-entry (entry) - "Translate a single element from `coq-load-path' into options. -See `coq-load-path' for the possible forms of entry and to which -options they are translated." - (cond - ((and coq-pre-v85 (stringp entry)) - (list "-I" (expand-file-name entry))) - ((and (not coq-pre-v85) (stringp entry)) - (list "-Q" (expand-file-name entry) "")) - ((and coq-pre-v85 (eq (car entry) 'nonrec)) - (list "-I" (expand-file-name (nth 1 entry)) "-as" (nth 2 entry))) - ((and (not coq-pre-v85) (eq (car entry) 'nonrec)) ;; N/A? - (list "-Q" (expand-file-name (nth 1 entry)) (nth 2 entry))) - ((eq (car entry) 'recnoimport) ;; only for >=8.5 - (list "-Q" (expand-file-name (nth 1 entry)) (nth 2 entry))) - (t - (if (eq (car entry) 'rec) - (setq entry (cdr entry))) - (if coq-pre-v85 ;; -as obsolete in 8.5 - (list "-R" (expand-file-name (car entry)) "-as" (nth 1 entry)) - (list "-R" (expand-file-name (car entry)) (nth 1 entry)))))) - -(defun coq-include-options (file coq-load-path) - "Build the list of include options for coqc, coqdep and coqtop. -The options list includes all entries from argument COQ-LOAD-PATH +(make-obsolete-variable 'coq-load-path-include-current "Coq 8.5 does not need it" "4.3") + +(defun coq-option-of-load-path-entry (entry &optional pre-v85) + "Translate a single ENTRY from `coq-load-path' into options. +See `coq-load-path' for the possible forms of ENTRY and to which +options they are translated. Use a non-nil PRE-V85 flag to +request compatibility handling of flags." + (if pre-v85 + ;; FIXME Which base directory do we expand against? Should the entries of + ;; load-path just always be absolute? + ;; NOTE we don't handle 'recnoimport in 8.4, and we don't handle 'nonrec + ;; in 8.5. + (pcase entry + ((or (and (pred stringp) dir) `(ocamlimport ,dir)) + (list "-I" (expand-file-name dir))) + (`(nonrec ,dir ,alias) + (list "-I" (expand-file-name dir) "-as" alias)) + ((or `(rec ,dir ,alias) `(,dir ,alias)) + (list "-R" (expand-file-name dir) alias))) + (pcase entry + ((and (pred stringp) dir) + (list "-Q" (expand-file-name dir) "")) + (`(ocamlimport ,dir) + (list "-I" (expand-file-name dir))) + (`(recnoimport ,dir ,alias) + (list "-Q" (expand-file-name dir) alias)) + ((or `(rec ,dir ,alias) `(,dir ,alias)) + (list "-R" (expand-file-name dir) alias))))) + +(defun coq-include-options (load-path &optional current-directory pre-v85) + "Build the base list of include options for coqc, coqdep and coqtop. +The options list includes all entries from argument LOAD-PATH \(which should be `coq-load-path' of the buffer that invoked the compilation) prefixed with suitable options and (for coq<8.5), if `coq-load-path-include-current' is enabled, the directory base of -FILE. The resulting list is fresh for every call, callers can +FILE. The resulting list is fresh for every call, callers can append more arguments with `nconc'. -FILE should be an absolute file name. It can be nil if -`coq-load-path-include-current' is nil." - (let ((result nil)) - (unless (coq-load-path-safep coq-load-path) - (error "Invalid value in coq-load-path")) - (when coq-load-path - (setq result (coq-option-of-load-path-entry (car coq-load-path))) - (dolist (entry (cdr coq-load-path)) - (nconc result (coq-option-of-load-path-entry entry)))) - (if coq-load-path-include-current - (setq result - (if coq-pre-v85 - (cons "-I" (cons (file-name-directory file) result)) - ;; from coq-8.5 beta3 cpqdep does not needthis anymore - ;; and actually it can clash with -Q . foo written in - ;; _CoqProject - ;; (cons "-Q" (cons (file-name-directory file) (cons "" result))) - result))) - result)) - - - -(defun coq-coqdep-prog-args (&optional src-file loadpath) - (let ((loadpath (or loadpath coq-load-path))) - (coq-include-options src-file loadpath))) - -(defun coq-coqc-prog-args (&optional src-file loadpath) +CURRENT-DIRECTORY should be an absolute directory name. It can be nil if +`coq-load-path-include-current' is nil. + +A non-nil PRE-V85 flag requests compatibility handling of flags." + (unless (coq-load-path-safep load-path) + (error "Invalid value in coq-load-path")) + (when (and pre-v85 coq-load-path-include-current) + (cl-assert current-directory) + (push current-directory load-path)) + (cl-loop for entry in load-path + append (coq-option-of-load-path-entry entry pre-v85))) + +(defun coq--options-test-roundtrip-1 (coq-project parsed pre-v85) + "Run a sanity check on COQ-PROJECT's PARSED options. +If PRE-V85 is non-nil, use compatibility mode." + (let* ((concatenated (apply #'append parsed)) + (coq-load-path-include-current nil) + (extracted (coq--extract-load-path parsed nil)) + (roundtrip (coq-include-options extracted nil pre-v85))) + (princ (format "[%s] with compatibility flag set to %S: " coq-project pre-v85)) + (if (equal concatenated roundtrip) + (princ "OK\n") + (princ (format "Failed.\n:: Original: %S\n:: LoadPath: %S\n:: Roundtrip: %S\n" + concatenated extracted roundtrip))))) + +(defun coq--options-test-roundtrip (coq-project &optional v85-only) + "Run a sanity check on COQ-PROJECT. +If V85-ONLY is non-nil, do not check the compatibility code." + (let ((parsed (coq--read-options-from-project-file coq-project))) + (coq--options-test-roundtrip-1 coq-project parsed nil) + (unless v85-only + (coq--options-test-roundtrip-1 coq-project parsed t)))) + +(defun coq--options-test-roundtrips () + "Run sanity tests on coq-project parsing code. +More precisely, check that parsing and reprinting the include +options of a few coq-project files does the right thing." + (with-output-to-temp-buffer "*tests*" + (coq--options-test-roundtrip "-Q /test Test") + (coq--options-test-roundtrip "-Q /test \"\"") + (coq--options-test-roundtrip "-R /test Test") + (coq--options-test-roundtrip "-I /test"))) + +(defun coq-coqdep-prog-args (load-path &optional current-directory pre-v85) + "Build a list of options for coqdep. +LOAD-PATH, CURRENT-DIRECTORY, PRE-V85: see `coq-include-options'." + (coq-include-options load-path current-directory pre-v85)) + +;;; !!! Fixme handle proof-prog-name-ask + +(defun coq-coqc-prog-args (load-path &optional current-directory pre-v85) + "Build a list of options for coqc. +LOAD-PATH, 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. - (let ((coqdep-args - (let ((coq-load-path-include-current nil)) ; obsolete >=8.5beta3 - ;; by the time this function is called, coq-prog-args should be set - (append coq-prog-args - (coq-coqdep-prog-args src-file loadpath))))) - (remove "-emacs" (remove "-emacs-U" coqdep-args)))) + (append (remove "-emacs" (remove "-emacs-U" coq-prog-args)) + (let ((coq-load-path-include-current nil)) ; Not needed in >=8.5beta3 + (coq-coqdep-prog-args coq-load-path 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. -(defun coq-coqtop-prog-args (&optional src-file loadpath) +(defun coq-coqtop-prog-args (load-path &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. - (cons "-emacs" (coq-coqc-prog-args src-file loadpath))) - -;; FIXME: we seem to need this function with this exact name, -;; otherwise coqtop command is not generated with the good load-path -;; (??). Is it interfering with defpgcustom's in pg-custom.el? -(defun coq-prog-args () (coq-coqtop-prog-args)) - + "Build a list of options for coqc. +LOAD-PATH, CURRENT-DIRECTORY, PRE-V85: see `coq-coqc-prog-args'." + (cons "-emacs" (coq-coqc-prog-args load-path current-directory pre-v85))) +(defun coq-prog-args () + "Recompute `coq-load-path' before calling `coq-coqtop-prog-args'." + (coq-load-project-file) + (coq-autodetect-version) + (coq-coqtop-prog-args coq-load-path)) (defcustom coq-use-project-file t "If t, when opening a coq file read the dominating _CoqProject. -If t when a coq file is opened, proofgeneral will look for a +If t, when a coq file is opened, Proof General will look for a project file (see `coq-project-filename') somewhere in the -current directory or its parents directory. If there is one, its -content is read and used to determine the arguments that must be -given to coqtop. In particular it sets the load path (including -the -R lib options) (see `coq-load-path') ." +current directory or its parent directories. If there is one, +its contents are read and used to determine the arguments that +must be given to coqtop. In particular it sets the load +path (including the -R lib options) (see `coq-load-path') ." :type 'boolean :group 'coq) @@ -293,10 +369,10 @@ the -R lib options) (see `coq-load-path') ." The coq project file of a coq developpement (Cf Coq documentation on \"makefile generation\") should contain the arguments given to coq_makefile. In particular it contains the -I and -R -options (one per line). If `coq-use-coqproject' is t (default) -the content of this file will be used by proofgeneral to infer -the `coq-load-path' and the `coq-prog-args' variables that set -the coqtop invocation by proofgeneral. This is now the +options (preferably one per line). If `coq-use-coqproject' is +t (default) the content of this file will be used by proofgeneral +to infer the `coq-load-path' and the `coq-prog-args' variables +that set the coqtop invocation by proofgeneral. 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 @@ -304,122 +380,121 @@ project file settings." :type 'string :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." - (let* ( - (projectfiledir (locate-dominating-file buffer-file-name coq-project-filename))) - (when projectfiledir - (let* ((projectfile (expand-file-name coq-project-filename 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)) - (projectbuffer (or projectbufferalreadyopen - (find-file-noselect projectfile t t)))) - (list projectbuffer projectbufferalreadyopen))))) - -;; No "." no "-" in coq module file names, but we do not check -;; TODO: look exactly at what characters are allowed. -(defconst coq-load-path--R-regexp - "\\_<-R\\s-+\\(?1:[^[:space:]]+\\)\\s-+\\(?2:[^[:space:]]+\\)") - -(defconst coq-load-path--Q-regexp - "\\_<-Q\\s-+\\(?1:[^[:space:]]+\\)\\s-+\\(?2:[^[:space:]]+\\)") - -;; second arg of -I is optional (and should become obsolete one day) -(defconst coq-load-path--I-regexp - "\\_<-I\\s-+\\(?1:[^[:space:]]+\\)\\(?:[:space:]+\\(?2:[^[:space:]]+\\)\\)?") - -;(defconst coq-load-path--I-regexp "\\_<-I\\s-+\\(?1:[^[:space:]]+\\)") - -;; match-string 1 must contain the string to add to coqtop command line, so we -;; ignore -arg, we use numbered subregexpr. - -;; FIXME: if several options are given (within "") in a single -arg line, then -;; they are glued and passed as a single argument to coqtop. this is bad and -;; not conforming to coq_makefile. HOWEVER: this is probably a bad feature of -;; coq_makefile to allow several arguments in a single - arg "xxx yyy". -(defconst coq-prog-args-regexp - "\\_<\\(?1:-opt\\|-byte\\)\\|-arg[[:space:]]+\\(?:\\(?1:[^\"\t\n#]+\\)\\|\"\\(?1:[^\"]+\\)\"\\)") - - -(defun coq-read-option-from-project-file (projectbuffer regexp &optional dirprefix) - "look for occurrences of regexp in buffer projectbuffer and collect subexps. -The returned sub-regexp are the one numbered 1 and 2 (other ones -should be unnumbered). If there is only subexp 1 then it is added -as is to the final list, if there are 1 and 2 then a list -containing both is added to the final list. If optional DIRPREFIX -is non nil, then options ar considered as directory or file names -and will be made absolute from directory named DIRPREFIX. This -allows to call coqtop from a subdirectory of the project." - (let ((opt nil)) - (when projectbuffer - (with-current-buffer projectbuffer - (goto-char (point-min)) - (while (re-search-forward regexp nil t) - (let* ((firstfname (match-string 1)) - (second (match-string 2)) - (first (if (null dirprefix) firstfname - (expand-file-name firstfname dirprefix)))) - (if second ; if second arg is "" (two doublequotes), it means empty string - (let ((sec (if (string-equal second "\"\"") "" second))) - (if (string-match coq-load-path--R-regexp (match-string 0)) - (setq opt (cons (list first sec) opt)) - (setq opt (cons (list 'recnoimport first sec) opt)))) - (setq opt (cons first opt)))))) - (reverse opt)))) - -;; Look for -R and -I options in the project buffer -;; add the default "." too -(defun coq-search-load-path (projectbuffer) - "Read project buffer and retrurn a value for `coq-load-path'." -;; no automatic insertion of "." here because some people want to do "-R . foo" so -;; let us avoid conflicts. - (coq-read-option-from-project-file - projectbuffer - (concat coq-load-path--R-regexp "\\|" coq-load-path--Q-regexp "\\|" coq-load-path--I-regexp) - (file-name-directory (buffer-file-name projectbuffer)))) - -;; Look for other options (like -opt, -arg foo etc) in the project buffer -;; adds the -emacs option too -(defun coq-search-prog-args (projectbuffer) - "Read project buffer and retrurn a value for `coq-prog-args'" - (cons - "-emacs" - (coq-read-option-from-project-file projectbuffer coq-prog-args-regexp))) - + (when buffer-file-name + (let* ((projectfiledir (locate-dominating-file buffer-file-name coq-project-filename))) + (when projectfiledir + (let* ((projectfile (expand-file-name coq-project-filename 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)) + (projectbuffer (or projectbufferalreadyopen + (find-file-noselect projectfile t t)))) + (list projectbuffer projectbufferalreadyopen)))))) + +(defconst coq--project-file-separator "[\r\n[:space:]]+") + +(defconst coq--makefile-switch-arities + '(("-R" . 2) + ("-Q" . 2) + ("-I" . 1) + ("-arg" . 1) + ("-opt" . 0) + ("-byte" . 0))) + +(defun coq--read-one-option-from-project-file (switch arity raw-args) + "Cons SWITCH with ARITY arguments from RAW-ARGS. +If ARITY is nil, return SWITCH." + (if arity + (let ((arguments + (condition-case-unless-debug nil + (cl-subseq raw-args 0 arity) + (warn "Invalid _CoqProject: not enough arguments for %S" switch)))) + (cons switch arguments)) + 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)) + (options nil)) + (while raw-args + (let* ((switch (pop raw-args)) + (arity (cdr (assoc switch coq--makefile-switch-arities)))) + (push (coq--read-one-option-from-project-file switch arity raw-args) options) + (setq raw-args (nthcdr (or arity 0) raw-args)))) + options)) + +(defun coq--extract-prog-args (options) + "Extract coqtop arguments from _CoqProject options OPTIONS. +OPTIONS is a list or conses (switch . argument) and strings. +Note that the semantics of the -arg flags in coq project files +are weird: -arg \"a b\" means pass a and b, separately, to +coqtop." + (let ((args nil)) + (dolist (opt options) + (pcase opt + ((or "-byte" "-op") + (push opt args)) + (`("-arg" ,concatenated-args) + (setq args + (append (split-string (cadr opt) coq--project-file-separator) + args))))) + (cons "-emacs" args))) + +(defun coq--extract-load-path-1 (option base-directory) + "Convert one _CoqProject OPTION, relative to BASE-DIRECTORY." + (pcase option + (`("-I" ,path) + (list 'ocamlimport (expand-file-name path base-directory))) + (`("-R" ,path ,alias) + (list 'rec (expand-file-name path base-directory) alias)) + (`("-Q" ,path ,alias) + (list 'recnoimport (expand-file-name path base-directory) alias)))) + +(defun coq--extract-load-path (options base-directory) + "Extract loadpath from _CoqProject options OPTIONS. +OPTIONS is a list or conses (switch . arguments) and strings. +Paths are taken relative to BASE-DIRECTORY." + (cl-loop for opt in options + for extracted = (coq--extract-load-path-1 opt base-directory) + when extracted collect extracted)) ;; optional args allow to implement the precedence of dir/file local vars (defun coq-load-project-file-with-avoid (&optional avoidargs avoidpath) - (let* ((projectbuffer-aux (coq-find-project-file)) - (projectbuffer (and projectbuffer-aux (car projectbuffer-aux))) - (no-kill (and projectbuffer-aux (car (cdr projectbuffer-aux))))) - (if (not projectbuffer-aux) + "Set `coq-prog-args' and `coq-load-path' from _CoqProject. +If AVOIDARGS or AVOIDPATH is set, do not set the corresponding +variable." + (pcase-let* ((`(,proj-file-buf ,no-kill) (coq-find-project-file))) + (if (not proj-file-buf) (message "Coq project file not detected.") - (unless avoidargs (setq coq-prog-args (coq-search-prog-args projectbuffer))) - (unless avoidpath (setq coq-load-path (coq-search-load-path projectbuffer))) - (let ((msg - (cond - ((and avoidpath avoidargs) "Coqtop args and load path") - (avoidpath "Coqtop load path") - (avoidargs "Coqtop args") - (t "")))) - (message - "Coq project file detected: %s%s." (buffer-file-name projectbuffer) - (if (or avoidpath avoidargs) - (concat "\n(" msg " overridden by dir/file local values)") - ""))) - (when coq-debug - (message "coq-prog-args: %S" coq-prog-args) - (message "coq-load-path: %S" coq-load-path)) - (unless no-kill (kill-buffer projectbuffer))))) - - + (let* ((contents (with-current-buffer proj-file-buf (buffer-string))) + (options (coq--read-options-from-project-file contents)) + (proj-file-name (buffer-file-name proj-file-buf)) + (proj-file-dir (file-name-directory proj-file-name))) + (unless avoidargs (setq coq-prog-args (coq--extract-prog-args options))) + (unless avoidpath (setq coq-load-path (coq--extract-load-path options proj-file-dir))) + (let ((msg + (cond + ((and avoidpath avoidargs) "Coqtop args and load path") + (avoidpath "Coqtop load path") + (avoidargs "Coqtop args") + (t "")))) + (message + "Coq project file detected: %s%s." proj-file-name + (if (or avoidpath avoidargs) + (concat "\n(" msg " overridden by dir/file local values)") + ""))) + (when coq-debug + (message "coq-prog-args: %S" coq-prog-args) + (message "coq-load-path: %S" coq-load-path)) + (unless no-kill (kill-buffer proj-file-buf)))))) (defun coq-load-project-file () "Set `coq-prog-args' and `coq-load-path' according to _CoqProject file. -Obeys `coq-use-project-file'. Note that if a variable is already +Obeys `coq-use-project-file'. Note that if a variable is already set by dir/file local variables, this function will not override its value. See `coq-project-filename' to change the name of the @@ -434,9 +509,7 @@ feature." (defun coq-load-project-file-rehack () "Reread file/dir local vars and call `coq-load-project-file'. -Does nothing if `coq-use-project-file' is nil. -Warning: -" +Does nothing if `coq-use-project-file' is nil." (when coq-use-project-file ;; Let us reread dir/file local vars, in case the user mmodified them (hack-local-variables) @@ -502,11 +575,11 @@ then be set using local file variables." 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)))) + (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 ../.. @@ -169,13 +169,14 @@ See also `coq-hide-additional-subgoals'." (defcustom coq-navigation-command-regexp (concat "^\\(\\(Focus\\)\\|\\(Unfocus\\)\\|" + "\\(all\\s-*:\\s-*\\(cycle\\|swap\\|revgoals\\)\\)\\|" "\\(\\+\\)\\|\\(-\\)\\|\\(\\*\\)\\|\\({\\)\\|\\(}\\)\\)") "Regexp for `proof-tree-navigation-command-regexp'." :type 'regexp :group 'coq-proof-tree) (defcustom coq-proof-tree-cheating-regexp - "admit" + "\\(?:admit\\)\\|\\(?:give_up\\)" "Regexp for `proof-tree-cheating-regexp'." :type 'regexp :group 'coq-proof-tree) @@ -187,8 +188,9 @@ See also `coq-hide-additional-subgoals'." :group 'coq-proof-tree) (defcustom coq-proof-tree-current-goal-regexp - (concat "^[0-9]+ \\(?:focused \\)?subgoal\\(?:s\\)?" - "\\(?: (unfocused: [-0-9]+)\\)?\\(?:\\s-*, subgoal 1\\)? " + (concat "^[0-9]+ \\(?:focused \\)?subgoal\\(?:s\\)?\\s-*" + "\\(?:(\\(?:unfocused: [-0-9]+\\)?,?" + "\\s-*\\(?:shelved: [-0-9]+\\)?)\\)?\\(?:\\s-*, subgoal 1\\)? " "(ID \\([0-9]+\\))\n\\s-*\n\\(\\(?: .*\n\\)+\\)\\(?:\n\\|$\\)") "Regexp for `proof-tree-current-goal-regexp'." :type 'regexp @@ -229,13 +231,26 @@ See also `coq-hide-additional-subgoals'." :type 'regexp :group 'coq-proof-tree) -;; pc: <infomsg> now has a newline (better output indentation) +;; 8.4: +;; <infomsg>This subproof is complete, but there are still unfocused goals.</infomsg> +;; +;; 8.5: +;; <infomsg> +;; This subproof is complete, but there are some unfocused goals. +;; Focus next goal with bullet *. +;; </infomsg> +;; +;; <infomsg>No more subgoals, but there are some goals you gave up:</infomsg> +;; +;; <infomsg>All the remaining goals are on the shelf.</infomsg> (defcustom coq-proof-tree-branch-finished-regexp - (concat "^\\(\\(?:Proof completed\\.\\)\\|\\(?:No more subgoals\\.\\)\\|" + (concat "^\\(\\(?:Proof completed\\.\\)\\|" + "\\(?:\\(?:<infomsg>\\)?No more subgoals\\)\\|" "\\(No more subgoals but non-instantiated " "existential variables:\\)\\|" + "\\(?:<infomsg>All the remaining goals are on the shelf\\)\\|" "\\(<infomsg>\\s-*This subproof is complete, but there are " - "still unfocused goals.\\s-*</infomsg>\\)\\)") + "\\(?:still\\|some\\) unfocused goals.\\)\\)") "Regexp for `proof-tree-branch-finished-regexp'." :type 'regexp :group 'coq-proof-tree) @@ -1810,6 +1825,11 @@ processing, the sequent text is send to prooftree as a sequent update (see `proof-tree-update-sequent') and the ID of the sequent is registered as known in `proof-tree-sequent-hash'. +Searching for new subgoals must only be done when the proof is +not finished, because Coq 8.5 lists open existential variables +as (new) open subgoals. For this test we assume that +`proof-marker' has not yet been moved. + The not yet delayed output is in the region \[proof-shell-delayed-output-start, proof-shell-delayed-output-end]." ;; (message "CPTGNS start %s end %s" @@ -1818,19 +1838,27 @@ The not yet delayed output is in the region (with-current-buffer proof-shell-buffer (let ((start proof-shell-delayed-output-start) (end proof-shell-delayed-output-end)) - (goto-char start) - (while (proof-re-search-forward - coq-proof-tree-additional-subgoal-ID-regexp end t) - (let ((subgoal-id (match-string-no-properties 1))) - (unless (gethash subgoal-id proof-tree-sequent-hash) - (setq proof-action-list - (cons (proof-shell-action-list-item - (coq-show-sequent-command subgoal-id) - (proof-tree-make-show-goal-callback (car proof-info)) - '(no-goals-display - no-response-display - proof-tree-show-subgoal)) - proof-action-list)))))))) + ;; The message "All the remaining goals are on the shelf" is processed as + ;; urgent message and is therefore before + ;; proof-shell-delayed-output-start. We therefore need to go back to + ;; proof-marker. + (goto-char proof-marker) + (unless (proof-re-search-forward + coq-proof-tree-branch-finished-regexp end t) + (goto-char start) + (while (proof-re-search-forward + coq-proof-tree-additional-subgoal-ID-regexp end t) + (let ((subgoal-id (match-string-no-properties 1))) + (unless (gethash subgoal-id proof-tree-sequent-hash) + (message "CPTGNS new sequent %s found" subgoal-id) + (setq proof-action-list + (cons (proof-shell-action-list-item + (coq-show-sequent-command subgoal-id) + (proof-tree-make-show-goal-callback (car proof-info)) + '(no-goals-display + no-response-display + proof-tree-show-subgoal)) + proof-action-list))))))))) (add-hook 'proof-tree-urgent-action-hook 'coq-proof-tree-get-new-subgoals) @@ -2047,7 +2075,7 @@ Warning: this makes the error messages (and location) wrong.") (cond ((string-match ";" s) s) ;; composed tactic cannot be treated ((string-match coq-auto-as-hack-hyp-name-regex s) - (concat "infoH " (match-string 1 s) " !" (match-string 2 s) ".")) + (concat "infoH " (match-string 1 s) " (" (match-string 2 s) ").")) ((string-match coq-keywords-accepting-as-regex s) (concat "infoH " s)) (t (concat "infoH " s)))) diff --git a/doc/Makefile.doc b/doc/Makefile.doc index 87e1d1cb..b5eb4d82 100644 --- a/doc/Makefile.doc +++ b/doc/Makefile.doc @@ -18,7 +18,7 @@ MAKE = make -f Makefile.doc MAKEINFO = makeinfo -TEXI2HTML = texi2html -expandinfo -number -split_chapter --noheader --css-include proofgen.css +TEXI2HTML = texi2html -expandinfo -number-sections -split_chapter --noheader --css-include proofgen.css # `texinfo-tex' package contains texi2pdf TEXI2PDF = texi2pdf # `dviutils' package contains these useful utilities. diff --git a/etc/ProofGeneral.spec b/etc/ProofGeneral.spec index 5e812fdb..1543949a 100644 --- a/etc/ProofGeneral.spec +++ b/etc/ProofGeneral.spec @@ -1,6 +1,6 @@ Summary: Proof General, Emacs interface for Proof Assistants Name: ProofGeneral -Version: 4.3pre150313 +Version: 4.4pre Release: 1 Group: Text Editors/Integrated Development Environments (IDE) License: GPL diff --git a/generic/proof-site.el b/generic/proof-site.el index 521a8d8c..11d84715 100644 --- a/generic/proof-site.el +++ b/generic/proof-site.el @@ -71,8 +71,8 @@ ;; (eval-and-compile -;; WARNING: do not edit next line (constant is edited in Makefile.devel) - (defconst proof-general-version "Proof General Version 4.3pre150313. Released by da." + ;; WARNING: do not edit next line (constant is edited in Makefile.devel) + (defconst proof-general-version "Proof General Version 4.4pre." "Version string identifying Proof General release.")) (defconst proof-general-short-version |