| Age | Commit message (Collapse) | Author |
|---|
|
Add headers to a few files which were missing them.
|
|
|
|
ie default goal selector !
How to do this:
- change the default value of default goal selector in goal_select.ml
- eval the emacs code in this commit message
- compile Coq and in each erroring file repeatedly run
[C-c f] (my/maybe-fix-buller-error) then [C-c C-b] (proof-process-buffer)
until there are no errors (NB the first [C-c f] has no effect).
You need to watch for 2 cases:
- overly deep proofs where the bullets need to go beyond the list in
my/bullet-stack (6 layers is enough the vast majority of the time
though). The system will give you an error and you need to finish
the lemma manually.
- weird indentation when a bullet starts in the middle of a line and
doesn't end in that line. Just reindent as you like then go to the
next error and continue.
~~~emacs-lisp
(defconst my/bullet-stack (list "-" "+" "*" "--" "++" "**")
"Which bullets should be used, in order.")
(defvar-local my/bullet-count nil
"The value in the car indicates how many goals remain in the
bullet at (length-1), and so on recursively. nil means we
haven't started bulleting the current proof.")
(defvar-local my/last-seen-qed nil)
(defun my/get-maybe-bullet-error ()
"Extract the number of focused goals from the ! selector error message."
(when-let* ((rbuf (get-buffer "*response*"))
(str (with-current-buffer "*response*" (buffer-string)))
(_ (string-match
(rx "Error: Expected a single focused goal but " (group (+ digit)))
str))
(ngoals (string-to-number (match-string 1 str))))
ngoals))
(defun my/bullet-fix-indent ()
"Auto indent until the next Qed/Defined, and update my/last-seen-qed."
;; (insert (format "(* %s -> %s *)\n" my/prev-count my/bullet-count))
(when-let ((qed (save-excursion (search-forward-regexp (rx (or "Defined." "Qed.")) nil t))))
(set-marker my/last-seen-qed qed)
(indent-region (- (point) 1) qed)))
(defun my/nth-bullet (n)
"Get nth bullet, erroring if n >= length my/bullet-stack"
(or (nth n my/bullet-stack)
(error "Too many bullets.")))
(defun my/maybe-fix-bullet-error (&optional arg)
"Main function for porting a file to strict focusing.
Repeatedly process your file in proof general until you get a
focusing error, then run this function. Once there are no more
errors you're done.
Indentation commonly looks bad in the middle of fixing a proof,
but will be fixed unless you start a bullet in the middle of a
line and don't finish it in that line. ie in 'tac1. - tac2.\n
tac3.' tac3 will get indented to align with tac2, but if tac2
finished the bullet the next action will reindent.
This is a stateful process. The state is automatically reset when
you get to the next proof, but if you get an error or take manual
action which breaks the algorithm's expectation you can call with
prefix argument to reset."
(interactive "P")
(unless my/last-seen-qed
(setq my/last-seen-qed (set-marker (make-marker) 0)))
(when (or arg (> (point) my/last-seen-qed))
(setq my/bullet-count nil)
(set-marker my/last-seen-qed 0))
(when-let ((ngoals (my/get-maybe-bullet-error)))
(setq my/prev-count (format "%s %s" ngoals my/bullet-count))
(if (= ngoals 0)
(progn
(while (and my/bullet-count (= (car my/bullet-count) 0))
(pop my/bullet-count))
(insert (concat (my/nth-bullet (- (length my/bullet-count) 1)) " "))
(setq my/bullet-count (cons (- (car my/bullet-count) 1) (cdr my/bullet-count)))
(my/bullet-fix-indent))
(setq my/bullet-count (cons (- ngoals 1) my/bullet-count))
(insert (concat (my/nth-bullet (- (length my/bullet-count) 1)) " "))
(my/bullet-fix-indent))))
(bind-key "C-c f" #'my/maybe-fix-bullet-error coq-mode-map)
~~~
|
|
|
|
|
|
|
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Most of these heavyweight annotations were introduced a long time ago
by the automatic 7.x -> 8.0 translator
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Many of them were broken, some of them after Pierre B's rework
of mli for ocamldoc, but not only (many bad annotation, many files
with no svn property about Id, etc)
- Useless for those of us that work with git-svn (and a fortiori
in a forthcoming git-only setting)
- Even in svn, they seem to be of little interest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
implicits for left, inl or eq, hence some theories had to be changed
again. It should make some user contribs compile again too. Also
do not import functional extensionality when importing Program.Basics,
add a Combinators file for proofs requiring it and a Syntax file for the
implicit settings. Move Classes.Relations to Classes.RelationClasses to
avoid name clash warnings as advised by Hugo and Pierre.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10681 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
out. The semantics of the old setoid are faithfully simulated by the new
tactic, hence no scripts involving rewrite are modified. However,
parametric morphism declarations need to be changed, but there are only a
few in the standard library, notably in FSets. The declaration and the
introduction of variables in the script need to be tweaked a bit,
otherwise the proofs remain unchanged.
Some fragile scripts not introducting their variable names explicitely
were broken. Requiring Setoid requires Program.Basics which sets stronger
implicit arguments on some constants, a few scripts benefit from that.
Ring/field have been ported but do not really use the new typeclass
architecture as well as they could. Performance should be mostly
unchanged, but will certainly improve in the near future. Size of the
vo's seems not to have changed at all.
It will certainly break some contribs using Setoid.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10631 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9642 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
par les fichiers nouvelle syntaxe
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4463 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3267 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2650 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1623 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1387 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@900 85f007b7-540e-0410-9357-904b9bb8a0f7
|
