We're getting enough issues that it seems worth prioritizing them. What are your top 5 ltac2 issues?
(feel free to open new issues so you can put them in your top 5 ;))
And two more that didn't quite make top-5:
My priorities are:
1.) mechanisms to compute symbol lists (that is mostly support for iterating over modules I guess) - @Pierre-Marie Pédrot wanted to work on this, not sure where he stands. Afaik there is no issue for it.
2.) https://github.com/coq/coq/issues/16409 (hash sets and maps).
does https://github.com/coq/coq/pull/17482 seem like a useful feature?
Yes, though I'm not sure if I can think of any usecases that aren't subsumed by a hypothetical Ltac2 Compile
I don't think we would have a single use case in our code base for this feature. Everything we'd like to pre-compute affects the implicit state (e.g. typechecking constrs with universes and possibly holes in them). Having said that, I don't actually think that pre-computing anything will bring noticeable speedups any more; at least in our code. Our perf profiles show very little avoidable computation. Instead they show a lot of Ltac2 interpreter overhead.
Last updated: May 28 2023 at 20:30 UTC