Stream: Coq users

Topic: LTAC vs LTAC2


view this post on Zulip walker (Oct 02 2022 at 18:52):

As per https://coq.inria.fr/refman/proof-engine/ltac2.html

LTAC2 is better than LTAC because it is typed tactics language, but the reality is most tactics I have ever see are LTAC tactics,

Is there a reason for that? is there some limitations for ltac2 that makes people move away from? Also why is standard library tactics not ltac2 based

The reason I am asking is me trying to figure out if it is worth it trying to learn ltac2 or should I spend my time on something more valuable

view this post on Zulip walker (Oct 02 2022 at 18:56):

any incompatiabiliy issues that I should know ahead of time (maybe ltac and ltac2 cannot be mixed for instance..) would be very useful to know about ahead of time.

view this post on Zulip Paolo Giarrusso (Oct 02 2022 at 23:44):

Most of what you see is that for a long time only Ltac1 existed, so most code and learning material uses Ltac1 instead of Ltac2.

view this post on Zulip Paolo Giarrusso (Oct 02 2022 at 23:48):

That also covers why the stdlib is in Ltac1

view this post on Zulip Paolo Giarrusso (Oct 02 2022 at 23:49):

Ltac2 improves on Ltac1 beyond having a type system — it lets you define datatypes instead of Ltac1's hacks, it has a more predictable semantics, better support for notations including _variadic_ notations, etc

view this post on Zulip Paolo Giarrusso (Oct 02 2022 at 23:50):

an Ltac2<->Ltac1 FFI does exist, thankfully

view this post on Zulip Paolo Giarrusso (Oct 02 2022 at 23:52):

_personally_, I usually stick to Ltac1, but the one time I was motivated dealing with an Ltac1 serious limitation (variadic tactics — that is, taking a variable number of arguments), I came up with an Ltac2 solution in a few hours, so it's not impossible :-)

view this post on Zulip walker (Oct 03 2022 at 06:08):

noted, I will try all my tactics in ltac2 and hope it pays off in the long run at least in understnding other parts of coq

view this post on Zulip James Wood (Oct 03 2022 at 08:23):

Is it feasible/advisable to start new projects off with something like From Ltac2 Require Export Ltac2.? What differences would I or users of such a library notice?

view this post on Zulip Théo Zimmermann (Oct 03 2022 at 08:49):

I think that at this point, it is probably not reasonable to expect that every dependency will be fine with using only the Ltac2 proof mode. Ltac2 is mostly useful to write advanced tactic automation. It does not bring that many benefits as a proof mode, and you may encounter the issue that not all tactics are yet available in the Ltac2 proof mode.

view this post on Zulip Théo Zimmermann (Oct 03 2022 at 08:52):

People have been asking for a feature to be able to extend the Ltac1 proof mode with tactics defined entirely in Ltac2 (including the parsing rules), cf. https://github.com/coq/coq/pull/16394, precisely because of this limitation of current Ltac2 proof mode and not wanting to impose it upon their users.


Last updated: Mar 29 2024 at 07:01 UTC