Stream: Ltac2

Topic: Why Ltac2 cannot obsolete Ltac1 yet

Paolo Giarrusso (Oct 02 2021 at 12:27):

The title is maybe a bit provocative, so let me clarify this is not about _technical_ criticism.

But a thread seemed appropriate, since @Karl Palmskog was suggesting a migration away from ltac1, and we were having multiple discussions on the migration, and on the documentation, etc.

Paolo Giarrusso (Oct 02 2021 at 12:34):

And to be sure, this is an outside POV — I have not yet learned how to migrate from Ltac1 to Ltac2. For starters:

1. Ltac2 lacks a tutorial — one can still learn it, but at some cost.
2. Ltac2 has not been adopted that much, outside of (quite a few) experts — most Coq users still learn Ltac1. And the stdlib still uses ltac1 (almost exclusively?)
3. AFAICT from my last look, Ltac2 lacks convenience bindings which you'd want to have to port existing code — we can write ltac1:() everywhere, but you'll probably want to write wrappers for that.

Paolo Giarrusso (Oct 02 2021 at 12:35):

AFAICT, this is likely circular — nobody writes those conveniences, so nobody uses Ltac2 as an Ltac1 replacement, so nobody writes those conveniences... Basically, it's a standard adoption problem

Karl Palmskog (Oct 02 2021 at 12:41):

in other words (from game theory), it's a coordination problem, and I was suggesting future sunsetting of Ltac1 as a coordination signal

Paolo Giarrusso (Oct 02 2021 at 12:48):

That makes sense, but I don’t think it’s _only_ a coordination problem. Are there resources to devote to kickstarting this migration, and is this actually a priority?

Karl Palmskog (Oct 02 2021 at 12:50):

if there is to be a migration plan (or at least a plan of getting people to use Ltac2), then that plan obviously has to consider the availability and procurement of resources. But this should also be compared against what maintaining and developing and bugfixing Ltac1 is costing now, and the costs of using Ltac1 by Coq project maintainers.

Paolo Giarrusso (Oct 02 2021 at 12:53):

Good. I thought all Ltac1 bugs were now WONTFIX, but I’m sure regressions count.

Karl Palmskog (Oct 02 2021 at 12:54):

if Ltac1 bugs are now WONTFIX, that's news to be, and is at least an initial signal that should perhaps be broadcasted more loudly and frequently.

Paolo Giarrusso (Oct 02 2021 at 12:58):

hmm, I vaguely remember @Pierre-Marie Pédrot making some such off-hand comment, but “don’t quote me on that”, as they say.

Paolo Giarrusso (Oct 02 2021 at 13:02):

Meanwhile coq@master$ ack --coq --ignore-dir test-suite --ignore-dir user-contrib/Ltac2 Ltac2 finds no Coq occurrences of Ltac2 outside the testsuite and its library… am I doing something wrong? I remember Odersky saying that the Scala3 compiler had to bootstrap before it could be a credible alternative (and bootstrap it did).

Pierre-Marie Pédrot (Oct 02 2021 at 13:22):

The problem is that the stdlib is supposed to also be replaced by the stdlib2 at some point. Porting code that should disappear soon looks like a bad use of dev time...

Paolo Giarrusso (Oct 02 2021 at 13:24):

"stdlib2 will happen" is not in the same galaxy as "ltac2 will happen"

Pierre-Marie Pédrot (Oct 02 2021 at 13:28):

(There were also build system issues, since Ltac2 lives in user-contrib for some sordid reason related to -R stdlib namespacing, precluding its use in the stdlib)

Pierre-Marie Pédrot (Oct 02 2021 at 13:28):

maybe with the switch to dune we're on the good way though

Théo Zimmermann (Oct 02 2021 at 13:30):

Pierre-Marie Pédrot said:

The problem is that the stdlib is supposed to also be replaced by the stdlib2 at some point. Porting code that should disappear soon looks like a bad use of dev time...

You should consider stdlib2 dead. If it happens fine. But let's not that be an excuse for not porting the current stdlib.

Théo Zimmermann (Oct 02 2021 at 13:31):

And that Ltac1 bugs are WONTFIX isn't even true in practice.

Paolo Giarrusso (Oct 02 2021 at 13:31):

Thanks for the correction!

Paolo Giarrusso (Oct 02 2021 at 13:31):

@Pierre-Marie Pédrot to be clear, this wasn't in any way a criticism of your work, so no need to defend it. But yes, some dogfooding would be necessary.

Paolo Giarrusso (Oct 02 2021 at 13:34):

Also, I doubt somebody (or even the community) will rewrite 3 MLoC of Coq code, so a migration strategy might need some way to minimize the migration cost...

Paolo Giarrusso (Oct 02 2021 at 13:35):

@Karl Palmskog did you (or somebody) say that lots of project did not migrate beyond Coq 8.10? Does that match the breaking changes in require/import semantics?

Paolo Giarrusso (Oct 02 2021 at 13:37):

oh, it was @Michael Soegtrop observing that here https://coq.zulipchat.com/#narrow/stream/250632-Coq-Platform.20devs.20.26.20users/topic/LOC.20size.20of.202021.2E09.20and.20later/near/255589209 — and yes it matches that breakage https://coq.inria.fr/refman/changes.html#version-8-11.

Karl Palmskog (Oct 02 2021 at 13:37):

well, I noted that according to Gauillaume Claret's coq-bench, 8.8 and 8.9 currently have the highest number of compatible projects in the released opam repository. From 8.10 on, fewer and fewer projects are compatible. But there could be several reasons, including that most contribs have not been updated for 8.10.

Karl Palmskog (Oct 02 2021 at 13:38):

at least an MLOC of Coq code uses SSReflect, which I believe would be mostly unaffected by a switch from Ltac1 to Ltac2. In fact, one of the original motivations of developing SSR (IIUC) was to obtain independence from Ltac1.

Paolo Giarrusso (Oct 02 2021 at 13:45):

ssreflect seems a set of ltac1 tactics, and not yet compatible with ltac2; https://github.com/coq/coq/issues/12843. I'm looking forward to the diff size for the ltac2 migration.

Paolo Giarrusso (Oct 02 2021 at 13:47):

I haven't tried Ltac2 enough yet to know, but it seems there are enough changes that an impact of <1% would be amazing... but pretty clearly, this is a number pulled out of thin air :sweat_smile:

Enrico Tassi (Oct 02 2021 at 13:56):

Karl Palmskog said:

at least an MLOC of Coq code uses SSReflect, which I believe would be mostly unaffected by a switch from Ltac1 to Ltac2. In fact, one of the original motivations of developing SSR (IIUC) was to obtain independence from Ltac1.

IMO we should distinguish "tactic language" and "proof language".

SSR is a language to write proofs, it uses ltac1 in a very basic way (mostly ;). It is implemented in OCaml directly, that is its tactics don't need to be ported to Ltac2. Internally it uses, still, both the legacy APIs and new ones (around which Ltac2 is also geared, the monad stuff). Porting is slow, since it amounts at rewriting things almost completely. And I don't love the new API, which also does not give much in return, so motivation is little.

From time to time SSR folks write domain specific automation, a field where ltac1 + reflection is a well established solution. I guess also for proximity reasons, the new code is using Elpi rather than ltac1/ltac2. Eg https://github.com/math-comp/algebra-tactics

Karl Palmskog (Oct 02 2021 at 14:06):

so in principle, SSR/MathComp projects are probably good first targets to investigate for feasibility of being Ltac1-free - either port existing higher-level proof automation to Ltac2 or to Elpi

Enrico Tassi (Oct 02 2021 at 14:09):

Another way to clarify: Ltac1 means 2 things which are different. A basic set of tactics (eg intros, induction, trivial...) and a glue language to combine them (eg ;, match goal with...). The SSR set of basic tactics is not available to Ltac2 scripts (nor Elpi) at the time of writing. :-/ (IIRC you have to go via ltac1 to call them)

Karl Palmskog (Oct 02 2021 at 14:12):

OK, good to know, my argument was basically that any reasonable Ltac2 migration would put calling-SSR-from-Ltac2 as a high priority milestone, since then you would suddenly have several hundred KLOC of Ltac2-only (Ltac1-free) projects, and you could get more by porting the occasional Ltac1 high level automation script

Michael Soegtrop (Oct 02 2021 at 15:32):

Karl Palmskog said:

well, I noted that according to Gauillaume Claret's coq-bench, 8.8 and 8.9 currently have the highest number of compatible projects in the released opam repository. From 8.10 on, fewer and fewer projects are compatible. But there could be several reasons, including that most contribs have not been updated for 8.10.

I guess this means I should provide Coq 8.9 upwards in Coq Platform - I think it helps to port code if one can easily install the old and new Coq version in parallel, which is well supported by Coq Platform (it also gives instructions on how to configure different opam switches in different shells, so that one can have e.g. a 8.9 and 8.13 CoqIDE running at the same time).

Last updated: Apr 19 2024 at 15:02 UTC