Stream: Coq devs & plugin devs

Topic: Ltac2 abstract and evars

Gaëtan Gilbert (Jun 16 2023 at 12:00):

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?

Jason Gross (Jun 18 2023 at 18:22):

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.

Gaëtan Gilbert (Jun 19 2023 at 10:37):

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

Last updated: Nov 29 2023 at 21:01 UTC