Stream: Ltac2

Topic: Performance worse than Ltac1

Jason Gross (Sep 30 2022 at 16:06):

Is Ltac2 supposed to be ~uniformly slower than Ltac1 when I'm not using unsafe features? Am I porting my code wrong? I have 9 examples where porting some Ltac1 to basically-equivalent Ltac2 results in a slowdown of 5--10 seconds (in one case, 30 seconds):
https://github.com/mit-plv/fiat-crypto/pull/1389#issuecomment-1263755032

Janno (Sep 30 2022 at 16:12):

Are you using in_context? I have found it to be so slow that I had to ban it entirely from any piece of code that is executed more than a constant number of times.

Jason Gross (Sep 30 2022 at 16:12):

For example ("Port strip_invalid_or_fail to Ltac2"), it seems that replacing Ltac1

lazymatch term with
| fun _ => ?f => f
| fun invalid : ?T => ?f
=> do some stuff then eventually fail with a big number
end

in code that never hits the second branch, with Ltac2

lazy_match! term with
| fun _ => ?f => f
| _ => do some stuff then eventually Control.throw
end

results in an 8 second increase in compilation time (6s in one file, 2s in another)

Jason Gross (Sep 30 2022 at 16:14):

@Janno I am unfortunately using in_context, because I see no other way to make use of typeclass resolution, Pattern.instantiate, and Std.eval_pattern under binders. (But the Ltac1 is doing constr:(fun x => match P return _ with P' => ltac:(let P := (eval cbv delta [P'] in P') in ... in exact ...) end), which I expect is about as slow as Constr.in_context?)

Jason Gross (Sep 30 2022 at 16:14):

I don't see why Constr.in_context should be slower than the corresponding way of recursing under binders in Ltac1

Janno (Sep 30 2022 at 16:16):

I can't speak to the Ltac1 alternative(s) since I never even dared to write complicated automation in Ltac1. All I know is that replacing in_context by unsafe alternatives made the difference between infeasible and feasible in multiple tactics I wrote.

Janno (Sep 30 2022 at 16:16):

But it seems your problem is more general than that given your example above.

Janno (Sep 30 2022 at 16:17):

Which commit does the lazy_match! example correspond to?

Jason Gross (Sep 30 2022 at 16:17):

Yeah... I don't suppose you have an unsafe alternative to typeclass resolution, Constr.type, or to Std.eval_pattern and Pattern.instantiate?

Jason Gross (Sep 30 2022 at 16:18):

Here's another change bizarrely adding 4 seconds in one file (unless I'm just seeing noise, but I don't think that's it):

      Ltac change_pattern_base_subst_default_relax_internal term :=
        lazymatch (eval pattern (@pattern.base.subst_default_relax), (@pattern.base.unsubst_default_relax) in term) with
        | ?f _ _
          => let base := fresh "base" in
             let P := fresh "P" in
             let t := fresh "t" in
             let evm := fresh "evm" in
             (eval cbv beta in (f (fun base P t evm => @pattern_base_subst_default_relax' base t evm P) (fun base P t evm => @pattern_base_unsubst_default_relax' base t evm P)))
        end.

vs

      Ltac2 change_pattern_base_subst_default_relax (term : constr) : constr :=
        Reify.debug_wrap
          "change_pattern_base_subst_default_relax" Message.of_constr term
          Reify.should_debug_fine_grained Reify.should_debug_fine_grained (Some Message.of_constr)
          (fun ()
           => lazy_match! (eval pattern (@pattern.base.subst_default_relax), (@pattern.base.unsubst_default_relax) in $term) with
              | ?f _ _
                => (eval cbv beta in ($f (fun base P t evm => @pattern_base_subst_default_relax' base t evm P) (fun base P t evm => @pattern_base_unsubst_default_relax' base t evm P)))
              end).

(Reify.debug_wrap is a bunch of if statements on Ints for debugging purposes, unless I enable debug in which case it does a lot more)

Janno (Sep 30 2022 at 16:19):

Does $term force type checking of term?

Jason Gross (Sep 30 2022 at 16:19):

Which commit does the lazy_match! example correspond to?

https://github.com/mit-plv/rewriter/commit/135c8598a / https://github.com/mit-plv/fiat-crypto/pull/1389/commits/a9c0eb53f33c3b6eb4da0068d5bd78d54d805de7

Jason Gross (Sep 30 2022 at 16:21):

Does $term force type checking of term?

Yeah, it does. (retyping, though, not full typing) You think that's the issue here?

Janno (Sep 30 2022 at 16:21):

On one hand I am happy to see that I am not the only one that ends up with hundreds of lines of code in a single Ltac2 function but on the other hand I cannot parse what is going on in that commit :D

Jason Gross (Sep 30 2022 at 16:22):

Yeah, it doesn't help that most of it is dead code. Look at Ltac2 strip_invalid_or_fail vs Ltac strip_invalid_or_fail_internal, and ignore everything after the first branch of the lazymatch (which is guaranteed to always error fatally; since the code builds the second branch is never reached)

Janno (Sep 30 2022 at 16:23):

Avoiding retyping/type checking has made a huge difference for me in the past but only if the terms are not small. I still sometimes use constr:(f $x $y) if I know the terms up front, if I know that they are very small, and if I cannot be bothered to construct the term unsafely.

Jason Gross (Sep 30 2022 at 16:23):

The pattern commit is https://github.com/mit-plv/fiat-crypto/pull/1389/commits/f5f05d9faa51ede2450f7bc93d1deaf2b36dfb33 / https://github.com/mit-plv/rewriter/commit/d61b34590

Jason Gross (Sep 30 2022 at 16:24):

Hmm, yeah, I guess I can cut out the typing in that function. I figured that since there was so much typechecking going on already, one more wouldn't make a difference, but I could be wrong

Jason Gross (Sep 30 2022 at 16:25):

(Seems as likely to be the if Int.le 6 0 then debug stuff else normal stuff statements? Or is there no way that can add up to 6s overhead even if it's called on every subterm?)

Jason Gross (Sep 30 2022 at 16:28):

This one is a 13s overhead, distributed across multiple files:

      Ltac replace_type_try_transport_internal term :=
        lazymatch term with
        | context[@type.try_transport ?base_type ?try_make_transport_base_type_cps ?P ?t ?t]
          => let v := constr:(@type.try_transport base_type try_make_transport_base_type_cps P t t) in
             let term := lazymatch (eval pattern v in term) with
                         | ?term _ => (eval cbv beta in (term (@Some _)))
                         end in
             replace_type_try_transport_internal term
        | _ => term
        end.

vs

      Ltac2 rec replace_type_try_transport (term : constr) : constr :=
        Reify.debug_wrap
          "replace_type_try_transport" Message.of_constr term
          Reify.should_debug_fine_grained Reify.should_debug_fine_grained (Some Message.of_constr)
          (fun ()
           => let res := match! term with
                         | context[?v]
                           => lazy_match! v with
                              | @type.try_transport ?base_type ?try_make_transport_base_type_cps ?p ?t ?t
                                => Some v
                              end
                         | _ => None
                         end in
              match res with
              | Some v
                => let term := lazy_match! (eval pattern $v in $term) with
                               | ?term _ => (eval cbv beta in ($term (@Some _)))
                               end in
                   replace_type_try_transport term
              | None => term
              end).

Janno (Sep 30 2022 at 16:28):

I didn't find Int functions to be slow in any way but I guess they could add up if you have tens of thousands of them

Jason Gross (Sep 30 2022 at 16:28):

I guess this could plausibly be the same issue with overtypechecking

Gaëtan Gilbert (Sep 30 2022 at 16:28):

could lazy_match! be slower?

Jason Gross (Sep 30 2022 at 16:29):

Could be, that's part of why I'm asking here. (I'll probably try to dig into this more in the next couple of days)

Janno (Sep 30 2022 at 16:29):

I use lazy_match! in extremely performance sensitive code and it hasn't shown up on any profiles IIRC

Janno (Sep 30 2022 at 16:30):

In fact, I used to inspect terms unsafely and switched back to lazy_match! later when I realized there was no performance benefit (and the code was much nicer to read)

Janno (Sep 30 2022 at 16:31):

This shouldn't be very hard to test, though.

Jason Gross (Sep 30 2022 at 16:32):

But it does seem plausible that my issue is just "Ltac2 doesn't have good support for building trivial constrs with convenient notation without introducing extra typechecking" Like, I can't write eval pattern $foo in $bar without introducing extra typechecking in Ltac2, but in Ltac1, eval pattern foo in bar does not first retype foo and bar

Jason Gross (Sep 30 2022 at 16:33):

(Retyping test:

Require Import Ltac2.Ltac2. Import Constr.Unsafe. Ltac2 Eval let v := make (Rel (-1)) in let __ := '$v in ().
(* Error: Anomaly "in retyping: unbound local variable." Please report at http://coq.inria.fr/bugs/. *)

)

Janno (Sep 30 2022 at 16:39):

I did some testing: unsafe term inspection is definitely faster than lazy_match! but I suspect the overhead will be negligible compared to other things a normal tactic would be doing. lazy_match! is also definitely faster than lazymatch in my tests so it is unlikely to be the culprit.

From Ltac2 Require Import Ltac2.

Ltac2 rec test_lazy_match t :=
    lazy_match! t with
    | S ?n => test_lazy_match n
    | 0 => ()
    end.

Ltac test_lazymatch t :=
  lazymatch t with
  | S ?n => test_lazymatch n
  | 0 => idtac
  end.

Import Constr. Import Unsafe.
Ltac2 rec test_unsafe t :=
  match kind t with
  | App h args =>
    if Int.equal (Array.length args) 1 then
      test_unsafe (Array.get args 0)
    else
      Control.throw (Invalid_argument None)
  | Constructor _ _ => ()
  | _ => Control.throw (Invalid_argument None)
  end.

Ltac2 Eval let n := '5000 in Control.time None (fun () => test_lazy_match n). (* min: 0.025s *)
Goal True. ltac1:(let n := constr:(5000) in time (test_lazymatch n)). Abort. (* min: 0.045s *)
Ltac2 Eval let n := '5000 in Control.time None (fun () => test_unsafe n). (* min: 0.006s *)

Jason Gross (Sep 30 2022 at 16:41):

Here's a test for retyping:

Require Import Coq.ZArith.ZArith.
Definition foo := Eval vm_compute in Z.div_eucl.
Require Import Ltac2.Ltac2.
Goal True.
  Time ltac1:(let v := (eval cbv delta [foo] in foo) in do 5 time do 100 (idtac; let _ := eval pattern v in v in idtac)).
  (* Tactic call ran for 0.276 secs (0.276u,0.s) (success)
Tactic call ran for 0.247 secs (0.247u,0.s) (success)
Tactic call ran for 0.222 secs (0.222u,0.s) (success)
Tactic call ran for 0.214 secs (0.214u,0.s) (success)
Tactic call ran for 0.234 secs (0.234u,0.s) (success)
Finished transaction in 1.199 secs (1.197u,0.002s) (successful)
 *)
  Time let v := (eval cbv delta [foo] in foo) in do 5 (time (do 100 (let _ := eval pattern $v in $v in ()))).
  (*
Tactic call ran for 0.214 secs (0.214u,0.s) (success)
Tactic call ran for 0.184 secs (0.184u,0.s) (success)
Tactic call ran for 0.26 secs (0.26u,0.s) (success)
Tactic call ran for 0.209 secs (0.209u,0.s) (success)
Tactic call ran for 0.223 secs (0.223u,0.s) (success)
Finished transaction in 1.096 secs (1.096u,0.s) (successful) *)
  Time let v := (eval cbv delta [foo] in foo) in do 5 (time (do 100 (let _ := Std.eval_pattern [(v, Std.AllOccurrences)] v in ()))).
  (*
Tactic call ran for 0.113 secs (0.113u,0.s) (success)
Tactic call ran for 0.094 secs (0.094u,0.s) (success)
Tactic call ran for 0.07 secs (0.07u,0.s) (success)
Tactic call ran for 0.073 secs (0.073u,0.s) (success)
Tactic call ran for 0.068 secs (0.068u,0.s) (success)
Finished transaction in 0.425 secs (0.425u,0.s) (successful)*)

What I am confused about, though, what I don't see here but do see in my actual code, is that Ltac2 is fractionally slower than Ltac1...

Janno (Sep 30 2022 at 16:41):

I am not sure about the whole eval thing. I've never used these notations in Ltac2 but they must be backed by something that accepts constr, right? So in the most trivial cases you can call that instead of using the notation with $term

Gaëtan Gilbert (Sep 30 2022 at 16:42):

in Ltac1, eval pattern foo in bar does not first retype foo and bar

it does though AFAICT

Jason Gross (Sep 30 2022 at 16:42):

Huh, interesting

Jason Gross (Sep 30 2022 at 16:44):

So in the most trivial cases you can call that instead of using the notation with $term

Yeah, and you can even see the desugared version with Print Ltac2. But eval cbv beta delta [id] in $x is so much nicer than Std.eval_cbv { Std.rBeta := true; Std.rMatch := false; Std.rFix := false; Std.rCofix := false; Std.rZeta := false; Std.rDelta := false; Std.rConst := [reference:(id)] } x

Gaëtan Gilbert (Sep 30 2022 at 16:45):

for instance

Goal True -> True.
intros T.
let x := constr:(T) in
clear T;
let p := eval pattern x in x in
idtac p.
(* Error: Cannot reinterpret "T" in the current environment. *)

which is from https://github.com/coq/coq/blob/477c5aac7a92134de0c5660f9b9b71fcd06ed0e8/pretyping/globEnv.ml#L135-L140

Jason Gross (Sep 30 2022 at 16:47):

@Gaëtan Gilbert The performance numbers back up Ltac1 eval pattern doing constr retyping, but are you sure that message comes from retyping before doing pattern rather than typechecking after doing pattern (because pattern needs to ensure that the abstracted term is well-typed)

Gaëtan Gilbert (Sep 30 2022 at 16:48):

it's from the x in pattern x (because it's the first one that gets looked at)

Jason Gross (Sep 30 2022 at 16:48):

I've reported https://github.com/coq/coq/issues/16586 (for retyping)

Gaëtan Gilbert (Sep 30 2022 at 16:49):

ltac variables in a constr expr are just vars and they get handled by pretyping which returns a type
so the type needs to come from somewhere

Janno (Sep 30 2022 at 16:49):

I would suggest a different solution: just make the notation accept tactic instead of constr

Jason Gross (Sep 30 2022 at 16:49):

@Janno how would that help?

Gaëtan Gilbert (Sep 30 2022 at 16:50):

constr needs a type so can't avoid retyping

Janno (Sep 30 2022 at 16:52):

It would help in the same way that it helps with Ltac2's refine notation: if you have the constr already, you can just pass it without any extra type checking.

Janno (Sep 30 2022 at 16:53):

I don't think the JIT compilation proposal is entirely sound: depending on how things are retyped/type checked it could be that avoiding the check in $v actually changes the behavior of the tactic

Janno (Sep 30 2022 at 16:53):

(I am thinking about universe constraints here)

Gaëtan Gilbert (Sep 30 2022 at 16:54):

retyping does not add univ constraints

Janno (Sep 30 2022 at 16:55):

In that case the transformation might be sound

Gaëtan Gilbert (Sep 30 2022 at 16:55):

it is not sound because retyping can fail

Janno (Sep 30 2022 at 16:55):

Oh, right :)

Jason Gross (Sep 30 2022 at 16:55):

@Janno I believe the behavior will only change if you made v unsafely, or if you have changed the environment since making v

Janno (Sep 30 2022 at 16:55):

Well, that's almost all my tactics

Jason Gross (Sep 30 2022 at 16:56):

Sure, but it's not the responsibility of the convenience notation for Std.eval_pattern to do these checks for you

Jason Gross (Sep 30 2022 at 16:57):

(and the only change in behavior is that it will now succeed in some cases where it previously failed)

Jason Gross (Sep 30 2022 at 16:58):

Also, here's another one: @Janno do you see anything in https://github.com/mit-plv/rewriter/commit/61a85a68c that could add 8s? (My current guess is Constr.eq_nounivs, which I had to hand-roll because it's not provided)

Jason Gross (Sep 30 2022 at 16:59):

Also, how the heck does https://github.com/mit-plv/rewriter/commit/1cfbb6bb6 add 14s?!

Jason Gross (Sep 30 2022 at 16:59):

The change is

-              let term := '(ltac2:(Control.refine (fun () => deep_substitute_beq base_interp_beq only_eliminate_in_ctx term))) in
+              let term := deep_substitute_beq base_interp_beq only_eliminate_in_ctx term in
               let term := Std.eval_cbv (strategy:([base.interp_beq $base_interp_beq_head])) term in
-              let term := '(ltac2:(Control.refine (fun () => remove_andb_true term))) in
+              let term := remove_andb_true term in

Jason Gross (Sep 30 2022 at 17:01):

And https://github.com/mit-plv/rewriter/commit/f6a79ed59 adds 30s, but is too big for me to reasonably debug :-(

I guess I should just go back and get rid of all the needless retyping...

Gaëtan Gilbert (Sep 30 2022 at 17:01):

some backtracking or other monad nonsense? what happens if you do let term := once (deep_substitute ...)?

Janno (Sep 30 2022 at 17:04):

The same thing might apply to https://github.com/mit-plv/rewriter/commit/61a85a68c. I see match! without once around it

Janno (Sep 30 2022 at 17:05):

Unless your Constr.eq_nounivs implementation is something that doesn't simply call the corresponding OCaml function..

Jason Gross (Sep 30 2022 at 17:09):

My Constr.equal_nounivs: https://github.com/mit-plv/rewriter/blob/447661334668ba1cc73753b294b306aa781e454e/src/Rewriter/Util/Tactics2/Constr.v#L69-L185 (Is there a way to write a plugin that extends Ltac2 with the corresponding OCaml function? It's not currently exposed :'-( )

Gaëtan Gilbert (Sep 30 2022 at 17:10):

what function isn't exposed?

Jason Gross (Sep 30 2022 at 17:12):

My question is: can I write a plugin that does https://github.com/coq/coq/pull/16532 ? (The relevant Ltac2 tac2core functions seem to be private to tac2core, and I'm not sure how much of the Ltac2 implementation I have to copy/paste to get this.)

Gaëtan Gilbert (Sep 30 2022 at 17:13):

doesn't it just use

let define_primitive name arity f =
  Tac2env.define_primitive (pname name) (mk_closure arity f)

let define2 name r0 r1 f = define_primitive name (arity_suc arity_one) begin fun x y ->
  f (Value.repr_to r0 x) (Value.repr_to r1 y)
end

?
Value is an alias of Tac2ffi

Jason Gross (Sep 30 2022 at 17:17):

If that's all it needs (mk_closure, pname, arity_suc, and arity_one are all public?), that would be nice, I should try it

Gaëtan Gilbert (Sep 30 2022 at 17:18):

pname is let pname s = { mltac_plugin = "coq-core.plugins.ltac2"; mltac_tactic = s } (which type is from tac2expr) so you want to define a different one for your plugin
mk_closure and arities are from tac2ffi

Jason Gross (Sep 30 2022 at 17:20):

Thank you, I'll try that!

Jason Gross (Sep 30 2022 at 17:21):

@Janno

I see match! without once around it

match! is a notation for Ltac2.Pattern.one_match0 which is defined at https://github.com/coq/coq/blob/477c5aac7a92134de0c5660f9b9b71fcd06ed0e8/user-contrib/Ltac2/Pattern.v#L115 as Ltac2 one_match0 t m := Control.once (fun _ => multi_match0 t m).

Jason Gross (Sep 30 2022 at 17:24):

@Janno

I would suggest a different solution: just make the notation accept tactic instead of constr

I was confused by this, but I think I now understand how it works. This would require adding constr:(...) to get the current behavior in most cases, but would let you insert variables as-is, right? I am a fan of this solution

Jason Gross (Oct 01 2022 at 06:19):

@Gaëtan Gilbert I'm getting Error: Unbound module Tac2env. I can open Proofview and open Ltac2_plugin, but I can't open Ltac2, nor open Ltac2_plugin, nor open Tac2env

Jason Gross (Oct 01 2022 at 06:20):

I guess this is because coq_makefile generates a Makefile that has FINDLIBPKGS = -package coq-core.plugins.ltac $(CAMLPKGS)? (Should this be fixed upstream?)

Jason Gross (Oct 01 2022 at 06:24):

Reported as https://github.com/coq/coq/issues/16591

Jason Gross (Oct 01 2022 at 06:44):

@Gaëtan Gilbert I don't think I can really define a different pname? There's no way to use Ltac2 external unless I start with coq-core.plugins (reported at https://github.com/coq/coq/issues/16592)

Janno (Oct 01 2022 at 08:40):

Oh, I had no idea match! was using once internally. Time to simplify some code, I guess..

Janno (Oct 01 2022 at 08:41):

In that case, yes, I suspect your equality function might be to blame for the slowdown. The Ltac2 interpreter isn't the slowest but there is no way it's going to come close to OCaml performance for stuff like that.

Last updated: Oct 12 2024 at 13:01 UTC