Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Validate Proof command: runs typing.ml on the current proof #17467

Merged
merged 2 commits into from Jun 5, 2023
Merged

Validate Proof command: runs typing.ml on the current proof #17467

merged 2 commits into from Jun 5, 2023

Conversation

SkySkimmer
Copy link
Contributor

@SkySkimmer SkySkimmer commented Apr 4, 2023 •
edited

cf some discussion in #17452

Close #9911

Depends #17466 removed dependency

@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 Apr 4, 2023
@SkySkimmer

This comment was marked as outdated.

Sign in to view
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 6, 2023
@coqbot-app coqbot-app bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Apr 6, 2023
@SkySkimmer SkySkimmer added needs: documentation Documentation was not added or updated. needs: changelog entry This should be documented in doc/changelog. labels Apr 6, 2023
@coqbot-app

This comment was marked as outdated.

Sign in to view
@SkySkimmer

This comment was marked as outdated.

Sign in to view
@coqbot-app

This comment was marked as outdated.

Sign in to view
@coqbot-app

This comment was marked as outdated.

Sign in to view
@coqbot-app

This comment was marked as outdated.

Sign in to view
@coqbot-app

This comment was marked as outdated.

Sign in to view
@coqbot-app

This comment was marked as outdated.

Sign in to view
@coqbot-app

This comment was marked as outdated.

Sign in to view
@github-actions github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Apr 7, 2023
@coqbot-app coqbot-app bot added needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. and removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. labels Apr 17, 2023
@SkySkimmer SkySkimmer added the needs: merge of dependency This PR depends on another PR being merged first. label Apr 17, 2023
@github-actions github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Apr 25, 2023
@coqbot-app coqbot-app bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Apr 25, 2023
@SkySkimmer SkySkimmer removed the needs: merge of dependency This PR depends on another PR being merged first. label Apr 25, 2023
@SkySkimmer SkySkimmer added this to the 8.18+rc1 milestone Apr 25, 2023
@SkySkimmer SkySkimmer added request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: documentation Documentation was not added or updated. needs: changelog entry This should be documented in doc/changelog. labels Apr 25, 2023
@coqbot-app coqbot-app bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Apr 25, 2023
@SkySkimmer
Copy link
Contributor Author

Dropped the dependency on #17466 which isn't actually needed for this PR

@SkySkimmer SkySkimmer marked this pull request as ready for review April 25, 2023 13:01
@SkySkimmer SkySkimmer requested review from a team as code owners April 25, 2023 13:01
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 25, 2023
@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 25, 2023
jfehrle
jfehrle reviewed Apr 26, 2023
View reviewed changes
Copy link
Member

@jfehrle jfehrle left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A few wording suggestions.

doc/sphinx/language/core/variants.rst Outdated Show resolved Hide resolved
doc/sphinx/language/core/variants.rst Outdated Show resolved Hide resolved
doc/sphinx/language/core/variants.rst Outdated Show resolved Hide resolved
doc/sphinx/proofs/writing-proofs/proof-mode.rst Outdated Show resolved Hide resolved
doc/sphinx/proofs/writing-proofs/proof-mode.rst Outdated Show resolved Hide resolved
doc/sphinx/proofs/writing-proofs/proof-mode.rst Outdated Show resolved Hide resolved
@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 Apr 27, 2023
@SkySkimmer
Copy link
Contributor Author

@coqbot run full ci

@coqbot-app coqbot-app bot 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 Apr 27, 2023
@SkySkimmer SkySkimmer added the kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. label May 3, 2023
@ppedrot ppedrot self-assigned this May 30, 2023
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label May 30, 2023
@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 May 30, 2023
@ppedrot
Copy link
Member

ppedrot commented Jun 5, 2023

@coqbot merge now

@coqbot-app coqbot-app bot merged commit b5e77f6 into coq:master Jun 5, 2023
12 checks passed
@SkySkimmer SkySkimmer deleted the validate-proof branch June 5, 2023 11:23
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jfehrle jfehrle jfehrle left review comments

@cpitclaudel cpitclaudel cpitclaudel left review comments

@ppedrot ppedrot ppedrot approved these changes

Assignees

@ppedrot ppedrot

Labels
kind: enhancement Enhancement to an existing user-facing feature, tactic, etc.
Projects
None yet
Milestone
8.18+rc1
Development

Successfully merging this pull request may close these issues.

Request: Version of Guarded for "please make sure I'm not going to get an error / anomaly on Qed"
4 participants
@SkySkimmer @ppedrot @jfehrle @cpitclaudel