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 ;))

- https://github.com/coq/coq/issues/10111 (Ltac2 profiler)
- https://github.com/coq/coq/issues/10107 / https://github.com/coq/coq/issues/10106 (precompile Ltac2 for performance)
- https://github.com/coq/coq/issues/16409 (hash sets and maps)
- https://github.com/coq/coq/issues/13977 (uconstr / notation for unsafe term building)
- Edit: https://github.com/coq/coq/issues/17330 (scoped infix notations for int, etc operators) (Previously: <strike> https://github.com/coq/coq/issues/12808 (infix notations in Ltac2 (is this still open?) (actually the thing I want is to be able to have scoped notations for all the list and bool and int operators in Ltac2, maybe I should open a separate bug))</strike>)

And two more that didn't quite make top-5:

- https://github.com/coq/coq/issues/11641 (manipulate patterns)
- https://github.com/coq/coq/issues/16546 (fine grained backtrace)

- https://github.com/coq/coq/pull/16394 Allow Ltac2 notations from within Ltac1 (I'll add more later)

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