Skip to content

STM classifier: Guarded and Validate Proof are queries not proof steps - #19383

Merged
coqbot-app[bot] merged 1 commit into
rocq-prover:masterfrom
SkySkimmer:classify-guard
Jul 20, 2024
Merged

STM classifier: Guarded and Validate Proof are queries not proof steps#19383
coqbot-app[bot] merged 1 commit into
rocq-prover:masterfrom
SkySkimmer:classify-guard

Conversation

@SkySkimmer

@SkySkimmer SkySkimmer commented Jul 17, 2024

Copy link
Copy Markdown
Contributor

No description provided.

@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 17, 2024
@SkySkimmer
SkySkimmer requested a review from a team as a code owner July 17, 2024 11:14
@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 17, 2024
@gares

gares commented Jul 17, 2024

Copy link
Copy Markdown
Member

You are right @SkySkimmer , but how did you spot these?

@SkySkimmer

SkySkimmer commented Jul 17, 2024

Copy link
Copy Markdown
Contributor Author

I was looking at #19091 (comment) and wondered if the problem was misclassification of Guarded.
It wasn't but Guarded still wasn't as precisely classified as it could be.

@gares

gares commented Jul 17, 2024

Copy link
Copy Markdown
Member

Note that at some point Undo, for backward compatibility, was made to count only proof steps.
So if you classify guarded as Query it changes that for Guarded.

@herbelin herbelin mentioned this pull request Jul 17, 2024
Merged
@SkySkimmer

SkySkimmer commented Jul 18, 2024

Copy link
Copy Markdown
Contributor Author

@coqbot run full ci

@SkySkimmer SkySkimmer added kind: fix This fixes a bug or incorrect documentation. part: STM State Transition Machine, asynchronous proofs, etc. labels Jul 19, 2024
@SkySkimmer SkySkimmer added this to the 8.21+rc1 milestone Jul 19, 2024
@coqbot-app coqbot-app Bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jul 19, 2024
@SkySkimmer

SkySkimmer commented Jul 19, 2024

Copy link
Copy Markdown
Contributor Author

only added changelog, full ci was green at https://gitlab.inria.fr/coq/coq/-/pipelines/1009037

@SkySkimmer SkySkimmer removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jul 19, 2024
@gares gares self-assigned this Jul 20, 2024
@gares

gares commented Jul 20, 2024

Copy link
Copy Markdown
Member

@coqbot merge now

@coqbot-app
coqbot-app Bot merged commit dedfdf1 into rocq-prover:master Jul 20, 2024
@SkySkimmer
SkySkimmer deleted the classify-guard branch July 22, 2024 11:20
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@gares gares gares approved these changes

Assignees

@gares gares

Labels

kind: fix This fixes a bug or incorrect documentation. part: STM State Transition Machine, asynchronous proofs, etc.

Projects

None yet

Milestone

9.0+rc1

Development

Successfully merging this pull request may close these issues.

2 participants

@SkySkimmer @gares