The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Examples: I have some Ltac2 files in https://github.com/JasonGross/doctoral-thesis/tree/master/performance-experiments (see files with ltac2 in the names)

There's also two implementations of reification using a slightly older version of Ltac2 at https://github.com/mit-plv/reification-by-parametricity (see files starting with Ltac2)

I believe the exception-catching mechanism is Control.case (in https://github.com/coq/coq/blob/master/user-contrib/Ltac2/Control.v).  It can catch exceptions from Control.zero, and the bit you were reading about uncatchable exceptions was probably talking about those raised by Control.throw.

On Tue, Apr 21, 2020, 23:40 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."