diff options
| -rw-r--r-- | CHANGES | 6 | ||||
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | coq/coq.el | 14 | ||||
| -rwxr-xr-x | coq/coqtags | 121 | ||||
| -rw-r--r-- | coq/ex/example-utf8.v | 9 | ||||
| -rw-r--r-- | easycrypt/easycrypt-keywords.el | 4 | ||||
| -rw-r--r-- | easycrypt/easycrypt.el | 1 | ||||
| -rw-r--r-- | generic/proof-config.el | 18 | ||||
| -rw-r--r-- | generic/proof-script.el | 7 | ||||
| -rw-r--r-- | generic/proof-shell.el | 16 |
10 files changed, 170 insertions, 28 deletions
@@ -12,6 +12,12 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac - Using query-replace (or replace-string) in the processed region doesn't wrongly jump to the first match anymore. +*** remove key-binding for proof-electric-terminator-toggle + - The default key-binding for proof-electric-terminator-toggle + (C-c .) was too easy to enter by mistake. And it was not that + useful as we can expect users to configure electric-terminator + once and for all. Hence the removal of this default key-binding. + ** Coq changes *** new menu Coq -> Auto Compilation for all background compilation options @@ -33,7 +33,7 @@ EMACS=$(shell if [ -z "`which emacs`" ]; then echo "Emacs executable not found"; PREFIX=$(DESTDIR)/usr DEST_PREFIX=$(DESTDIR)/usr -PROVERS=acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell +PROVERS=acl2 ccc coq easycrypt hol-light hol98 isar lego pghaskell pgocaml pgshell phox twelf OTHER_ELISP=generic lib contrib/mmm ELISP_DIRS=${PROVERS} ${OTHER_ELISP} ELISP_EXTRAS= @@ -1218,6 +1218,17 @@ flag Printing All set." (remove-hook 'proof-assert-command-hook 'coq-adapt-printing-width) (remove-hook 'proof-retract-command-hook 'coq-reset-printing-width))) +;; In case of nested proofs (which are announced as obsolete in future versions +;; of coq) Coq does not show the goals of enclosing proof when closing a nested +;; proof. This is coq's proof-shell-empty-action-list-command function which +;; inserts a "Show" if the last command of an action list is a save command and +;; there is more than one open proof before that save. +(defun coq-empty-action-list-command (cmd) + (when (or (and (string-match coq-save-command-regexp-strict cmd) + (> (length coq-last-but-one-proofstack) 1)) + (and (string-match "\\(S\\|Uns\\)et\\s-+Printing" cmd) + (> (length coq-last-but-one-proofstack) 0))) + (list "Show."))) (defpacustom auto-adapt-printing-width t "If non-nil, adapt automatically printing width of goals window. @@ -1541,6 +1552,9 @@ Near here means PT is either inside or just aside of a comment." proof-goal-command "Goal %s. " proof-save-command "Save %s. " proof-find-theorems-command "Search %s. ") + + (setq proof-shell-empty-action-list-command 'coq-empty-action-list-command) + ;; FIXME da: Does Coq have a help or about command? ;; proof-info-command "Help" diff --git a/coq/coqtags b/coq/coqtags index 76b5bcc9..50d4a2f5 100755 --- a/coq/coqtags +++ b/coq/coqtags @@ -2,26 +2,27 @@ # # Or perhaps: /usr/local/bin/perl # -# # $Id$ # -undef $/; +undef $/; # undef input file separator; $_ gives the whole file if($#ARGV<$[) {die "No Files\n";} -open(tagfile,">TAGS") || die "Couldn't open TAGS: $!\n"; +open($tagfile,">TAGS") || die "Couldn't open TAGS: $!\n"; while(<>) { print "Tagging $ARGV\n"; - $a=$_; - $cp=1; - $lp=1; - $tagstring=""; + $a=$_; # read the whole file into $a + $cp=1; # emacs char number of the start of + # the current line + $lp=1; # line number + $tagstring=""; # accumulate all tags of one file here while(1) { # ---- Get the next statement starting on a newline ---- + # read over balanced comments if($a=~/^[ \t\n]*\(\*/) { while($a=~/^\s*\(\*/) { $d=1; $a=$'; $cp+=length $&; $lp+=(($wombat=$&)=~tr/\n/\n/); @@ -33,14 +34,18 @@ while(<>) } } + # skip remainder of a line after a comment or a statement if($cp>1 && $a=~/.*\n/) {$a=$'; $cp+=length $&; $lp++;} - while($a=~/^\n/) {$cp++;$lp++;$a=$'} + # skip white space lines + while($a=~/^[ \t]*\n/) {$cp+=length $&;$lp++;$a=$'} + # match the next statement if($a=~/^[^\.]*\./) { $stmt=$&; $newa=$'; $newcp=$cp+length $&; - $newlp=$lp+(($wombat=$&)=~tr/\n/\n/); } + $newlp=$lp+(($wombat=$&)=~tr/\n/\n/); + } else { last;} # ---- The above embarrasses itself if there are semicolons inside comments @@ -48,20 +53,28 @@ while(<>) # print "----- (",$lp,",",$cp,")\n", $stmt, "\n"; - if($stmt=~/^([ \t]*((Fact)|(Goal)|(Lemma)|(Remark)|(Theorem))\s+([\w\']+))\s*:/) - { $tagstring.=$1."\177".$8."\001".$lp.",".$cp."\n"; } + if($stmt=~/^([ \t]*((Fact)|(Goal)|(Lemma)|(Remark)|(Theorem)|(Proposition)|(Corollary))\s+([\w\']+))\s*:/) + { $tagstring.=$1."\177".$10."\001".$lp.",".$cp."\n"; } elsif($stmt=~/^([ \t]*((Axiom)|(Hypothesis)|(Parameter)|(Variable))\s+[\w\']+)/) { adddecs($stmt,$1); } - elsif($stmt=~/^([ \t]*((Definition)|(Fixpoint)|(Inductive))\s+[\w\']+)/) - { $tagstring.=$1."\177".$6."\001".$lp.",".$cp."\n"; } + elsif($stmt=~/^([ \t]*((Definition)|(Fixpoint)|(Inductive)|(CoInductive)|(Record))\s+([\w\']+))/) + { + $tagstring.=$1."\177".$8."\001".$lp.",".$cp."\n"; + if($2 eq "Inductive" || $2 eq "CoInductive"){ + add_constructors($stmt); + } + elsif($2 eq "Record"){ + add_record_labels($stmt, $8); + } + } $cp=$newcp; $lp=$newlp; $a=$newa; } - print tagfile "\f\n".$ARGV.",".(length $tagstring)."\n".$tagstring; + print $tagfile "\f\n".$ARGV.",".(length $tagstring)."\n".$tagstring; } -close tagfile; +close $tagfile; sub adddecs { $wk=$_[0]; @@ -71,3 +84,81 @@ sub adddecs { { $sep=$2; $tagstring.=$tag."\177".$1."\001".$lp.",".$cp."\n"; $wk=$'; } 0; } + +sub add_constructors { + my ($stmt) = @_; + my ($line, $tag); + my $current=0; + + # skip to the body of the inductive definition + # and match the first constructor + if($stmt=~/:=\s*(?:\|\s*)?([\w\']+)/gc){ + do { + $tag=$1; + $line=substr($stmt, $current, pos($stmt)-$current); + + # the previous match may span several lines + # need to remove all but the last line + if($line=~/^.*\n/s){ + $current+= length($&); + $cp+= length($&); + $lp+= (($wombat=$&)=~ tr/\n/\n/); + $line=substr($stmt, $current, pos($stmt)-$current); + } + + # print "C $tag in line $lp at $cp\n\tline: $line\n"; + $tagstring.=$line."\177".$tag."\001".$lp.",".$cp."\n"; + + # match now the next constructor + } while($stmt=~/\G.*?\|\s*([\w\']+)/sgc); + } +} + +sub add_record_labels { + my ($stmt, $record_name) = @_; + my ($line, $tag); + my $current=0; + + # skip to the body of the record and match the record constructor + if($stmt=~/:=\s*([\w\']+)?/gc){ + if(defined($1)){ + $tag=$1; + } else { + $tag="Build_".$record_name; + } + + $line=substr($stmt, $current, pos($stmt)-$current); + + # the previous match may span several lines + # need to remove all but the last line + if($line=~/^.*\n/s){ + $current+= length($&); + $cp+= length($&); + $lp+= (($wombat=$&)=~ tr/\n/\n/); + $line=substr($stmt, $current, pos($stmt)-$current); + } + + $tagstring.=$line."\177".$tag."\001".$lp.",".$cp."\n"; + + # match the first record label + if($stmt=~/\G\s*{\s*([\w\']+)/gc){ + do { + $tag=$1; + $line=substr($stmt, $current, pos($stmt)-$current); + + # the previous match may span several lines + # need to remove all but the last line + if($line=~/^.*\n/s){ + $current+= length($&); + $cp+= length($&); + $lp+= (($wombat=$&)=~ tr/\n/\n/); + $line=substr($stmt, $current, pos($stmt)-$current); + } + + $tagstring.=$line."\177".$tag."\001".$lp.",".$cp."\n"; + + # match now the next record label + } while($stmt=~/\G.*?;\s*([\w\']+)/sgc); + } + } +} diff --git a/coq/ex/example-utf8.v b/coq/ex/example-utf8.v index 4cba17c8..0f528f14 100644 --- a/coq/ex/example-utf8.v +++ b/coq/ex/example-utf8.v @@ -1,11 +1,6 @@ (* -*- coding: utf-8; -*- *) -(* utf8 notations: You can (re)use the version here, - or a compiled version distributed with Coq IDE: - Add LoadPath "/usr/lib/coq/ide". - Require Import utf8. -*) -Load "utf8". +Require Import Utf8. (* Printing of unicode notation, in *goals* *) Lemma test : ∀ A:Prop, A -> A. @@ -23,4 +18,4 @@ Qed. Check (fun (X:Set)(x:X) => x). (* Parsing of unicode notation here, printing in *response* *) -Check (∀A, A→A).
\ No newline at end of file +Check (∀A, A→A). diff --git a/easycrypt/easycrypt-keywords.el b/easycrypt/easycrypt-keywords.el index 0bc10346..e0b9d369 100644 --- a/easycrypt/easycrypt-keywords.el +++ b/easycrypt/easycrypt-keywords.el @@ -5,7 +5,7 @@ ;; Distributed under the terms of the GPL-v3 license ;; -------------------------------------------------------------------- -; Generated on Thu Dec 17 16:14:05 2015 +; Generated on Tue Feb 21 23:37:34 2017 (defvar easycrypt-bytac-keywords '( "exact" @@ -43,6 +43,7 @@ "const" "op" "pred" + "inductive" "notation" "abbrev" "require" @@ -96,6 +97,7 @@ "hoare" "phoare" "islossless" + "async" )) (defvar easycrypt-tactic-keywords '( diff --git a/easycrypt/easycrypt.el b/easycrypt/easycrypt.el index ecea9744..017b2563 100644 --- a/easycrypt/easycrypt.el +++ b/easycrypt/easycrypt.el @@ -61,7 +61,6 @@ this list are strings." ;; -------------------------------------------------------------------- (defun easycrypt-prog-args () - (message "%s" easycrypt-load-path) (append easycrypt-prog-args (easycrypt-include-options))) ;; -------------------------------------------------------------------- diff --git a/generic/proof-config.el b/generic/proof-config.el index 8ce53168..8bb40634 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1187,6 +1187,24 @@ If nil, use the whole of the output from the match on :type '(choice (const nil) regexp) :group 'proof-shell) +(defcustom proof-shell-empty-action-list-command nil + "A function returning a list of commands (strings) to be sent +to the prover when the last command in the queue has been +performed. Typically to ask for some informational +display (goals, etc). + +The function takes as argument the last command in the queue. + +NOTE 1: The commands will be tagged invisible, i.e. not related +to a place in the buffer. + +NOTE 2: The commands should NOT have any effect on the state of +the prover. Otherwise running the script outside pg would be +inconsistent." + :type 'function + :group 'proof-shell) + + (defcustom proof-shell-eager-annotation-start nil "Eager annotation field start. A regular expression or nil. An \"eager annotation indicates\" to Proof General that some following output diff --git a/generic/proof-script.el b/generic/proof-script.el index e67a7774..7d9afe22 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -2565,9 +2565,10 @@ finish setup which depends on specific proof assistant configuration." ;; Additional key def for (first character of) terminal string (if proof-terminal-string (progn - (define-key proof-mode-map - (vconcat [(control c)] (vector (aref proof-terminal-string 0))) - 'proof-electric-terminator-toggle) +;; This key-binding was disabled following a request in PG issue #160. +;; (define-key proof-mode-map +;; (vconcat [(control c)] (vector (aref proof-terminal-string 0))) +;; 'proof-electric-terminator-toggle) (define-key proof-mode-map (vector (aref proof-terminal-string 0)) 'proof-electric-terminator))) diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 13da8d98..51305eef 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1110,6 +1110,22 @@ contains only invisible elements for Prooftree synchronization." (setq cbitems (cons item (proof-shell-slurp-comments))) + ;; If proof-action-list is empty after removing the already + ;; processed actions and the last action was not already + ;; added by proof-shell-empty-action-list-command (prover + ;; specific), call it. + (when (and (null proof-action-list) + (not (memq 'empty-action-list flags))) + (let* ((cmd (mapconcat 'identity (nth 1 item) " ")) + (extra-cmds (apply proof-shell-empty-action-list-command (list cmd))) + ;; tag all new items with 'empty-action-list + (extra-items (mapcar (lambda (s) (proof-shell-action-list-item + s 'proof-done-invisible + (list 'invisible 'empty-action-list))) + extra-cmds))) + ;; action-list should be empty at this point + (setq proof-action-list (append extra-items proof-action-list)))) + ;; This is the point where old items have been removed from ;; proof-action-list and where the next item has not yet been ;; sent to the proof assistant. This is therefore one of the |