Stream: Ltac2

Topic: ✔ CompCert exploit tactic in Ltac2

Notification Bot (Sep 08 2023 at 12:59):

Michael Soegtrop has marked this topic as resolved.

Jason Gross (Sep 08 2023 at 13:35):

Michael Soegtrop said:

So a difference between Ltac2 refine and Ltac refine is that Ltac1 refine includes a shelve_unifiable.

Do you think I should open an issue to adjust the behaviour of Ltac2 refine (the notation, not the Control.refine function) to that of Ltac1 refine?

Yes. For ease of translation from Ltac1, I think the version that does not shelve should be named simple refine, and the version that shelves everything should be named eexact. If this is too ad-hoc, then instead there should be another file "Ltac1CompatNotations", or something, which (re)defines notations to more closely match with Ltac1, maybe making them all deprecated (with no scheduled removal date) to indicate that they should not be used in new scripts, only in porting.

Michael Soegtrop (Sep 08 2023 at 13:41):

I think most people who build elaborate automation based on Ltac2 use the functions and not the notations and few people are using Ltac2 in proof mode, so my expectation is that changing this breaks close to nothing, but one would have to see. The nice thing about changing the notations is that it is then very explicit what they do.

Jason Gross (Sep 08 2023 at 18:10):

My thought with compat was less about whether or not the change breaks things and more about whether or not Ltac1's design here is good enough to keep in Ltac2 (e.g., maybe this difference was deliberate on @Pierre-Marie Pédrot 's part)

Last updated: Nov 29 2023 at 22:01 UTC