CRGTCoq20120920
Participants: Pierre Boutillier, Thomas Braibant, Guillaume Claret, Pierre Courtieu, Lourdes del Carmen González Huesca, Hugo Herbelin, Pierre Letouzey, Pierre-Marie Pédrot, Yann Régis-Gianas, François Ripault, Arnaud Spiwack.
Note: a talk was planned on extraction of programs from inductive specifications, but it had be cancelled.
New step in plugging existing tactics on top of the 8.4 new proof engine, using the new "Proofview.tactic" type.
New features:
- "refine" is now a true refine: it uses the given partial proof term as proof for the current goal
- tactics have several succeesses and can do deep backtracking
- tactics can return values in addition to making the goal evolve
- separation interp/run
- tactics applying to multiple goals
Adaptations to do on the ML code:
- all tactics having tactic as arguments have to be rebuilt to use the new "tactic" type
- all TACTIC EXTEND have to be adapted
- "intro" modified, so all tactics using "intro" needs to be adapted
Caveats:
- performance loss of 15% on the compilation of the standard library
Incompatibilities to resolve:
- "refine" currently uses names provided by the "match" compiler which are different from the ones used in the previous version of "refine"
Questions about "refine": how to manage names clash?
- What shall we do for "refine (fun x => _)" on goal "x:nat |- nat -> nat"?
- fail, as if doing "intros x"?
- leading to "x:nat, x0:nat |- nat", as the 8.4 "refine"
- leading to "x0:nat, x:nat |- nat", so as to implement "name shadowing" the same way it is implemented in "Definition f x x := x".
- one of the two previous cases with a warning
- Similarly, what shall we do for "refine (fun x x => _)" on goal "|- nat -> nat -> nat"?
- fail, as if doing "intros x x"?
- leading to "x:nat, x0:nat |- nat", as the 8.4 "refine"
- leading to "x0:nat, x:nat |- nat", so as to implemented "name shadowing"
- one of the two previous cases with a warning
No consensus found
The discussion moved to the question of giving a different status to Coq-generated names and to user-generated names: consensus to eventually go into this direction (but this needs work!)
The new proof engine implements the law "(a+b);c = (a;c)+(b;c)", meaning that if c fails after a succeeded, than backtract to b is applied
Tactics have multiple successes, for instance, tactic a+b concatenates the successes of a and the successes of b (this is what allows the above backtracking).
The new engine also allows to define new tacticals such as Shan and Kiselyov's "split", or a primitive "once t" which returns a single success of t.
Loss seems related to an extra pervasive creation of ML closures, due to the use of a monadic style (tactics now work by side-effects on a state).
Hugo and Thomas remind that many users are very dependent of (and limited by) the performance issues of Coq. Extra losses of performance would be painful for many heavy users such as Chlipala, Leroy, Gonthier.
- (>>=) : 'a tactic -> ('a -> 'b tactic) -> b tactic
- tclUNIT : 'a -> 'a tactic
In particular, tclUNIT is what allows to have tactics returning values.
Internally, the monad includes several levels, two of them being accessible from the user: "Logical" for successes and failures and "NonLogical" for side-effects such as printing on the console.
For instance, "tclIDTAC" uses printing facilities from the NonLogical level.
At the Logical level, there are for instance:
- tclZERO : exn -> 'a tactic
- tclPLUS : 'a tactic -> (exn -> 'a tactic) -> 'a tactic
The functions
- Proofview.Goal.hyps : named_context_val glist tactic
- Proofview.Goal.concl : constr glist tactic
return the hypotheses and conclusion of the goal (by side-effect on the goal state).
Coq developers and plugins developers would have to learn the new model.
Thomas asks about the existence of a documentation to ease the transition for plugin developers.
New prefix "all:" applies tactic to all goals.
Can this model of tactics be used for redesigning Ltac?
Considering the amount of new and potential features introduced by the use of the new proof engine, a majority of participants supports the switch to the new tactical branch without much delay, betting that the resulting slow down can be resolved by the next official release (which is not planned before 1 year from now).
However, it is first expected
- that the bench over contribs successfully compiles with trunk (so that there is no interferences with other ongoing changes)
- that the compilation of contribs is tested with the new-tacticals branch with a global evaluation of time loss and of the conviction that the amount of time needed to repair the contribs is reasonably tractable (not more than a few days)
Yann presents the project of new coqdoc on which François Ripault is working. It would support literate programming: coqdoc would drive coqc, possibly reordering parts of the original file to be sent to coqtop which would be a compiler of requests more than a compiler of linear .v file as it is now.
Roadmap for 8.5 on cocorico has been validated by the present participants.
Pierre Boutillier will setup a system for automatic patch level releases.
Pierre Boutillier will organize a bug squash party in October.
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.