Ignat Insarov (Oct 01 2021 at 13:43): Ignat Insarov (Oct 01 2021 at 13:43):What is Ltac2 and should I care?
I want to write fancy tactics, following Certified Programming with Dependent Types by Adam Chlipala. I am often annoyed how tedious and repetitive «elementary» proofs are. Can Ltac2 help me? What learning resources are available, other than the section in the reference manual? Especially examples.
Pierre-Marie Pédrot (Oct 01 2021 at 14:01):Can Ltac2 help me?
Probably not, or at least not much more than Ltac1 in that respect.
Pierre-Marie Pédrot (Oct 01 2021 at 14:01):Ltac2 is about writing robust automation that scales. It does not free you from writing your business logic code in the first place.
Ignat Insarov (Oct 01 2021 at 14:09):If Ltac2 is all the same as Ltac1 but more robust and scalable, then clearly I should wield Ltac2 rather than Ltac1. Are there any drawbacks?
Pierre-Marie Pédrot (Oct 01 2021 at 14:27):Lack of documentation, and some missing bindings.
Ignat Insarov (Oct 01 2021 at 14:30):Are there plans to eventually replace the one with the other?
Pierre-Marie Pédrot (Oct 01 2021 at 14:32):I'd say yes but I am obviously biased.
Pierre-Marie Pédrot (Oct 01 2021 at 14:32):(Disclaimer: I designed and implemented Ltac2)
Pierre-Marie Pédrot (Oct 01 2021 at 14:33):But the inclusion was decided collegially and other core devs also push for a replacement
Ignat Insarov (Oct 01 2021 at 14:37):So are there some examples, like maybe on GitHub?
Ignat Insarov (Oct 01 2021 at 14:37):Examples of developments that wield Ltac2. Not isolated snippets, like in the reference.
Ignat Insarov (Oct 01 2021 at 14:38):Something I could clone and poke at would be ideal.
Ignat Insarov (Oct 01 2021 at 14:39):I am anxious to rewrite my tactics into the language of the future!
Ignat Insarov (Oct 01 2021 at 14:55):And a question if I may. How to fix this?
Ltac simplify_everything := simpl; simpl in *.
Fail Ltac2 simplify_everything := simpl; simpl in *.
Tactic definition must be a syntactical value
Semicolon composition is the most basic way to wield Ltac, and now it is forbidden?
Alexander Gryzlov (Oct 01 2021 at 16:05):Note that there's a separate #Ltac2 stream on this server.
Ignat Insarov (Oct 01 2021 at 16:07):Thanks, I did not know.
Karl Palmskog (Oct 01 2021 at 16:08):I would argue the core Coq team should set a planned end-date (year?) soon for Ltac1-maintained-as-part-of-Coq,and then throw it out to the community to maintain and go all in on Ltac2. It isn't unknown that some proof language gets thrown out in favor of another. Clearly, migrating to Ltac2 would be a benefit to many projects in the longer term (not least due to weird/unspecified Ltac1 behavior and bugs)
Michael Soegtrop (Oct 01 2021 at 18:06):@Karl Palmskog : I am not su sure this is a good idea. Some projects have vast amounts of complex Ltac1 code, e.g. VST. I would almost say I am sure it is not a good idea. Porting VST to Ltac2 would take years.
@Ignat Insarov : I (mostly) switched to Ltac2 (and Mtac2) a while back and didn't regret this. Complicated stuff is definitely easier to write and Maintain in Ltac2 than in Ltac1. Interfacing between Ltac1 and Ltac2 tactics works reasonably well.
One consideration: @Jim Fehrle is working on an interactive debugger for Ltac1 in CoqIDE - there will be a preview in Coq Platform 2021.09 (coming in a few days). Eventually this might also work for Ltac2, but currently it doesn't (afaik). On the other hand printf style debugging works well in Ltac2, especially since the printing functions have been substantially improved. I have a verbosity definition in each of my larger Ltac2 files, with which I can control debug printing. I find Printf (idtac) debugging in Ltac1 is much harder.
And yes, there is also an Mtac2 is: it is a dependently typed tactic language (essentially an extension of Gallina), so in case you change some lemma you apply in a tactic, your tactic won't type check any more rather than fail later. I think you should enjoy stuff like chess riddles in case you want to use Mtac2. But it has its strong points and I try to find some time to improve my skills with it.
Hope this helps a bit to find your path.
Karl Palmskog (Oct 01 2021 at 18:08):@Michael Soegtrop so if they flagged up that Ltac will be community-maintained from (say) 2024, there would be plenty of time. Otherwise we will be stuck with Ltac1-in-Coq practically forever.
Karl Palmskog (Oct 01 2021 at 18:13):I would be more interested in the situation of SSReflect and Ltac2, i.e., can we get SSR primitives on top of Ltac2 and never have to touch Ltac1.
Paolo Giarrusso (Oct 01 2021 at 21:51):Compared to Ltac1, Ltac2 seems the language of the future, but it does not seem the language of the present yet (for the reasons given by Pierre-Marie).
Paolo Giarrusso (Oct 01 2021 at 22:09):More precisely, everybody who’s writing complex proof automation and tried ltac2 prefers it over ltac1; but I haven’t seen write concrete proofs in ltac2. Could one port, say, Software Foundations?
Jim Fehrle (Oct 02 2021 at 03:46):@Karl Palmskog What is the big benefit of making Ltac community maintained? Why are you so eager? As Michael noted, VST and other projects depend on it and it would require a huge effort by them to migrate. Indeed, several of the professors in DeepSpec pay the Consortium for support services. They might not appreciate a change in Ltac's status. There's no well defined migration strategy to go from Ltac1 to Ltac2; the Ltac2 doc currently says "we do not guarantee [migrating] will be a blissful walk in the park".
I don't think we're anywhere close to being ready to retire Ltac1.
It isn't unknown that some proof language gets thrown out in favor of another.
A great way to alienate a large swathe of the community.
Jim Fehrle (Oct 02 2021 at 03:50):@Ignat Insarov The debugger preview will come out a few days after the initial 8.14 release, which it will be based on.
I'm unlikely to look at Ltac2 support until the debugger work done thus far has been reviewed and merged. I would like to see it included in 8.15.
Ignat Insarov (Oct 02 2021 at 09:42):So, it turns out that I have to make all my Ltac2 definitions accept at least one argument even if they do not need any. This adds syntactic noise. I am going to look at alternatives.
Notification Bot (Oct 02 2021 at 09:42):Ignat Insarov has marked this topic as resolved.
Théo Zimmermann (Oct 02 2021 at 11:21):Yeah, that's because Ltac2 is an ML language. So it behaves like an ML language.
Théo Zimmermann (Oct 02 2021 at 11:22):But I'm pretty sure you can add tactic notations on top to avoid having to explicitly provide the argument when using the tactics in a proof script.
Ignat Insarov (Oct 02 2021 at 11:41):Yes, I can. So, I have 2 options:
… ( ) everywhere I want to call an Ltac2 effect.Ltac2 Notation … everywhere I want to define an Ltac2 effect.Yeah, that's because Ltac2 is an ML language. So it behaves like an ML language.
I do not think this explains much. Compare:
Yeah, that's because Ltac2 is designed mostly by French researchers. So it behaves like a language designed mostly by French researchers.
Yeah, that's because Ltac2 is a voodoo language. So it behaves like a voodoo language.
In any case the answer to the question «why design a new language in such a way that it is obviously less comfortable than the previous» is not given. See also this cute little essay.
That is not to argue «for» or «against» something. I merely want to make clear from what environment my previous messages arise.
Gaëtan Gilbert (Oct 02 2021 at 11:42):it's because the implicit thunking in ltac1 was a major pain point when trying to understand ltac1 semantics, so it was forced to be explicit in ltac2
Ignat Insarov (Oct 02 2021 at 11:43):It is often on this forum that I see people explaining my messages as «this person clearly is not aware of an obvious argument» when the real explanation is that the obvious argument does not explain the issue.
Michael Soegtrop (Oct 02 2021 at 11:44):I agree with @Gaëtan Gilbert. The implicit thunking saves you a few () here and there, but the cost is very substantial complication when things get complicated. I prefer a language which works well for complicated stuff. I don't care much how well it works for trivial stuff. And for the really common stuff you have notations.
Ignat Insarov (Oct 02 2021 at 11:44):In this case:
it's because the implicit thunking in ltac1 was a major pain point when trying to understand ltac1 semantics, so it was forced to be explicit in ltac2
I am already aware of these premises, but I do not think the conclusion «we must make another ML language» is as inevitable as you imply.
Gaëtan Gilbert (Oct 02 2021 at 11:45):I don't imply, I'm not the one who brought up ML
Ignat Insarov (Oct 02 2021 at 11:45):… I don't care much how well it works for trivial stuff. …
Is this arrogance? «Pf, those undergraduate students that want to formalize the fundamental theorem of Arithmetics.»
Paolo Giarrusso (Oct 02 2021 at 11:48):@Ignat Insarov I am convinced it’s not arrogance, and either way you’ve been warned _today_ against ascribing motives.
Michael Soegtrop (Oct 02 2021 at 11:48):I think one need not debate that there a different languages optimized for different levels of complexity. I use mostly shell, python and OCaml (besides Coq). There is an area of overlap between these languages on the complexity scale, but it is rather small compared to the full scale of complexity I encounter.
IMHO Ltac1 is optimized for situations like shell, Ltac2 is optimized for situations for which I would use OCaml. These targets naturally lead to some inconvenience at the other end of complexity.
Paolo Giarrusso (Oct 02 2021 at 11:49):Thanks for expanding, Michael :-)
Ignat Insarov (Oct 02 2021 at 11:50):@Paolo Giarrusso I was?
Paolo Giarrusso (Oct 02 2021 at 11:50):going to find the link in a minute
Paolo Giarrusso (Oct 02 2021 at 11:51):And FYI: You have valid questions, but whether the way you ask them _comes off_ as unnecessarily confrontational — I don’t know whether that’s intended, but that’s not the most effective way to understand the design and propose changes.
Ignat Insarov (Oct 02 2021 at 11:52):@Michael Soegtrop This is another overly general explanation. It does not tell us precisely that there is no other way to make a better language than add some syntactic noise. I can easily give an example of the opposite: Haskell has far less noise than shell.
Michael Soegtrop (Oct 02 2021 at 11:52):@Karl Palmskog : I think it is worthwhile to replace Ltac1 with Ltac2 in the long run, but I would upfront ask people for a time scale. For VST I don't see how it could be done in say 2 years.
Paolo Giarrusso (Oct 02 2021 at 11:54):@Ignat Insarov I'll retract the warning part — I was thinking about https://coq.zulipchat.com/#narrow/stream/278935-Ltac2/topic/.E2.9C.94.20What.20to.20do.20instead.20of.20semicolons.3F/near/255864515, but I'm not going to argue it's exactly the same thing. Still.
Michael Soegtrop (Oct 02 2021 at 11:55):@Ignat Insarov : well you are free to design such a language - I haven't seen one as yet. All I can say is that I use shell for certain tasks, python for other tasks and OCaml for still other tasks. Maybe one can make a language which is equally well at all of this, but languages which try to be powerful and super concise at the same time are IMHO a night mare (think of perl).
Paolo Giarrusso (Oct 02 2021 at 11:55):@Michael Soegtrop on the merits, the comparison with Perl is not the right one.
Gaëtan Gilbert (Oct 02 2021 at 11:56):ltac1 is more a javascript
Paolo Giarrusso (Oct 02 2021 at 11:57):the question seems similar to the one in https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Proof.20monad.3F: hiding side effects is error-prone, and ML and Haskell both tackle the problem differently and more robustly from Ltac1
Michael Soegtrop (Oct 02 2021 at 11:57):@Gaëtan Gilbert : I wouldn't say so. I would compare Ltac1 more with shell - it is optimize for giving single line commands in a concise way.
Gaëtan Gilbert (Oct 02 2021 at 11:59):fair enough
Karl Palmskog (Oct 02 2021 at 12:01):@Michael Soegtrop Python 2 and 3 are obvious examples, they even have an end-of-life specified for each minor release: https://endoflife.date/python
If "big" projects like VST are currently what is preventing an end-of-life plan for Ltac1, then I think we should be explicit about this in the community, e.g., we say that we maintain it [Ltac1] indefinitely because projects X, Y, Z will take years upon years to migrate, so people know this is the reason.
Théo Zimmermann (Oct 02 2021 at 12:11):I don't think this is the only thing. Ltac2 is just too complicated for simple things where Ltac1 is suitable.
Karl Palmskog (Oct 02 2021 at 12:13):@Jim Fehrle I'm a bit surprised about your strong wording about alienating users by moving to Ltac2. Python 2 is clearly a language of its own, yet the Python authors and maintainers sunset Python 2 last year, in spite of this leading to migration problems for probably millions of users. Clearly they saw the tradeoff was worthwhile. I've spent around 10 years editing and maintaining my own and other people's Ltac1 code, and it is the most time-consuming and frustrating part of any work with Coq.
In my view, a plan for sunsetting Ltac1 (inside Coq itself) will act as a coordination signal for the community to improve tactic code and thus work towards avoiding grueling and pointless maintenance work.
Paolo Giarrusso (Oct 02 2021 at 12:23):Should we have a unified thread for discussion about the Ltac2 migration? While it'll save work in the long term, it'll require lots of work now for the overall community.
Karl Palmskog (Oct 02 2021 at 12:25):best forum might be the Discourse, if we want a serious discussion with lots of links and stats and examples.
Théo Zimmermann (Oct 02 2021 at 12:26):Maybe we should start by advising people to stop writing new Ltac1 code (beyond a certain scale) and reporting any issues they encounter while using Ltac2 instead.
Paolo Giarrusso (Oct 02 2021 at 12:39):From the other discussion, the first answer seems "no transition tutorial exists"...
and sorry I had missed the Discourse suggestion and I had written a few thoughts in https://coq.zulipchat.com/#narrow/stream/278935-Ltac2/topic/Why.20Ltac2.20cannot.20obsolete.20Ltac1.20yet ...
Michael Soegtrop (Oct 02 2021 at 13:47):@Karl Palmskog : I don't think one can compare the move from python 2 to python 3 with the move from Ltac1 to Ltac2. Python 2 and 3 are still very similar languages and the porting effort is minimal. Ltac1 and Ltac2 are completely different languages, although Ltac2 tries to mimic some Ltac1 with notations. But any non trivial code will have pretty much 0 overlap between Ltac1 and Ltac2 - one has to rewrite it from scratch. This might not apply to that extent to proof scripts which mostly use one liners. But it does apply to any serious automation tactics.
Karl Palmskog (Oct 02 2021 at 13:48):if Python2 -> Python3 porting effort was minimal, why did they postpone the sunsetting of Python2 for years? What I heard was that often the effort was substantial.
Paolo Giarrusso (Oct 02 2021 at 13:49):The syntax differences were minimal, but Python3 had Unicode strings rather than "ASCII" strings.
Paolo Giarrusso (Oct 02 2021 at 13:51):so AFAICR you had to redesign anything manipulating strings and debug different indexing problems. Otherwise, AFAICT, Python3 gave very few benefits worth migrating — unlike Ltac2 — so it was also a community consensus problem.
Paolo Giarrusso (Oct 02 2021 at 13:51):Also, they had no interop whatsoever — another metric on which Ltac2 is in fact better.
Paolo Giarrusso (Oct 02 2021 at 13:53):for another data point, I wonder about Scala2->3: good interop, same stdlib, much better language (tho Scala2 wasn't as bad as Ltac1), and lots of community buy-in from their community build.
Paolo Giarrusso (Oct 02 2021 at 13:55):(and yet it's unclear to me if anybody's using it in production — I'm not as close to that world, but there seems to be still quite some inertia!)
Michael Soegtrop (Oct 02 2021 at 15:35):Karl Palmskog said:
if Python2 -> Python3 porting effort was minimal, why did they postpone the sunsetting of Python2 for years? What I heard was that often the effort was substantial.
Well all I am saying is that you should expect that Ltac1->Ltac2 is much worse than Python2->Python3. So you should scale the time line accordingly. Of course there is much more python2 than Ltac1 code out in the wild, but also more people who could port it.
Michael Soegtrop (Oct 02 2021 at 15:37):@Paolo Giarrusso 's argument that cause of the larger benefit in going from Ltac1->Ltac2 there is a larger incentive to do it, but still, one shouldn't underestimate it.
Jim Fehrle (Oct 03 2021 at 22:11):@Karl Palmskog You seemed to be arguing that we should, to some degree, try to force Ltac1 users to migrate to Ltac2 for their own good, which AFAIK will require a very large effort on their part. I expect they would be rather unhappy with that rationale. We should focus on first getting Ltac2 more complete, better documented, etc. and once ready, making the case to users that they should switch. If they are persuaded and usage of Ltac1 declines sufficiently, then discuss a possible change in its status.
(SSR support on Ltac2 is another example of making Ltac2 more complete.)
(We should ask a volunteer to convert something and write up something about how to do conversions. That might identify some improvements to Ltac2 to make conversion easier, or perhaps suggest simple tooling to add to Ltac1 to make conversion easier.)
Other rationales may be more persuasive--e.g. that keeping Ltac1 prevents us from making other major technical improvements (directly or by diverting developer attention from the rest of Coq). I'm skeptical there will be strong enough arguments. Note that Coq developers don't try to fix every bug (except maybe anomalies)--and that's really driven by developers volunteering to fix them.
Python 3 came out in 2008. End of support for Python 2 was in Jan 2020. That's a long transition period.
Théo Zimmermann (Oct 04 2021 at 08:42):While I generally agree with the point that Jim made that Ltac2 should be much improved before we can even discuss the EOL of Ltac1, the case of omega / lia shows that sometimes, stating the intent to eventually deprecate and remove some feature can lead to huge improvements of the replacement features (thanks to significant efforts by users & developers to report and to fix bugs).
Jim Fehrle (Oct 04 2021 at 19:55):It makes sense to state intentions about getting Ltac2 to a more mature state and soliciting help. However, the final removal of omega was trivial. Converting from Ltac1 to Ltac2 will never be trivial, so I wouldn't emphasize the possibility of an Ltac1 EOL now. Instead, make a persuasive case about why Ltac2 is/will be better.
I think better documentation alone would go a long way to encouraging use of/experimentation with Ltac2. I updated the Ltac2 chapter (focusing primarily on syntax) some time ago with a lot of help from @Jason Gross. But, for example, there are a large number of OCaml functions that can be invoked from Ltac2, some of them essential, but I recall the descriptions were quite limited and mostly discoverable only by reading .v files. IIRC many (most?) didn't have any description. Also it seemed that a lot of important principles and intentions were not stated. These are not things I can generate on my own.
There are probably also some key bugs and missing features. When I was updating that chapter, I created a Github Project (https://github.com/coq/coq/projects/41) listing and ranking some possible Ltac2 improvements as a starting point for discussion. It's unclear whether it has been helpful at all.
Karl Palmskog (Oct 04 2021 at 20:11):the switch from omega to lia was far from trivial. Many maintainers had to spend significant time to convert. Even the final removal will likely result in a lot of extra work and keep people off of 8.14. I predict a bunch of projects will be forever stuck on 8.13 due to omega.
Jim Fehrle (Oct 04 2021 at 20:17):EDITED Regarding Ltac2 documentation, see @Andrew Appel's comment from June 2020 in https://github.com/coq/coq/issues/12549. This was after before I updated what I could in the Ltac2 chapter, but I think it likely still applies:
In Coq 8.11 or 8.12beta1, the Ltac2 chapter of the reference manual could be improved by a substantial reorganization, and in places it is incomplete. I have been using Ltac, heavily, for a long time, and I would like to switch to Ltac2. But when I tried it recently, I found that the Ltac2 documentation is difficult to use, and I gave up. [continues with specifics]
Jim Fehrle (Oct 04 2021 at 20:26):@Karl Palmskog Yeah, I may not know the full story. I did the PR that removed the omega code from Coq. I fixed some broken test suites and others fixed the rest. Elapsed time was, I think, about 2 months and the time I spent actually making changes was a few days at most. I did the changes as cleanup solely based on others' recommendation. If I had known it would leave a bunch of projects stuck at 8.13 I would have questioned that.
Karl Palmskog (Oct 04 2021 at 20:41):due to the distributed nature of Coq project maintenance, the consequences of choices made by developers in some version might be felt only 1-2 years later. Let me be clear why I think projects will get stuck: maintainers want to spend as little time as possible to maintain some code that is only one of their dependencies for the interesting work. For example, we had a discussion about how to use Dune for both Coq 8.9 and OCaml code (in my view, extremely difficult and likely requires building Coq 8.9 with Dune) in the SerAPI channel due to a library that will likely never be ported to Coq 8.10 and beyond.
Paolo Giarrusso (Oct 05 2021 at 00:54):In comparison to Ltac2, _learning_ to use lia was trivial. The “lia language” has one word, lia, with 2 possible results. It’s also the same language as omega (up to alpha-renaming). So the whole doesn’t seem comparable to Ltac2 (and I agree with @Jim Fehrle ).
Jim Fehrle (Oct 05 2021 at 01:30):If there are cases where omega works and lia doesn't, that would make for a more difficult conversion.
Théo Zimmermann (Oct 05 2021 at 06:55):Jim Fehrle said:
If there are cases where
omegaworks andliadoesn't, that would make for a more difficult conversion.
That used to be the case. And this is why the effort was significant. It took years to find about and fix these cases, and this work only started thanks to the declared intent of eventually deprecating and removing omega.
Last updated: Oct 13 2024 at 01:02 UTC