## Stream: Ltac2

### Topic: ✔ Performance of antiquotation

#### Jason Gross (Sep 26 2022 at 15:14):

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

#### 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).

#### Gaëtan Gilbert (Sep 26 2022 at 15:18):

no, `_` with no type constraint does that

Oh, I see.

#### 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 *)
``````

#### Notification Bot (Sep 26 2022 at 15:22):

Jason Gross has marked this topic as resolved.

#### Gaëtan Gilbert (Sep 26 2022 at 15:22):

why would it even generate an evar?

#### 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