diff options
| -rw-r--r-- | coq/ex/test-cases/README | 12 | ||||
| -rw-r--r-- | coq/ex/test-cases/retract-completely-asserted/.cvsignore | 2 | ||||
| -rw-r--r-- | coq/ex/test-cases/retract-completely-asserted/README | 20 | ||||
| -rw-r--r-- | coq/ex/test-cases/retract-completely-asserted/a.v | 4 | ||||
| -rw-r--r-- | coq/ex/test-cases/retract-completely-asserted/b.v | 4 | ||||
| -rw-r--r-- | coq/ex/test-cases/retract-completely-asserted/c.v | 9 | ||||
| -rw-r--r-- | doc/.cvsignore | 1 | ||||
| -rw-r--r-- | doc/PG-adapting.texi | 41 | ||||
| -rw-r--r-- | generic/proof-config.el | 13 | ||||
| -rw-r--r-- | generic/proof-script.el | 8 |
10 files changed, 104 insertions, 10 deletions
diff --git a/coq/ex/test-cases/README b/coq/ex/test-cases/README new file mode 100644 index 00000000..62081521 --- /dev/null +++ b/coq/ex/test-cases/README @@ -0,0 +1,12 @@ +This directory contains test cases for coq ProofGeneral, +especially for its multi-file support. + +Each test case is in one subdirectory. Each such subdirectory has +a README file, describing the test case. + + +Overview of the test cases: + +retract-completely-asserted + test how proof-no-fully-processed-buffer retracts fully + asserted buffers diff --git a/coq/ex/test-cases/retract-completely-asserted/.cvsignore b/coq/ex/test-cases/retract-completely-asserted/.cvsignore new file mode 100644 index 00000000..480bc6d5 --- /dev/null +++ b/coq/ex/test-cases/retract-completely-asserted/.cvsignore @@ -0,0 +1,2 @@ +*.vo +*.glob diff --git a/coq/ex/test-cases/retract-completely-asserted/README b/coq/ex/test-cases/retract-completely-asserted/README new file mode 100644 index 00000000..68cca029 --- /dev/null +++ b/coq/ex/test-cases/retract-completely-asserted/README @@ -0,0 +1,20 @@ +In coq different modules may contain definition with the same +name, because for coq they have different "absolute names" because +they are in different modules. + +To provoke an error inside ProofGeneral on correct coq input, +do the following: +- Visit a.v and script the initial comment. +- Set proof-no-fully-processed-buffer to nil. +- assert buffer a.v completely +- switch to b.v +- scripting "Definition a" in b.v will give the error "a already + exists" + +Now retract a.v, set proof-no-fully-processed-buffer to t and try +again. + +To see that the example is indeed valid, script c.v. (For c.v you +either have to switch coq-recompile-before-require to t or you +have to compile modules a and b yourself with "coqc a" and "coqc b".) + diff --git a/coq/ex/test-cases/retract-completely-asserted/a.v b/coq/ex/test-cases/retract-completely-asserted/a.v new file mode 100644 index 00000000..ea9a099d --- /dev/null +++ b/coq/ex/test-cases/retract-completely-asserted/a.v @@ -0,0 +1,4 @@ + +(* The following defines the absolut name a.a *) + +Definition a := 0.
\ No newline at end of file diff --git a/coq/ex/test-cases/retract-completely-asserted/b.v b/coq/ex/test-cases/retract-completely-asserted/b.v new file mode 100644 index 00000000..d07522ba --- /dev/null +++ b/coq/ex/test-cases/retract-completely-asserted/b.v @@ -0,0 +1,4 @@ + +(* The following defines the absolute name b.a *) + +Definition a := 1.
\ No newline at end of file diff --git a/coq/ex/test-cases/retract-completely-asserted/c.v b/coq/ex/test-cases/retract-completely-asserted/c.v new file mode 100644 index 00000000..bd82b351 --- /dev/null +++ b/coq/ex/test-cases/retract-completely-asserted/c.v @@ -0,0 +1,9 @@ + +Require Import a. +Require Import b. + +(* b.a hides a.a, therefore the partial name "a" refers to b.a *) +Print a. + +(* a.a is available under its longer name *) +Print a.a.
\ No newline at end of file diff --git a/doc/.cvsignore b/doc/.cvsignore index c667379c..1e54881b 100644 --- a/doc/.cvsignore +++ b/doc/.cvsignore @@ -20,6 +20,7 @@ ProofGeneral.info-* ProofGeneral.txt ProofGeneral PG-adapting +PG-adapting.log PG-adapting.dvi PG-adapting.ps PG-adapting.pdf diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index 63d3c697..c774200f 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -666,6 +666,7 @@ the behaviour of script management. * Safe (state-preserving) commands:: * Activate scripting hook:: * Automatic multiple files:: +* Completely asserted buffers:: * Completions:: @end menu @@ -1219,6 +1220,38 @@ file dependencies then you should configure it to communicate with Proof General about the dependencies rather than using this setting. @end defvar +@node Completely asserted buffers +@section Completely asserted buffers + +When switching scripting from buffer A to buffer B Proof General +normally offers the choice of either completely retracting or +completely asserting buffer A. The option to completely assert +buffer A is offered, because the material in B may depend on A. +Even if B does not depend on A, it does no harm if one keeps the +development of A loaded in the proof assistant. This observation +is true for many proof assistants. + +One exception is Coq. Assume file B depends on file A. When Coq +processes B it does not read the sources of A. Instead it loads a +compiled object representation of A. Therefore, when switching +from A to B, it does make no sense to keep the material of A +loaded in the proof assistant. For Coq, the material of A may +even provoke errors on correct input. Therefore, for coq, the +right behaviour is to completely retract buffer A before +switching to B. + +@c TEXI DOCSTRING MAGIC: proof-no-fully-processed-buffer +@defvar proof-no-fully-processed-buffer +Set to t if buffers should always retract before scripting elsewhere.@* +Leave at nil if fully processd buffers make sense for the current +proof assistant. If nil the user can choose to fully assert a +buffer when starting scripting in a different buffer. If t there +is only the choice to fully retract the active buffer before +starting scripting in a different buffer. This last behavior is +needed for Coq. +@end defvar + + @node Completions @section Completions @@ -3085,7 +3118,13 @@ We make sure that the active scripting buffer either has no locked region or a full locked region (everything in it has been processed). If this is not already the case, we question the user whether to retract or assert, or automatically take the action indicated in the -user option @samp{@code{proof-auto-action-when-deactivating-scripting}.} +user option @samp{@code{proof-auto-action-when-deactivating-scripting}}. + +If @samp{@code{proof-no-fully-processed-buffer}} is t there is only the choice +to fully retract the active scripting buffer. In this case the +active scripting buffer is retract even if it was fully processed. +Setting @samp{@code{proof-auto-action-when-deactivating-scripting}} to @code{'process} +is ignored in this case. If the scripting buffer is (or has become) fully processed, and it is associated with a file, it is registered on diff --git a/generic/proof-config.el b/generic/proof-config.el index f93235d4..cf090aa1 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -51,7 +51,7 @@ ;; ;; i. When adding a new configuration variable, please ;; (a) put it in the right customize group, and -;; (b) add a magical comment in ProofGeneral.texi/PG-Adapting.texi +;; (b) add a magical comment in ProofGeneral.texi/PG-adapting.texi ;; ;; ii. Presently the customize library seems a bit picky over the ;; :type property and some correct but complex types don't work: @@ -667,6 +667,17 @@ assistant, for example, to compile a completed file." :type '(repeat function) :group 'proof-script) +(defcustom proof-no-fully-processed-buffer nil + "Set to t if buffers should always retract before scripting elsewhere. +Leave at nil if fully processd buffers make sense for the current +proof assistant. If nil the user can choose to fully assert a +buffer when starting scripting in a different buffer. If t there +is only the choice to fully retract the active buffer before +starting scripting in a different buffer. This last behavior is +needed for Coq." + :type 'boolean + :group 'proof-script) + (defcustom proof-script-evaluate-elisp-comment-regexp "ELISP: -- \\(.*\\) --" "Matches text within a comment telling Proof General to evaluate some code. This allows Emacs Lisp to be executed during scripting. diff --git a/generic/proof-script.el b/generic/proof-script.el index 2c2c760d..2db38563 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -969,14 +969,6 @@ retracted using `proof-auto-retract-dependencies'." ;; taken when scripting is turned off/on. ;; -(defconst proof-no-fully-processed-buffer nil - "Set to t if buffers should always retract before scripting elsewhere. -Leave at nil if fully processd buffers make sense for the current proof -assistant. If nil the user can choose to fully assert a buffer when -starting scripting in a different buffer. If t there is only to choice -to fully retract the active buffer before starting scripting in a different -buffer. This last behavior is needed for Coq.") - (defun proof-protected-process-or-retract (action &optional buffer) "If ACTION='process, process, If ACTION='retract, retract. Process or retract the current buffer, which should be the active |