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.

I think with 8.19 we have some good progress. Some of the issues remain open though. Also maybe some new issues should be high priority.

@Jason Gross (or anyone else but Jason is the only one with a >2 element list) do you want to post your current top 5?

mechanisms to compute symbol lists

I'll be looking into this next

I am sorry to say I haven't been using Ltac2 enough recently to have an up-to-date wishlist

I guess filling out the standard notations to achieve feature-parity with all of the implemented-in-OCaml Ltac1 tactics is a decent default thing to aim for, so we can suggest Ltac2 as a replacement for Ltac1 without having to say "but for these things you need to jump back to Ltac1".

Might be nice to also have an `ltac1to2`

tool for automatically porting existing scripts from Ltac1 to Ltac2. Not any of the tricky stuff (though maybe it would be nice to automatically wrap such things in the ltac2->ltac1->ltac2 machinery required), but something that, e.g., we could run over the standard library and have it mostly automatically port 80%+ of the proofs from Ltac1 to Ltac2.

One thing that comes up again and again is me missing unused variables (which so far have always been indicated a bug somewhere). Having a warning for that would be amazing!

While I was typing this @Rodolphe Lepigre already opened an issue for it: https://github.com/coq/coq/issues/18637

I just created another issue that might be a good candidate: https://github.com/coq/coq/issues/18656.

(This is about abstract types and related features.)

Belatedly @Gaëtan Gilbert I think maybe the next big missing feature I am aware of is https://github.com/coq/coq/issues/18364 (performant manual context management)

do you have a test showing the perf issues with in_context?

Not a great test, but if I were to write one I'd look at reification of terms with long chains with many binders. There's https://github.com/mit-plv/rewriter/blob/1cd64f2598427f8f4ddcbe453fb61bff32fd0d3a/src/Rewriter/Language/Reify.v#L70-L95, but this code is currently only used in error messages. I guess the real performance test is that at https://github.com/mit-plv/rewriter/blob/1cd64f2598427f8f4ddcbe453fb61bff32fd0d3a/src/Rewriter/Language/Reify.v#L780 I am passing around an extension to the context manually (`x :: ctx_tys`

), and I would like to instead be using a genuine context that I can feed to things like `match!`

and `cbv`

. If you insert a variant of `Constr.in_context`

there that allows returning `(constr * constr) option`

, I expect performance to suffer significantly

Actually, this is probably a good test case: https://github.com/coq-community/coq-performance-tests/blob/64012925b8e16392bb64ba031d7bffd1478af36c/PerformanceExperiments/Reify/Ltac2Reify.v#L74-L84 vs https://github.com/coq-community/coq-performance-tests/blob/64012925b8e16392bb64ba031d7bffd1478af36c/PerformanceExperiments/Reify/Ltac2Reify.v#L212-L219. (And all the fresh code above L74 also needs to be optimized)

There's a performance plot at https://coq-community.github.io/coq-performance-tests/dev-native/Reify-Ltac2.svg

Compare actual reif for Ltac2LowLevel (solid yellow square) with actual reif for Ltac2 (blue oplus, shows up in the far left of the plot)

The legend is ordered from slowest at the top to fastest at the bottom

Last updated: May 19 2024 at 18:02 UTC