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
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.
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.
That also covers why the stdlib is in Ltac1
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
an Ltac2<->Ltac1 FFI does exist, thankfully
_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 :-)
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
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?
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.
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: Sep 25 2023 at 14:01 UTC