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
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:
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.
open_constr in ltac1 and ltac2 evar normalizes the produced constr.
This is useful because it makes less impactful for instance
let x := '(%list) in abstract exact $x works instead of failing due to the
@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
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
lia?), this behavior should be separated off into its own dedicated tactic.
Last updated: Nov 29 2023 at 21:01 UTC