Skip to content

[parsing] Warn about another recovery mechanism#20870

Merged
coqbot-app[bot] merged 1 commit into
rocq-prover:masterfrom
proux01:forgotten-recovery
Jul 14, 2025
Merged

[parsing] Warn about another recovery mechanism#20870
coqbot-app[bot] merged 1 commit into
rocq-prover:masterfrom
proux01:forgotten-recovery

Conversation

@proux01

@proux01 proux01 commented Jul 6, 2025 •
edited
Loading

Copy link
Copy Markdown
Contributor

Another parsing recovery mechanism forgotten in #17876

At least, a CI run indicates it's almost unused in the whole CI.

@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 6, 2025
@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 Jul 6, 2025
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 6, 2025
@proux01 proux01 force-pushed the forgotten-recovery branch from ff1d3a4 to 09231f2 Compare July 6, 2025 09:42
@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 Jul 6, 2025
@proux01 proux01 changed the title [WIP, parsing] Yet another recovery mechanism [parsing] Warn about another recovery mechanism Jul 6, 2025
@proux01 proux01 added kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: parser The parser (also called gramlib, forked from camlp5) request: full CI Use this label when you want your next push to trigger a full CI. labels Jul 6, 2025
@proux01 proux01 added this to the 9.2+rc1 milestone Jul 6, 2025
@proux01 proux01 force-pushed the forgotten-recovery branch from 09231f2 to 2796077 Compare July 6, 2025 17:41
@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 Jul 6, 2025
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 7, 2025
@proux01 proux01 force-pushed the forgotten-recovery branch from 2796077 to 472275c Compare July 7, 2025 06:40
@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 Jul 7, 2025
@proux01 proux01 marked this pull request as ready for review July 7, 2025 07:48
@proux01 proux01 requested a review from a team as a code owner July 7, 2025 07:48
@proux01

proux01 commented Jul 7, 2025

Copy link
Copy Markdown
Contributor Author

Cc @herbelin

ppedrot
ppedrot reviewed Jul 10, 2025
View reviewed changes
Comment thread gramlib/grammar.ml Outdated
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 11, 2025
@proux01 proux01 force-pushed the forgotten-recovery branch from 472275c to 5398e5b Compare July 11, 2025 06:24
@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 Jul 11, 2025
@ppedrot ppedrot self-assigned this Jul 11, 2025
@ppedrot

ppedrot commented Jul 11, 2025

Copy link
Copy Markdown
Member

CI failure is unrelated, will merge soon if no reactions.

@ppedrot

ppedrot commented Jul 14, 2025

Copy link
Copy Markdown
Member

@coqbot merge now

@coqbot-app coqbot-app Bot merged commit 902ff30 into rocq-prover:master Jul 14, 2025
6 of 8 checks passed
@proux01 proux01 deleted the forgotten-recovery branch July 14, 2025 15:38
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@ppedrot ppedrot ppedrot approved these changes

Assignees

@ppedrot ppedrot

Labels

kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: parser The parser (also called gramlib, forked from camlp5)

Projects

None yet

Milestone

9.2+rc1

Development

Successfully merging this pull request may close these issues.

2 participants

@proux01 @ppedrot