I entered Require Import Ltac2.Ltac2 and it broke a bunch of stuff in my Coq script, for example easy and intuition invocations. I’m aware that I can use ltac1:(...) to make it work, but I’m guessing that this is not the “blessed” way to do things in Ltac2? If so I would love to learn more about Ltac2. Where should I start?
Thank you in advance.
Hi,
The only documentation of Ltac2 so far is the one in the reference manual: Ltac2 — Coq 8.18.0 documentation
One important point that I want to attract your attention to is the following one: Ltac2 — Coq 8.18.0 documentation
We recommend using the
Default Proof Modeoption to switch between tactic languages with a proof-based granularity. This allows to incrementally port the proof scripts.
In particular, calling Set Default Proof Mode "Classic". will allow you to write some Ltac1 scripts including all the tactics you are used to and Set Default Proof Mode "Ltac2". will allow you to switch to a fully Ltac2 mode. Even in “Classic” (Ltac1) mode, you can rely on the tactics you have defined using Ltac2 constructs. You can bind them in Tactic Notations.
A number of tactics are not exported as syntax in the Ltac2 plugin yet: you are encouraged to open issues every time you encounter an example of this. As a workaround, you can use Ltac2 Notation to redefine the syntax for these existing but unexported tactics.
Thank you for testing Ltac2!
I’ve also been learning Ltac2 and documenting a number of experiments here: https://github.com/tchajed/coq-ltac2-experiments.
I haven’t yet written up a guide to Ltac2, but you’ll at least find more code examples.
BTW, feel free to contribute to improving the reference manual, for instance by adding more examples!
I actually did write an Ltac2 tutorial, if you’re interested in a guided tour through a few features: https://github.com/tchajed/ltac2-tutorial.