Paolo Giarrusso (Feb 07 2023 at 21:29): Paolo Giarrusso (Feb 07 2023 at 21:29):Should hints/commands inside proofs be supported further or change semantics? For instance
Lemma foo : P 1.
Proof.
...
#[local] Hint ...
..
Qed.
but this includes further constructs like Remove Hints, Opaque, (Require) Import.
I ask because a new Proof General feature would need special handling similar to the STM, and PG devs ( @Pierre Courtieu @Hendrik Tews @Erik Martin-Dorel ) seem uneasy with the idea in https://github.com/ProofGeneral/PG/issues/688, and argue such hints are a bad idea (I disagree) and should probably be scoped to the proof anyway (I agree, but that'd be a large semantic change).
Ali Caglayan (Feb 07 2023 at 21:33):I think Require inside a proof is definitely not something we want.
Ali Caglayan (Feb 07 2023 at 21:39):I think it would be good for Hints inside proofs to revert their mutation of the global state at the end of a proof. That way it would be more compatible with skipping proofs.
Ali Caglayan (Feb 07 2023 at 21:40):If it needs to be global, then it should go outside of the proof.
Ali Caglayan (Feb 07 2023 at 21:40):This would of course require a change to the semantics of adding hints in Coq, but I don't think it would be an unpopular or difficult change. cc @Emilio Jesús Gallego Arias
Ali Caglayan (Feb 07 2023 at 21:41):I'm tempted to think that Opaque and Import should also behave similarly.
Maxime Dénès (Feb 07 2023 at 21:59):There are two ways you may want to change the scoping :
Maxime Dénès (Feb 07 2023 at 22:01):For Opaque, it depends what you want to do at Qed time in terms of unfolding strategy.
Paolo Giarrusso (Feb 07 2023 at 22:05):FWIW: today's semantics when the STM skip proofs is to replay those commands. Making them local by default sounds reasonable, but what about migration? The PG issue suggests supporting #[global] as well (and then #[export]).
Re Require, I agree, and that's _almost_ trivial to avoid, except that dropping Require can change the semantics so this is error-prone (even in manual changes and especially automatically) — From Coq Import Arith. doesn't exist, and Import Arith or Import Coq.Arith.Arith. can pick up _other_ modules.
Erik Martin-Dorel (Feb 07 2023 at 22:30):Thanks @Paolo Giarrusso for raising this discussion upstream.
Actually as proposed by @Pierre Courtieu in https://github.com/ProofGeneral/PG/issues/688#issuecomment-1420601232, there are mostly 3 possible strategies to address Paolo's request:
Hence a few questions:
A. how to "detect such non local side effecting commands" ? is it easy to find a snippet in Coq's codebase that declare them?
B. would strategy 3. be a tractable solution from your viewpoint? (either with a comment, or better, with a #[global] parsed attribute?)
in which case, an Opaque plus. command would only impact plus within the proof, while #[global] Opaque plus. would also keep it opaque afterwards. (Maybe this approach, removing side-effects from inline Commands by default would also simplify the STM implementation?)
Cc-ing @Enrico Tassi & @Emilio Jesús Gallego Arias as well, in case they would miss this brainstorming discussion…
Ali Caglayan (Feb 07 2023 at 22:35):Maxime Dénès said:
For
Opaque, it depends what you want to do at Qed time in terms of unfolding strategy.
Is this true? I was under the impression that Qed ignored opaque?
Gaëtan Gilbert (Feb 07 2023 at 22:36):A. how to "detect such non local side effecting commands" ? is it easy to find a snippet in Coq's codebase that declare them?
Coq detects them using the "vernac classifier" https://github.com/coq/coq/blob/master/vernac/vernac_classifier.ml
plugins which add commands register those commands with the classifier (actual data for plugin commands is in vernacextend.ml) when they are declared, this is the CLASSIFIED BY in .mlg files https://github.com/coq/coq/blob/8f1590f7840d0dff71fa9b7a7bbc1ed01d779359/plugins/ltac/extratactics.mlg#L245
the commands which get replayed are the "VtSideff" ones IIRC
some other commands may get treated specially (IIRC Definition gets treated specially for instance)
Gaëtan Gilbert (Feb 07 2023 at 22:38):Is this true? I was under the impression that Qed ignored opaque?
I think he means
Lemma foo : bla.
Proof.
Opaque bar.
some tactic.
Qed. (* when checking the body of foo, bar is opaque *)
(* when checking the body of foo, bar is opaque *)
but that only means that the kernel _prefers_ to not unfold bar
Gaëtan Gilbert (Feb 07 2023 at 22:40):that's what Opaque means isn't it?
Paolo Giarrusso (Feb 07 2023 at 22:45):just clarifying, since the topic's so confusing and Ali had a question
Paolo Giarrusso (Feb 07 2023 at 22:46):@Erik Martin-Dorel I'd be happy to add #[local], #[export] or #[global] as appropriate — and I'll note #[local] already means something else — but we need a warning
Paolo Giarrusso (Feb 07 2023 at 22:47):and a warning in proof general wouldn't help when I'm using PG to step proofs from users of other IDEs
Enrico Tassi (Feb 08 2023 at 07:09):I'd personally change the scope of global directives, making them end with Qed. I did propose so ten years ago, but it never got too much traction.
Maybe a #[proof_local] thing is the way to go.
I don't know what omit-proof is exactly, but if you end up facing these problems it probably means it should not be implemented in the UI.
Karl Palmskog (Feb 08 2023 at 07:16):I understand this is a feature that some interfaces may want, but is this discussion really an UI issue?
Karl Palmskog (Feb 08 2023 at 07:17):(or, can I move it to #Coq devs & plugin devs, where I think it belongs, and which has larger audience)
Paolo Giarrusso (Feb 08 2023 at 09:34):I don't know what omit-proof is exactly, but if you end up facing these problems it probably means it should not be implemented in the UI.
omit-proofs is a poor man's STM without the XML protocol — it simply admits earlier proofs. I agree new UIs should eventually make this unnecessary, but all current PG alternatives have downsides.
Notification Bot (Feb 08 2023 at 09:35):This topic was moved here from #User interfaces devs & users > Plans for hints in proofs by Karl Palmskog.
Emilio Jesús Gallego Arias (Feb 08 2023 at 18:18):From my point of view I don't care so much what the semantics of such a command is, in the sense that coq-lsp can handle all of them as long as indeed they declare how they update the state correctly.
So indeed, if a hint command will cause an update to the global hint database, then everything that depends on that database must be rebuilt, but it doesn't, then I'm happy too.
Emilio Jesús Gallego Arias (Feb 08 2023 at 18:19):So indeed, with my methodology, Paolo request could be implemented by simply having a proof-local copy of the relevant parts of the summary. Unfortunately this requires changes in Coq, I proposed we do something like this a few years ago but we didn't advance much.
Emilio Jesús Gallego Arias (Feb 08 2023 at 18:20):It is also fine to skip a proof but have global-updating commands, if the data flow is registered correctly
Paolo Giarrusso (Feb 09 2023 at 00:50):Part of the motivation is that PG uses simpler tech, and the cleanups are generally desirable anyway; I've seen many Coq users assume that hints in proofs are proof-local, and they were by no means just beginners
Last updated: Nov 29 2023 at 18:01 UTC