Coq-HoTT
Coq-HoTT copied to clipboard
HoTT
Automation and tactics
Over the next few years, it will be desirable to slowly shift to writing new automation in one of the successor tactic languages to Ltac, such as Ltac2 or Elpi. As the paper motivating Ltac2 points out, Ltac is slow and relies on many heuristics to "automagically" do the right thing for the user, while the newer tactic languages are faster and more composable. In addition, my impression is that the Elpi API is fairly comprehensive and the Ltac2 API is steadily growing while the Ltac API is static, so Ltac2 should be more expressive than Ltac in the long run.
There are some related questions:
- in what language should new tactics be written? Personally I like the Elpi language but Ltac2 is the more conservative approach, both in terms of not requiring additional dependencies and being similar to Ltac. (Other major libraries like math-comp use Elpi, so I think it's an acceptable dependency.)
- what are the downsides and how severe are they? One question is stdlib dependency: I will defer discussion of Ltac2 until Rocq 9 is on opam and I can play with it, it has some problems in Coq 8.*. Elpi afaik does not depend on anything in the stdlib but I will double check. (Cyril Cohen stated that HoTT-compatibility is one goal for the Trocq project which uses both Elpi and this library, so others have interest in keeping Elpi separate from the stdlib)
I consider Ltac2 to be not well documented. There are a few tutorials online. If we wanted to use this language for automation I would personally contribute some tutorials for the Coq-HoTT wiki to explain the usage of Ltac2. Elpi is well documented imo.
I don't know anything about either option, so I have no opinion at this point. @JasonGross might have some thoughts.
Regarding Elpi
Adding elpi to the library is not technically feasible right now due to the lack of Dune support. This is something that has been a problem for a while and is not something that is going to be solved easily. There is a lack of motivation / money from the developers.
Mathcomp has fully moved to use elpi which is quite good as it has reduced a lot of boilerplate. On the other hand, there is a visible performance penalty, so its not a straight upgrade. I think using elpi in this library would take some effort and there would have to be a big payoff for it to be worth it.
Elpi also isn't great with universe polymorphism last I checked, which is something that we would need before even considering using it in the library. The situation may have changed however.
I wouldn't mind having some stuff that relies on elpi sitting in a separate library, kind of like what we have with HoTT.Contrib. It would definitely be worthwhile to investigate, but it wouldn't be something I personally would put a lot of time into. It seems like there will be many problems before something practical is feasible.
Regarding ltac2
Ltac2 is poorly documented as you have said, and for us has some teething problems due to noinit and the way it relies on other plugins. These are problems that can be fixed, but since we are one of the only libraries to have these issues, it has not been a big priority upstream.
In general, its hard to say if moving to a new tactic language would be beneficial. There are some ltac tactics we have written that are very good at their job, and others with lots of room for improvement. But importantly, we mostly know how they work.
I'm open to having ltac wrappers around efficiently implemented ltac2 tactics. That seems like a good trade off. Basically ltac2 answers the question of "what if I could write this tactic in straight ocaml without introducing a plugin". There are situations where such custom tactics would benefit enormously, say for bookkeeping during a complicated argument. Then it seems sensible to put the effort into partially using ltac2.
Regarding automation in general
There are situations which ltac2 or elpi might benefit enormously, but that would come at the cost of perhaps making maintaining the rest of the library a bit harder. The question of "is automation good?" is not really a "well-defined" question since it ultimately depends on what you are automating.
Having proofs explicitly laid out is a huge benefit for readers and people learning. Having proofs be automated is a huge benefit for people writing the proofs. Maximising the benefits in these two groups can have some tension, which is why there is a spectrum of mathematical literature from expert to introductory. In the library we have a mix of the two, but I think it is an acceptable amount. Most newcomers can understand some of the basic proofs on types and algebraic structures, whereas some proofs like BlakersMassey might start to look alien. This is all before any fancy tactics, so I think having something that does the hard work for you might leave you in ignorance and make a proof harder to understand or appreciate.
Those are some of my thoughts on the matter.
I'd like to read more about some of the critiques you brought up of Elpi. For Dune compatibility, Elpi is currently packaged via Dune though I'm aware that there is some annoying hack involved to keep track of dependencies, so I am not sure I understand this comment. For performance issues do you have a link to a Zulip discussion or benchmark on this issue? And on universe polymorphism can you be concrete? I am aware that the main "refine" tactic has a flag to ignore universes which is enabled by default. I also have filed a GitHub issue that the weak head normal form tactic doesn't handle universe polymorphic terms correctly.
Elpi itself is built using dune, but coq-elpi itself has some issues. The issue is that coq.theory stanzas have no way of keeping track of .elpi files which are required by the coq-elpi plugin. I proposed a design some time back https://github.com/ocaml/dune/pull/9591 but there were some design issues we couldn't agree on and it was never finished.
Performance issues are from speaking to people about the mathcomp port to Hierarchy Builder which IIRC is around a 10% slowdown in build time. There are multiple reasons for this. Partly its about elpi just being slow, there is probably room for speed up. Another issue was the use of modules as namespaces. I don't recall the details exactly, but if you ask on the Coq Zulip the elpi and mathcomp people should be able to give exact figures. This is not a deal-breaker in practice, but it is something to be aware of. I don't have a link unfortunately as this was from in person discussions from more than 2 years ago.
I think i was misremembering the universe polymorphism issue with elpi. I was probably thinking about hierarchy builder having little support https://github.com/math-comp/hierarchy-builder/issues/281. That issue is pointing towards the new universe algo in Coq which doesn't appear to be progressing at the moment.
The issue with loading prelude should not be a problem with Ltac2; we can just copy and replicate the .v files as HoTT.Ltac2.* or similar and it should work fine.
Early benchmarks of Coq 8.21 showed significant performance improvements for math-comp and coq-elpi, this is an old convo so I'm not sure how reliable it is but the benchmarks in this post seems like a positive sign https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/Performance.20of.208.2E21.20.28the.20first.20release.20of.20Rocq.2C.20Jan.202025.29
Also, regarding *.elpi files that seems more like a minor inconvenience to me. We can just write the tactics in *.v files using the Elpi Accumulate syntax around it.
After a recent PR that was merged, Ltac2 will be much more compatible with noinit in the next Rocq release. I have opened a documentation PR to add technical documentation to many types and functions defined in the Ltac2 Rocq API. The Rocq Platform Docs project wants to write some Ltac2 tutorials.