Stream: Ltac2

Topic: issue prioritization


view this post on Zulip Gaëtan Gilbert (Mar 02 2023 at 15:24):

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

view this post on Zulip Jason Gross (Mar 02 2023 at 16:02):

  1. https://github.com/coq/coq/issues/10111 (Ltac2 profiler)
  2. https://github.com/coq/coq/issues/10107 / https://github.com/coq/coq/issues/10106 (precompile Ltac2 for performance)
  3. https://github.com/coq/coq/issues/16409 (hash sets and maps)
  4. https://github.com/coq/coq/issues/13977 (uconstr / notation for unsafe term building)
  5. 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:

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

view this post on Zulip Janno (Mar 02 2023 at 16:05):

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

view this post on Zulip Michael Soegtrop (Mar 03 2023 at 08:32):

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

view this post on Zulip Gaëtan Gilbert (Apr 07 2023 at 15:04):

does https://github.com/coq/coq/pull/17482 seem like a useful feature?

view this post on Zulip Jason Gross (Apr 07 2023 at 16:34):

Yes, though I'm not sure if I can think of any usecases that aren't subsumed by a hypothetical Ltac2 Compile

view this post on Zulip Janno (Apr 11 2023 at 09:36):

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.

view this post on Zulip Gaëtan Gilbert (Feb 01 2024 at 15:24):

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?

view this post on Zulip Gaëtan Gilbert (Feb 01 2024 at 15:24):

mechanisms to compute symbol lists

I'll be looking into this next

view this post on Zulip Jason Gross (Feb 07 2024 at 21:57):

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

view this post on Zulip Jason Gross (Feb 07 2024 at 22:07):

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".

view this post on Zulip Jason Gross (Feb 07 2024 at 22:10):

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.

view this post on Zulip Janno (Feb 08 2024 at 09:16):

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!

view this post on Zulip Janno (Feb 08 2024 at 09:17):

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

view this post on Zulip Rodolphe Lepigre (Feb 10 2024 at 13:13):

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

view this post on Zulip Jason Gross (Mar 21 2024 at 18:03):

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)

view this post on Zulip Gaëtan Gilbert (Mar 22 2024 at 14:40):

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

view this post on Zulip Jason Gross (Mar 22 2024 at 16:44):

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

view this post on Zulip Jason Gross (Mar 22 2024 at 16:48):

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)

view this post on Zulip Jason Gross (Mar 22 2024 at 16:50):

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

view this post on Zulip Jason Gross (Mar 22 2024 at 16:59):

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

view this post on Zulip Jason Gross (Mar 22 2024 at 16:59):

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


Last updated: May 19 2024 at 18:02 UTC