"Omit proofs" breaks other proofs because it also skips hints

[Blaisorblade]

The proof of bar breaks when using "Omit proofs" on foo:

Parameter P : nat -> Prop.
Axiom P_Z : P 0.
Axiom P_S : forall {n}, P n -> P (S n).

Lemma foo : P 1.
Proof.
  #[local] Hint Resolve P_Z P_S : core.
  (* ^^ This hint is skipped by PG when skipping [foo]'s proof. *)
  eauto.
Qed.

Lemma bar : P 3.
Proof.
  eauto. (* XXX Will fail when [foo] is skipped. *)
Qed.

This is with an old proof general, but it doesn't look like much relevant has changed since then:

  proof-general                  20220803.1702  dependency            A generic Emacs interface for proof assistants

Ideally, PG would either support this script, warn about occurrences, or document such problems.

If you're wondering "why would you even consider writing this code", at least it can arise temporarily during development, and uses can be hard to find in larger scripts.

[erikmd]

Thanks @Blaisorblade for your detailed report!

Ideally, PG would either support this script, warn about occurrences, or document such problems.

I don't know what is the best solution here. Cc @hendriktews and @ProofGeneral/core WDYT?

[erikmd]

Anyway, this issue does not look surprising to me, knowing the way the omit-proof feature is implemented (it replaces the whole Proof.→Qed. script with Admitted, so no intermediate vernacular will be processed).

I'm not sure if adding #[local] Hint Resolve P_Z P_S : core. at this precise location is really idiomatic. (Does it work if you add it just before the Proof vernacular?) Granted, adding it this way can be useful at development time! as can be the feature of proving a nested lemma during an on-going proof, for example (but nested lemmas have been deprecated since a few releases IIRC).

Of course, I believe filtering the Proof.→Qed. script to at least include some specific vernacular before the Admitted. could be implemented, but maybe some users would be surprised the other way around? What's your opinion?

[Matafou]

Detection of which commands to ignore (like Print which could fail when inside a proof) from the ones we need is going to be difficult really.

[Blaisorblade]

@Matafou wrote:

Detection of which commands to ignore (like Print which could fail when inside a proof) from the ones we need is going to be difficult really.

@erikmd wrote:

Of course, I believe filtering the Proof.→Qed. script to at least include some specific vernacular before the Admitted. could be implemented, but maybe some users would be surprised the other way around? What's your opinion?

Off the top of my head, commands like Opaque, Set/Unset, Hint, Remove Hints and (Require) Import need to be executed even when skipping proofs; I expect no surprise since this handling matches what the STM already does. And not sure what difficulty @Matafou hints at.

I'm not sure if adding #[local] Hint Resolve P_Z P_S : core. at this precise location is really idiomatic.

The real point are changes in the middle of a proof — they can be temporary or permanent, if parts of that proof need different hints, but they're too large for eauto using ...).

[...] nested lemmas have been deprecated since a few releases IIRC.

Neither nested lemmas nor nested hints are deprecated, but PG does not support hints (which cause no Coq warnings), only supports nested lemmas — which are disabled by default and discouraged, but can be re-enabled (deprecation isn't settled).

[Matafou]

The difficulty I am expecting is, as often, not at the moment but for long term maintenance. We will have to maintain a non trivial list of regular expressions from coq versions to coq versions. This is the kind of things we try to avoid as much as possible so that pg remains maintainable.

[hendriktews]

Thanks for reporting, I suggest to do the same here as for #687, see my comment there. I.e., detecting a hint will disable proof omission.

[Matafou]

@hendriktews wait, there are probably dozens of such commands that are allowed inside a proof and should not be ignored. Those pointed by @Blaisorblade: Opaque, Set/Unset, Hint, Remove Hints and (Require) Import but probably a lot more. Like I don't know: Notation, etc.
@Blaisorblade is there a place in coq's code where we can see a list of such commands?

[Matafou]

We had a very short pg meeting today and here are the points and solutions we are considering.
First let us say that:

• To us a side effecting command should be discouraged inside Proof. ... Qed.. Is there really a good reason not to put this Hint outside of the proof? Especially when nested proof (which do have a good reason not to be put outside the proof) are discouraged.
• Even more (personal opinion here): to me the ProofCommand should become (1) mandtory (2) behave almost like a section. So the commands inside it should be local to the proof by default. Then why not allow the #[global] tag and detect it easily.
• So unlike the other issue with omit proof (concerning Let, "Omit proof" on a Let in a section leads to warning #687), it is not clear if we should fix this and to what extend we should mimic the async mode of coqide&co.

We came up with 4 possible solutions + 1 cheap workaround.

Solutions:

1. detect such non local side effecting commands inside proof and
   1. disable omit proof from there position to the end of the file.
   2. disable omit proof only for the current proof
   3. ignore the proof but send the detected commands to coqtop
2. disable the omit proof altogether and secretly keep it for PG authors :-)
3. Workaround: have a special comment which would make the Proof Command not detected as such.

[Blaisorblade]

is there a place in coq's code where we can see a list of such commands?

Currently Coq's STM repeats those commands — I'm not sure if there's a single list, @gares might know. I'm not aware of changes to this list, except for the #[export] attribute.

For the rest: I believe I have valid use-cases, but my team already uses 3 IDEs, so per-IDE coding guidelines don't seem compelling and I'd rather move that part of the discussion upstream: https://coq.zulipchat.com/#narrow/stream/237661-User-interfaces-devs-.26-users/topic/Plans.20for.20hints.20in.20proofs.

---

Regarding alternative designs, if this isn't supported I believe I'd need a warning — Take for instance:

Workaround: have a special comment which would make the Proof Command not detected as such.

That won't be too helpful when I'm stepping through a large proof from a colleague, run into this bug, and I need to debug the proof misbehavior (because the hints are skipped) or the proof slowdown (because the proof was not skipped).

In the past, I have adapted my code to support make vos and deal with Proof using, but that was only possible because the guidelines were machine-checked.

[Matafou]

Right, a Coq tag #[sync] at the beginning of a command would be better.

[gares]

If you want a hack, then any command (i.e. starting with a capital) occurring inside a proof should be kept even if proofs are skipped.

If you don't want a hack, then you should not implement this feature in the UI, since it the job of Coq to know the semantics of the commands, and know which one is has a side effect and which one is pure.

[Blaisorblade]

AFAICT the "non-hacky way" requires the (successors of) the XML protocol, but we don't have a complete replacement yet.

For the other approach, some commands can prefix tactics or commands, will fail spuriously when they prefix tactics, and arguably warrant skipping; off the top of my head I can list Succeed, Timeout, Time, arguably Fail. OTOH, I wouldn't expect any of those wrappers around the interesting commands (outside testsuites or the like).

[Matafou]

Yeah and also commands needing a proof context need be non-ignored Guarded, Check hyp, Eval (...hyp...), Show, etc).

What protocol(s) should we ideally use nowadays? I am a bit lost. I will try to attend he next Coq UI meeting. Maybe the LSP stuff is the right way (emacs has good support for it I heard).

For now I guess a hack would be ok.

[hendriktews]

See also #689.