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.

Last updated: May 28 2023 at 20:30 UTC