Stream: Ltac2

Topic: ✔ Performance of antiquotation


view this post on Zulip Jason Gross (Sep 26 2022 at 15:14):

Does Ltac2 allocate a new evar for every antiquotation? (Things like '($foo $bar))

view this post on Zulip Janno (Sep 26 2022 at 15:17):

EDIT: it is _'s fault that an evar for the type is created.

From Ltac2 Require Import Ltac2.
Set Default Proof Mode "Classic".
Goal True.
  unshelve ltac2:(let x := '(_) in ()); [| |].

seems to indicate that open_constr: creates an evar for the type (and the value, in this case).

view this post on Zulip Gaëtan Gilbert (Sep 26 2022 at 15:18):

no, _ with no type constraint does that

view this post on Zulip Janno (Sep 26 2022 at 15:18):

Oh, I see.

view this post on Zulip Jason Gross (Sep 26 2022 at 15:21):

I guess Ltac2 is smart enough to not generate spurious evars, according to

Require Import Ltac2.Ltac2.
Goal True.
Optimize Proof. (* Evars: 1 -> 1 *)
ltac1:(let v := open_constr:(I) in idtac).
Optimize Proof. (* Evars: 1 -> 1 *)
let v := open_constr:(I) in ().
Optimize Proof. (* Evars: 1 -> 1 *)
ltac1:(let v := constr:(I) in let w := open_constr:(v) in idtac).
Optimize Proof. (* Evars: 1 -> 1 *)
let v := open_constr:(I) in let w := open_constr:($v) in ().
Optimize Proof. (* Evars: 1 -> 1 *)
let v := open_constr:(I) in let w := open_constr:(ltac2:(Control.refine (fun () => v))) in ().
Optimize Proof. (* Evars: 3 -> 1 *)
let v := open_constr:(I) in let w := open_constr:(@conj True True $v $v) in ().
Optimize Proof. (* Evars: 1 -> 1 *)

view this post on Zulip Notification Bot (Sep 26 2022 at 15:22):

Jason Gross has marked this topic as resolved.

view this post on Zulip Gaëtan Gilbert (Sep 26 2022 at 15:22):

why would it even generate an evar?

view this post on Zulip Jason Gross (Sep 26 2022 at 15:26):

I vaguely recall the documentation saying something about how $v is equivalent to ltac2:(Control.refine (fun () => v)), which, if taken literally, suggests evar generation. And I have a vague sense that when I translate Ltac1 to Ltac2 without introducing anything unsafe, it gets a little bit slower, and was wondering if this could be a cause.


Last updated: Jan 31 2023 at 09:01 UTC