Stream: Coq devs & plugin devs

Topic: invariants of the tactic engine


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

How strong of an invariant is it that all evars definable by unification have been defined? (I'm getting lots of anomalies in tactics like eval pattern and exact)

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

what does definable mean?

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

All (or most) constraints of the form ?ev == <term not containing ?ev> have been resolved. Especially, things like f : ?e1, x : ?e2 |- f x gives that ?e1 should be resolved to forall x : ?e2, ?e3, and when it's not, there seem to be lots of anomalies that crop up

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

See, e.g., https://github.com/coq/coq/issues/16540#issuecomment-1258255868

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

you can have postponed constraints
see eg https://github.com/coq/coq/pull/13371

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

So should all tactics be robust in the face of arbitrary postponed constraints, and I should expect the constraints that need not be postponed to be recovered and applied as needed? Or is this region of the tactic engine explicitly not supported?


Last updated: Feb 05 2023 at 20:03 UTC