Stream: Coq users

Topic: Learning Ltac2


view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Aug 08 2023 at 08:03):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Aug 08 2023 at 11:58):

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

view this post on Zulip 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: Jun 23 2024 at 04:03 UTC