diff options
| -rw-r--r-- | CHANGES | 5 | ||||
| -rw-r--r-- | coq/coq.el | 2 | ||||
| -rw-r--r-- | demoisa/demoisa-easy.el | 3 | ||||
| -rw-r--r-- | demoisa/demoisa.el | 2 | ||||
| -rw-r--r-- | generic/proof-config.el | 28 | ||||
| -rw-r--r-- | generic/proof-shell.el | 122 | ||||
| -rw-r--r-- | hol98/hol98.el | 6 | ||||
| -rw-r--r-- | isa/BUGS | 7 | ||||
| -rw-r--r-- | isa/isa.el | 11 | ||||
| -rw-r--r-- | lego/lego.el | 2 | ||||
| -rw-r--r-- | plastic/plastic.el | 2 | ||||
| -rw-r--r-- | todo | 24 |
12 files changed, 94 insertions, 120 deletions
@@ -21,12 +21,15 @@ ** Coq Changes - ** LEGO Changes ** Isabelle Changes +*** Fix for stack overflow in regexp which occurred with large proof states + ** Isar Changes ** Changes for developers to note +*** No need for match string 1 in proof-shell-proof-completed + @@ -72,7 +72,7 @@ (defvar coq-shell-abort-goal-regexp "Current goal aborted" "*Regexp indicating that the current goal has been abandoned.") -(defvar coq-shell-proof-completed-regexp "\\(Subtree proved!\\)" +(defvar coq-shell-proof-completed-regexp "Subtree proved!" "*Regular expression indicating that the proof has been completed.") (defvar coq-goal-regexp diff --git a/demoisa/demoisa-easy.el b/demoisa/demoisa-easy.el index f4cb30c9..cac8afae 100644 --- a/demoisa/demoisa-easy.el +++ b/demoisa/demoisa-easy.el @@ -48,8 +48,7 @@ "\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception- " proof-shell-init-cmd "fun pg_repeat f 0 = () | pg_repeat f n = (f(); pg_repeat f (n-1));" - proof-shell-proof-completed-regexp - "\\(\\(.\\|\n\\)*No subgoals!\n\\)" + proof-shell-proof-completed-regexp "^No subgoals!" proof-shell-eager-annotation-start "^\\[opening \\|^###\\|^Reading") diff --git a/demoisa/demoisa.el b/demoisa/demoisa.el index 9cee59ca..b1f7e1c3 100644 --- a/demoisa/demoisa.el +++ b/demoisa/demoisa.el @@ -96,7 +96,7 @@ proof-shell-error-regexp "\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception- " proof-shell-start-goals-regexp "Level [0-9]" proof-shell-end-goals-regexp "val it" - proof-shell-proof-completed-regexp "\\(\\(.\\|\n\\)*No subgoals!\n\\)" + proof-shell-proof-completed-regexp "^No subgoals!" proof-shell-eager-annotation-start "^\\[opening \\|^###\\|^Reading" proof-shell-init-cmd ; define a utility function, in a lib somewhere? "fun pg_repeat f 0 = () diff --git a/generic/proof-config.el b/generic/proof-config.el index 4f0aeafd..707c0477 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1343,11 +1343,14 @@ It is safe to leave this variable unset (as nil)." (defcustom proof-shell-proof-completed-regexp nil "Regexp matching output indicating a finished proof. -Match number 1 should be the response text. -This is used to enable the QED function (save a proof) and -to control what output appears in the response buffer at the -end of a proof." +When output which matches this regexp is seen, we clear the goals +buffer in case this is not also marked up as a `goals' type of +message. + +We also enable the QED function (save a proof) and will automatically +close off the proof region if another goal appears before a save +command." :type '(choice nil regexp) :group 'proof-shell) @@ -1711,23 +1714,6 @@ for parsing the is disabled." :type 'character :group 'proof-goals) -;; FIXME: remove this setting for 3.2, by matching on -;; completed-regexp as an extra step, after errors/interrupt, -;; but as well as ordinary output. -(defcustom proof-goals-display-qed-message nil - "If non-nil, display the proof-completed message in the goals buffer. -For some proof assistants (e.g. Isabelle) it seems aesthetic to -display the QED message in the goals buffer, even though it doesn't -contain any goals and shouldn't be marked up for proof-by-pointing. - -If this setting is non-nil, QED messages appear in the goals -buffer. Otherwise they appear in the response buffer. - -This is a hack specially for Isabelle. DON'T USE IT. -It will be removed in a future version of Proof General." - :type 'boolean - :group 'proof-goals) - (defcustom proof-goals-font-lock-keywords nil "Value of font-lock-keywords used to fontify the goals output. NB: the goals output is not kept in font-lock-mode because the diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 78986fc7..5814172e 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -887,6 +887,7 @@ This is a hook function for proof-shell-handle-delayed-output-hook." "Like string-match except returns nil if REGEXP is nil." (and regexp (string-match regexp string))) + (defun proof-shell-process-output (cmd string) "Process shell output (resulting from CMD) by matching on STRING. CMD is the first part of the proof-action-list that lead to this @@ -920,67 +921,68 @@ This function can return one of 4 things as the symbol: 'error, 'interrupt, 'loopback, or nil. 'loopback means this was output from pbp, and should be inserted into the script buffer and sent back to the proof assistant." - (cond - ((proof-shell-string-match-safe proof-shell-interrupt-regexp string) - 'interrupt) - - ((proof-shell-string-match-safe proof-shell-error-regexp string) - (cons 'error (proof-shell-strip-special-annotations - (substring string - (match-beginning 0))))) - - ((proof-shell-string-match-safe proof-shell-abort-goal-regexp string) - (proof-clean-buffer proof-goals-buffer) - (setq proof-shell-delayed-output (cons 'insert "\nAborted\n")) - ()) - - ;; FIXME: remove proof-goals-display-qed-message setting in version 3.2, - ;; by matching on completed-regexp as an extra step again when a goal - ;; is found, or alternatively in same part as errors/interrupt - ;; (but that risks displaying no subgoals message twice in Isabelle!). - ;; We can also remove the match-string 1 mess too, modify every - ;; instance accordingly. - ((proof-shell-string-match-safe proof-shell-proof-completed-regexp string) - (proof-clean-buffer proof-goals-buffer) - (setq proof-shell-proof-completed 0) ; counts commands since proof complete. - (setq proof-shell-delayed-output - (cons (if proof-goals-display-qed-message - 'analyse 'insert) - (match-string 1 string)))) - - ((proof-shell-string-match-safe proof-shell-start-goals-regexp string) - (let ((start (match-end 0)) - end) - ;; Find the last goal string in the output - (while (string-match proof-shell-start-goals-regexp string start) - (setq start (match-end 0))) - ;; Ugly hack: provers with special characters don't include - ;; the match in their goals output. Others do. - (unless proof-shell-first-special-char - (setq start (match-beginning 0))) - (setq end (if proof-shell-end-goals-regexp - (string-match proof-shell-end-goals-regexp string start) - (length string))) - (setq proof-shell-delayed-output - (cons 'analyse (substring string start end))))) - + (or + ;; First check for error, interrupt, abort, proof completed + (cond + ((proof-shell-string-match-safe proof-shell-interrupt-regexp string) + 'interrupt) + + ((proof-shell-string-match-safe proof-shell-error-regexp string) + (cons 'error (proof-shell-strip-special-annotations + (substring string + (match-beginning 0))))) + + ((proof-shell-string-match-safe proof-shell-abort-goal-regexp string) + (proof-clean-buffer proof-goals-buffer) + (setq proof-shell-delayed-output (cons 'insert "\nAborted\n")) + ()) + + ((proof-shell-string-match-safe proof-shell-proof-completed-regexp string) + ;; In case no goals display + (proof-clean-buffer proof-goals-buffer) + ;; counter of commands since proof complete. + (setq proof-shell-proof-completed 0) + ;; But! We carry on matching below for goals output, so that + ;; provers may include proof completed message as part of + ;; goals message (Isabelle, HOL) or not (LEGO, Coq). + nil)) + + ;; Check for remaining things + (cond + ((proof-shell-string-match-safe proof-shell-start-goals-regexp string) + (let ((start (match-end 0)) + end) + ;; Find the last goal string in the output + (while (string-match proof-shell-start-goals-regexp string start) + (setq start (match-end 0))) + ;; Ugly hack: provers with special characters don't include + ;; the match in their goals output. Others do. + (unless proof-shell-first-special-char + (setq start (match-beginning 0))) + (setq end (if proof-shell-end-goals-regexp + (string-match proof-shell-end-goals-regexp string start) + (length string))) + (setq proof-shell-delayed-output + (cons 'analyse (substring string start end))))) + ;; Test for a proof by pointing command hint - ((proof-shell-string-match-safe proof-shell-result-start string) - (let (start end) - (setq start (+ 1 (match-end 0))) - (string-match proof-shell-result-end string) - (setq end (- (match-beginning 0) 1)) - (cons 'loopback (substring string start end)))) - - ;; Hook to tailor proof-shell-process-output to a specific proof - ;; system, in the case that all the above matches fail. - ((and proof-shell-process-output-system-specific - (funcall (car proof-shell-process-output-system-specific) - cmd string)) - (funcall (cdr proof-shell-process-output-system-specific) - cmd string)) - - (t (setq proof-shell-delayed-output (cons 'insert string))))) + ((proof-shell-string-match-safe proof-shell-result-start string) + (let (start end) + (setq start (+ 1 (match-end 0))) + (string-match proof-shell-result-end string) + (setq end (- (match-beginning 0) 1)) + (cons 'loopback (substring string start end)))) + + ;; Hook to tailor proof-shell-process-output to a specific proof + ;; system, in the case that all the above matches fail. + ((and proof-shell-process-output-system-specific + (funcall (car proof-shell-process-output-system-specific) + cmd string)) + (funcall (cdr proof-shell-process-output-system-specific) + cmd string)) + + ;; Finally, any other output will appear as a response. + (t (setq proof-shell-delayed-output (cons 'insert string)))))) ;; diff --git a/hol98/hol98.el b/hol98/hol98.el index d2774915..98dce6d0 100644 --- a/hol98/hol98.el +++ b/hol98/hol98.el @@ -57,11 +57,7 @@ ;; FIXME: add optional help topic parameter to help command. ;; Have patch ready for PG 3.2, but PG 3.1 is strictly bug fix. proof-info-command "help \"hol\"" - ;; FIXME: Isabelle has introduced a mess here, and we need to fix it. - ;; See comments in proof-shell.el and proof-config.el and todo - proof-goals-display-qed-message t - proof-shell-proof-completed-regexp - "\\(.*Initial goal proved\\(.\\|\n\\)*\\)" + proof-shell-proof-completed-regexp "Initial goal proved" ;; FIXME: next one needs setting so that "urgent" messages are displayed ;; eagerly from HOL. ;; proof-shell-eager-annotation-start @@ -5,13 +5,6 @@ See also ../BUGS for generic bugs. -** "Stack overflow in regexp". - -This problem is caused by a poor regexp and large proofstates. It -needs some small alterations to other proof assistant regexps, so will -be fixed in 3.2. In the meantime, a workaround is to reduce the -number of subgoals displayed. - ** set proof_timing is problematic It will make the goals display disappear during proof. This is @@ -190,14 +190,7 @@ and script mode." proof-shell-end-goals-regexp "\367" proof-shell-goal-char ?\370 - ;; FIXME da: this needs improvement. I don't know why just - ;; "No subgoals!" isn't enough. (Maybe anchored to end-goals - ;; for safety). At the moment, this regexp reportedly causes - ;; overflows with large proof states. - proof-shell-proof-completed-regexp - (concat proof-shell-start-goals-regexp - "\\(\\(.\\|\n\\)*\nNo subgoals!\n\\)" - proof-shell-end-goals-regexp) + proof-shell-proof-completed-regexp "^No subgoals!" ;; initial command configures Isabelle by hacking print functions. ;; FIXME: temporary hack for almost enabling/disabling printing. @@ -217,8 +210,6 @@ and script mode." ;; annotations, see isa-output-font-lock-keywords-1 proof-shell-leave-annotations-in-output t - proof-goals-display-qed-message t - ;; === ANNOTATIONS === ones here are broken proof-shell-result-start "\372 Pbp result \373" proof-shell-result-end "\372 End Pbp result \373" diff --git a/lego/lego.el b/lego/lego.el index 55b5fe98..896660d7 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -117,7 +117,7 @@ Activates extended printing routines required for Proof General.") "*Regular expression indicating that the proof of the current goal has been abandoned.") -(defvar lego-shell-proof-completed-regexp "\\(\\*\\*\\* QED \\*\\*\\*\\)" +(defvar lego-shell-proof-completed-regexp "\\*\\*\\* QED \\*\\*\\*" "*Regular expression indicating that the proof has been completed.") (defvar lego-save-command-regexp diff --git a/plastic/plastic.el b/plastic/plastic.el index ceefdd18..a4b0bf51 100644 --- a/plastic/plastic.el +++ b/plastic/plastic.el @@ -145,7 +145,7 @@ "*Regular expression indicating that the proof of the current goal has been abandoned.") -(defvar plastic-shell-proof-completed-regexp "\\(\\*\\*\\* QED \\*\\*\\*\\)" +(defvar plastic-shell-proof-completed-regexp "\\*\\*\\* QED \\*\\*\\*" "*Regular expression indicating that the proof has been completed.") (defvar plastic-save-command-regexp @@ -52,16 +52,6 @@ X (Low) e.g. probably not worth spending time on default way of setting font-lock-keywords, removing from proof-easy-config and changing each supported prover instance. -**** A Fixup silly mess introduced by Isabelle's over the top - proof-shell-proof-completed-regexp. We shouldn't match on - the whole output, that was the point of start-goals and end-goals. - Instead we should treat the proof-completed as a case within - start-goals and end-goals, as well as outside it for other - provers. Then automatically display will be in right place. - Shouldn't need proof-goals-display-qed-message any more. - This change not yet in 3.1 because it risks changing behaviour - of other provers. - **** B Modify response display routine a bit to center around recent output, or display top, for long output. Makes better sense for big screen-fulls, perhaps? Or maybe display top with an itimer to @@ -88,6 +78,20 @@ X (Low) e.g. probably not worth spending time on ** 2. Things to in the generic interface +*** X Multiple session architecture (difficult) + + With some major re-engineering, PG could be made to work with multiple + provers at once, and multiple instances of the same prover. + + Ideas: - introduce "session" notion + - have list of current sessions in progress, + values of active scripting buffer and other per-session vars + for each one + - proof shell filter and other functions must automatically + switch context to correct session + - force everybody to use proof-easy-config macro, and set + <prover>-var automatically from <proof>-var there, + to get defaults for new sessions. *** C Is there a way to make colours defined for x work in mswindows too? |