| 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)
~~~
|
|
|
|
|
|
They were already commented out, Pierre confirms they're spurious.
|
|
|
|
|
|
|
|
in the Evd of proofs (Evd.from_env).
- Allow to set the Store.t value of new evars, e.g. to set constraint evars as
unresolvable in rewrite.ml.
- Fix a HUGE performance problem in the processing of constraints, which was remerging
all the previous constraints with the ambient global universes at each new constraint addition.
Performance is now back to (or better than) normal.
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14237 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- a ltac solve_proper which generalizes solve_predicate_wd and co
- using le_elim is nicer that (apply le_lteq; destruct ...)
- "apply ->" can now be "apply" most of the time.
Benefit: NumPrelude is now almost empty
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13762 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- For nat, we create a brand-new gcd function, structural in
the sense of Coq, even if it's Euclid algorithm. Cool...
- We re-organize the Zgcd that was in Znumtheory, create out of it
files Pgcd, Ngcd_def, Zgcd_def. Proofs of correctness are revised
in order to be much simpler (no omega, no advanced lemmas of
Znumtheory, etc).
- Abstract Properties NZGcd / ZGcd / NGcd could still be completed,
for the moment they contain up to Gauss thm. We could add stuff
about (relative) primality, relationship between gcd and div,mod,
or stuff about parity, etc etc.
- Znumtheory remains as it was, apart for Zgcd and correctness proofs
gone elsewhere. We could later take advantage of ZGcd in it.
Someday, we'll have to switch from the current Zdivide inductive,
to Zdivide' via exists. To be continued...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13623 85f007b7-540e-0410-9357-904b9bb8a0f7
|
