Stream: Coq users

Topic: Learning Ltac2

Pierre Rousselin (Aug 08 2023 at 07:34):

In my never-ending quest of learning Coq, I would like now to learn to write tactics.
If I'm not mistaken, Ltac2 is now the preferred tactic language. However, when reading the reference manual, or even tchajed's tutorial, I feel completely lost.

• Is it better to learn Ltac1 before trying to learn Ltac2? If so, what are good references for this?
• Do you know of other references to learn Ltac2?
• Does Ltac2 only change the way to write new tactics or does it change also the way we write proof scripts?

Paolo Giarrusso (Aug 08 2023 at 08:03):

https://coq.zulipchat.com/#narrow/stream/278935-Ltac2/topic/Resources.20to.20learn.20Ltac.2FLtac2/near/284413928

Paolo Giarrusso (Aug 08 2023 at 08:11):

AFAIU from colleagues who use it, you're correct that (a) most people still only use Ltac1 (b) Ltac2 documentation is much scarcer (c) Ltac2 itself has a much better core language, but some actual library conveniences are missing (d) most code around is in Ltac1.

At least because of (d), I'd personally recommend learning Ltac1 first.

Enrico Tassi (Aug 08 2023 at 11:09):

You could also ignore both and learn coq-elpi (semi serious). After all, you did not say what you want to do with it.

Pierre Rousselin (Aug 08 2023 at 11:24):

To be honest, my primary goal is actually to learn more and more Coq.
As for writing tactics, I'm thinking about a few things like:

• classical tactics : by_contradiction, push_neg, etc Maybe these exist already, but being able to write them myself would be nice.
• maybe pedagogical tactics, like weakened versions of existing tactics
  And if I feel I understand well Ltac[12], I could maybe write a tutorial with exercises as a contribution (if it's relevant)?
  Thanks for pointing out Coq-ELPI, I will look at it?

Pierre Rousselin (Aug 08 2023 at 11:27):

Paolo Giarrusso said:

https://coq.zulipchat.com/#narrow/stream/278935-Ltac2/topic/Resources.20to.20learn.20Ltac.2FLtac2/near/284413928

Thank you for the reference, looking at Chlipala's tutorial right now.

Karl Palmskog (Aug 08 2023 at 11:28):

there is this project that attempts to collect examples for different tactic languages (including Ltac2 and Elpi): https://github.com/coq-community/metaprogramming-rosetta-stone

Enrico Tassi (Aug 08 2023 at 11:55):

Given your use case both ltac2 and elpi seem OK.
I would not use ltac1 just because it won't be a good learning investment being already deprecated.
Ltac2 should look familiar, maybe a bit low level. Elpi is a bit more odd, if you have not used Prolog before, but is a bit more high level.

Paolo Giarrusso (Aug 08 2023 at 11:58):

We _should_ deprecate Ltac1, but Ltac2 isn't mature — we've discussed this.

Théo Zimmermann (Aug 11 2023 at 16:24):

People in the core dev team tend to abuse the word deprecated. Ltac1 is not deprecated yet, because Ltac2 is not ready to replace it fully yet. But programming new code in Ltac1, beyond very basic stuff, is certainly already discouraged: https://coq.github.io/doc/master/refman/proof-engine/ltac.html

Last updated: Oct 13 2024 at 01:02 UTC