CRGTCoq20120920

Pierre Letouzey edited this page Oct 12, 2017 · 5 revisions

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.

Presentation by Arnaud Spiwack of his new-tacticals branch

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

About new "refine"

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!)

Multiple successes and deep backtracking

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.

About performance loss

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.

Basic components of the new monadic approach to writing tactics

  • (>>=) : '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.

Multiple goals

New prefix "all:" applies tactic to all goals.

Future

Can this model of tactics be used for redesigning Ltac?

Schedule

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)

Miscellaneous discussions

Coqdoc

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

Roadmap for 8.5 on cocorico has been validated by the present participants.

Automatic patch level releases

Pierre Boutillier will setup a system for automatic patch level releases.

Bug squash party

Pierre Boutillier will organize a bug squash party in October.

Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.