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. (Ltac2 profiler)
  2. / (precompile Ltac2 for performance)
  3. (hash sets and maps)
  4. (uconstr / notation for unsafe term building)
  5. Edit: (scoped infix notations for int, etc operators) (Previously: <strike> (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. (manipulate patterns)
  2. (fine grained backtrace)

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

  1. 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.) (hash sets and maps).

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

does 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: Sep 25 2023 at 14:01 UTC