In https://github.com/coq/coq/pull/17704 we found out that abstract breaks when variables in the ltac/ltac2 environment contain evars and are used by the tactic

For instance

```
Require Import Ltac2.Ltac2.
Goal unit.
let x := '_ in
let _ := '(eq_refl : $x = tt) in
abstract (exact $x).
```

produces "anomaly evar ?X4 was not declared" (reminder: `'term`

means `open_constr:(term)`

in ltac2)

The corresponding ltac1 code

```
let x := open_constr:(_) in
let _ := open_constr:(eq_refl : x = tt) in
abstract (exact x).
```

works fine because ltac1 dynamically evar-normalizes constr variables in the environment (https://github.com/coq/coq/blob/ba574c6870652a804a14491fecb14ed97912337f/plugins/ltac/tacinterp.ml#L318-L333 and caller line 1160)

but it can still be caught out, eg

```
let x := open_constr:(_) in
let _ := open_constr:(eq_refl : x = tt) in
let tac := exact x in (* <- this is a closure *)
abstract tac.
```

is an anomaly.

Meanwhile `open_constr`

in ltac1 and ltac2 evar normalizes the produced constr.

This is useful because it makes less impactful for instance `let x := '([0]%list) in abstract exact $x`

works instead of failing due to the `[0]`

becoming `@cons ?nat 0 (@nil ?nat)`

with side definition `?nat := nat`

.

OTOH it has significant performance impacts because building terms with open_constr incurs full evar-normalization at every step, ie the underlying issue of https://github.com/coq/coq/issues/13977 which people work around using uconstr. (the same issue happens with `constr:()`

but IMO it is more acceptable that `constr:()`

evar normalizes).

For this reason I want to remove the evar normalization from open_constr, but I'm not sure how to deal with the `abstract`

problem.

The easiest way would be to add some `evar_normalize : constr -> constr`

and let people call that if they use abstract but it seems not user friendly.

We could also try to change `abstract`

to avoid resetting the evar map for its tactic run, I don't know what the implications would be though.

What do people think?

We could also try to change abstract to avoid resetting the evar map for its tactic run, I don't know what the implications would be though.

I'd be inclined to try out this one first, assuming it doesn't completely break `abstract`

. Insofar as people are relying on this sort of behavior (is there any chance this could be the reason `abstract omega`

/ `abstract lia`

was less memory-hungry than `omega`

/ `lia`

?), this behavior should be separated off into its own dedicated tactic.

https://github.com/coq/coq/pull/17745

Last updated: Oct 13 2024 at 01:02 UTC