Gaëtan Gilbert (Mar 02 2023 at 15:24): 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 ;))
Jason Gross (Mar 02 2023 at 16:02):And two more that didn't quite make top-5:
Janno (Mar 02 2023 at 16:05): 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).
Gaëtan Gilbert (Apr 07 2023 at 15:04):does https://github.com/coq/coq/pull/17482 seem like a useful feature?
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
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.
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?
Gaëtan Gilbert (Feb 01 2024 at 15:24):mechanisms to compute symbol lists
I'll be looking into this next
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
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".
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.
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!
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
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.)
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)
Gaëtan Gilbert (Mar 22 2024 at 14:40):do you have a test showing the perf issues with in_context?
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
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)
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
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)
Jason Gross (Mar 22 2024 at 16:59):The legend is ordered from slowest at the top to fastest at the bottom
Gaëtan Gilbert (May 27 2024 at 14:48):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
Gaëtan Gilbert (May 27 2024 at 15:25):seems to take less RAM
I don't understand why btw
Notification Bot (May 28 2024 at 11:44):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