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

I guess it can be reduced to something like this

```
Require Import Ltac2.Ltac2.
Import Ltac2.Constr.
Fixpoint naryT n := match n with 0 => nat | S k => nat -> naryT k end.
Fixpoint nary_aux n acc : naryT n := match n with 0 => acc | S k => fun x => nary_aux k (x+acc) end.
(* given (fun x1 x2 .. xn => v) produce (fun x1 x2 .. xn => S v) *)
Ltac2 rec rebuild_aux avoid f :=
match Unsafe.kind f with
| Unsafe.Lambda bnd bdy =>
let x := Binder.name bnd in
let t := Binder.type bnd in
let x :=
match x with
| Some x => x
| None => ident:(x)
end
in
let x := Fresh.fresh avoid x in
let avoid := Fresh.Free.union avoid (Fresh.Free.of_ids [x]) in
let xc := Unsafe.make (Unsafe.Var x) in
let res :=
Constr.in_context x t
(fun () =>
(* let f := eval cbv head beta in ($f $xc) in *)
let f := Unsafe.substnl [xc] 0 bdy in
let res := rebuild_aux avoid f in
exact $res)
in
res
| _ => '(S $f)
end.
Ltac2 rebuild f := rebuild_aux (Fresh.Free.of_goal()) f.
(* quick version, but unsafe *)
Ltac2 rec qrebuild f :=
match Unsafe.kind f with
| Unsafe.Lambda bnd bdy =>
Unsafe.make (Unsafe.Lambda bnd (qrebuild bdy))
| _ => Unsafe.make (Unsafe.App 'S [|f|])
end.
Goal True.
Time
Ltac2 Eval
let f := eval cbv -[Nat.add] in (nary_aux 10000 0) in
let _ := qrebuild f in
().
(* rebuild:
10 -> 0.001s
100 -> 0.03s
200 -> 0.1s
300 -> 0.25s
1000 -> 3.5s
2000 -> 19s
10000 -> many s
rebuild but use Unsafe.substnl on the body from Unsafe.Lambda instead of cbv head beta:
10 -> 0s
100 -> 0.02s
200 -> 0.08s
300 -> 0.18s
1000 -> 1.9s
2000 -> 7.5s
10000 -> many s, also takes many GB of RAM but not very fast
qrebuild:
10 -> 0s
100 -> 0.001s
200 -> 0.002s
300 -> 0.004s
1000 -> 0.025s
2000 -> 0.1s
10000 -> 3.6s, takes about 1GB
*)
```

delaying the substnl with

```
(* given (fun x1 x2 .. xn => v) produce (fun x1 x2 .. xn => S v) *)
Ltac2 rec rebuild_aux avoid f args :=
let f :=
match Unsafe.kind f with
| Unsafe.Lambda _ _ => f
| _ => Unsafe.substnl args 0 f
end
in
match Unsafe.kind f with
| Unsafe.Lambda bnd bdy =>
let x := Binder.name bnd in
let t := Binder.type bnd in
let x :=
match x with
| Some x => x
| None => ident:(x)
end
in
let x := Fresh.fresh avoid x in
let avoid := Fresh.Free.union avoid (Fresh.Free.of_ids [x]) in
let xc := Unsafe.make (Unsafe.Var x) in
let res :=
Constr.in_context x t
(fun () =>
let res := rebuild_aux avoid bdy (xc::args) in
exact $res)
in
res
| _ => '(S $f)
end.
Ltac2 rebuild f := rebuild_aux (Fresh.Free.of_goal()) f [].
```

seems to take less RAM but not be faster

seems to take less RAM

I don't understand why btw

3 messages were moved from this topic to #Ltac2 > Constr.in_context perf issues by Gaëtan Gilbert.

Last updated: Oct 12 2024 at 13:01 UTC