Skip to content

Warning for missing "Proof" command and error on duplicate or late "Proof"#21865

Merged
coqbot-app[bot] merged 1 commit intorocq-prover:masterfrom
SkySkimmer:warn-missing-proof
Apr 30, 2026
Merged

Warning for missing "Proof" command and error on duplicate or late "Proof"#21865
coqbot-app[bot] merged 1 commit intorocq-prover:masterfrom
SkySkimmer:warn-missing-proof

Conversation

@SkySkimmer
Copy link
Copy Markdown
Contributor

@SkySkimmer SkySkimmer commented Apr 1, 2026 •
edited
Loading

The warning is also emitted if Next Obligation has no Proof even though it seems nobody says Proof after Next Obligation. This seems reasonable but could be avoided (forbidding Proof after Next Obligation) if we want to.

Overlays (backwards compatible):

@SkySkimmer SkySkimmer requested review from a team as code owners April 1, 2026 13:23
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 1, 2026
@SkySkimmer SkySkimmer requested a review from a team as a code owner April 1, 2026 13:23
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 1, 2026
@SkySkimmer SkySkimmer added kind: feature New user-facing feature request or implementation. kind: user messages Error messages, warnings, etc. labels Apr 1, 2026
@SkySkimmer SkySkimmer added this to the 9.3+rc1 milestone Apr 1, 2026
@ppedrot ppedrot self-assigned this Apr 1, 2026
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 1, 2026
@SkySkimmer SkySkimmer force-pushed the warn-missing-proof branch from 6ab9110 to f0310db Compare April 1, 2026 14:51
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 1, 2026
@SkySkimmer SkySkimmer changed the title Warning for missing "Proof" command Warning for missing "Proof" command and error on duplicate or late "Proof" Apr 1, 2026
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 1, 2026
@SkySkimmer SkySkimmer force-pushed the warn-missing-proof branch from f0310db to 09b800e Compare April 1, 2026 14:51
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 1, 2026
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 1, 2026
@SkySkimmer SkySkimmer force-pushed the warn-missing-proof branch from 09b800e to fa3165a Compare April 1, 2026 14:53
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 1, 2026
@SkySkimmer
Copy link
Copy Markdown
Contributor Author

SkySkimmer commented Apr 1, 2026 •
edited
Loading

Additional notes:

  • as Restart vs. Proof using flagging #13743 says, Restart puts the state as it was after the proof opening command (Goal Lemma etc), not after Proof. This is why I edited rocqdomain.py to insert a Proof after Restart.
  • Succeed and Fail cannot modify the state, so eg Goal True. Succeed idtac. idtac. will say the warning twice.

@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 1, 2026
@SkySkimmer SkySkimmer force-pushed the warn-missing-proof branch from fa3165a to 346906d Compare April 1, 2026 17:21
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 1, 2026
@proux01 proux01 mentioned this pull request Apr 2, 2026
Merged
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 2, 2026
@SkySkimmer SkySkimmer force-pushed the warn-missing-proof branch from 346906d to 716f64c Compare April 2, 2026 12:53
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 20, 2026
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 20, 2026
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 21, 2026
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 21, 2026
silene
silene reviewed Apr 21, 2026
View reviewed changes
Comment thread doc/sphinx/addendum/type-classes.rst Outdated
@SkySkimmer SkySkimmer added needs: progress Work in progress: awaiting action from the author. request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: progress Work in progress: awaiting action from the author. labels Apr 21, 2026
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 22, 2026
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 22, 2026
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 22, 2026
@ppedrot
Copy link
Copy Markdown
Member

ppedrot commented Apr 26, 2026

I'll leave a bit of time for other people to comment before merging. (I've always been an advocate of Proof being mandatory, but for some reason there are people not of that opinion.)

@thomas-lamiaux
Copy link
Copy Markdown
Contributor

thomas-lamiaux commented Apr 26, 2026

I've always been an advocate of Proof being mandatory, but for some reason there are people not of that opinion.

Great to know but why 😅

@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 28, 2026
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 28, 2026
@SkySkimmer
Copy link
Copy Markdown
Contributor Author

SkySkimmer commented Apr 28, 2026

Removed the overlay file, everything should be merged upstream

@SkySkimmer
Copy link
Copy Markdown
Contributor Author

SkySkimmer commented Apr 29, 2026

@coqbot run full ci

@ppedrot
Copy link
Copy Markdown
Member

ppedrot commented Apr 30, 2026

Bedrock2 seems to be still lacking an overlay, or its dependencies haven't been updated yet.

@SkySkimmer
Copy link
Copy Markdown
Contributor Author

SkySkimmer commented Apr 30, 2026

@coqbot run full ci

@SkySkimmer
Copy link
Copy Markdown
Contributor Author

SkySkimmer commented Apr 30, 2026

green now

@ppedrot
Copy link
Copy Markdown
Member

ppedrot commented Apr 30, 2026

OK, let's merge then. @coqbot merge now

@coqbot-app coqbot-app Bot merged commit b050918 into rocq-prover:master Apr 30, 2026
11 of 12 checks passed
@SkySkimmer SkySkimmer deleted the warn-missing-proof branch April 30, 2026 16:02
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@silene silene silene left review comments

@thomas-lamiaux thomas-lamiaux thomas-lamiaux left review comments

@ppedrot ppedrot ppedrot approved these changes

Assignees

@ppedrot ppedrot

Labels

kind: feature New user-facing feature request or implementation. kind: user messages Error messages, warnings, etc.

Projects

None yet

Milestone

9.3+rc1

Development

Successfully merging this pull request may close these issues.

4 participants

@SkySkimmer @ppedrot @thomas-lamiaux @silene