The Coq mailing list

[Tej Chajed <tchajed AT mit.edu>]

I've written an Ltac2 tutorial with a handful of examples and detailed explanations. I also have a repo for Ltac2 experiments with slightly bigger examples but less documentation.

I haven't really used the backtracking support, although it looks cool; I'd recommend reading user-contrib/Ltac2/Pattern.v in the Coq sources to see how `match! goal with` and `match! constr:(...) with` are implemented, which is based on the Control.plus, Control.case, and Control.zero primitives.

On Tue, Apr 21, 2020 at 10:40 PM jonikelee AT gmail.com <jonikelee AT gmail.com> wrote:

I've read through the Ltac2 section of the 8.11 refman, and still have
many qeustions.  Perhaps seeing some examples would help.  Is there
somewhere I can find some links to Ltac2 examples?

The Ltac2 section appears to have been targeted in spots to Coq devs
with Ocaml knowledge.  At one point it says: "We recall that the
Proofview.tactic monad is essentially a IO monad together with
backtracking state representing the proof state."  There are
several other cases of this - so without the Coq Ocaml internals
background info, I'm left with many holes in my understanding.

There are also apparent inconsistencies, or at least omissions, in the
refman.  At the end, it says: "Ltac2 features a proper
exception-catching mechanism. For this reason, the Ltac1 mechanism
relying on fail taking integers, and tacticals decreasing it, has been
removed. Now exceptions are preserved by all tacticals, and it is your
duty to catch them and re-raise them as needed."  But I don't see any
catch mechanism described.  Indeed, at an earlier point, it says:
"There is currently no way to catch such an exception, which is a
deliberate design choice. Eventually there might be a way to catch it
and destroy all backtrack and return values."