Skip to content

Backports 9.0 - #20055

Closed
ppedrot wants to merge 3 commits into
rocq-prover:v9.0from
ppedrot:backports-9.0
Closed

Backports 9.0#20055
ppedrot wants to merge 3 commits into
rocq-prover:v9.0from
ppedrot:backports-9.0

Conversation

@ppedrot

@ppedrot ppedrot commented Jan 14, 2025

Copy link
Copy Markdown
Member

No description provided.

@ppedrot ppedrot added the request: full CI Use this label when you want your next push to trigger a full CI. label Jan 14, 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 Jan 14, 2025
@ppedrot
ppedrot changed the base branch from master to v9.0 January 14, 2025 21:18
@ppedrot

ppedrot commented Jan 14, 2025

Copy link
Copy Markdown
Member Author

@coqbot run full ci

@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 Jan 15, 2025
@ppedrot ppedrot added this to the 9.0+rc1 milestone Jan 15, 2025
@ppedrot ppedrot added the request: full CI Use this label when you want your next push to trigger a full CI. label Jan 15, 2025
@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 Jan 15, 2025
@ppedrot ppedrot added the request: full CI Use this label when you want your next push to trigger a full CI. label Jan 16, 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 Jan 16, 2025
@ppedrot ppedrot added the request: full CI Use this label when you want your next push to trigger a full CI. label Jan 16, 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 Jan 16, 2025
@ppedrot ppedrot added the request: full CI Use this label when you want your next push to trigger a full CI. label Jan 20, 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 Jan 20, 2025
@ppedrot ppedrot added the request: full CI Use this label when you want your next push to trigger a full CI. label Jan 20, 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 Jan 20, 2025
@ppedrot ppedrot added the request: full CI Use this label when you want your next push to trigger a full CI. label Jan 21, 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 Jan 21, 2025
@ppedrot ppedrot added the request: full CI Use this label when you want your next push to trigger a full CI. label Jan 21, 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 Jan 21, 2025
@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 Jan 23, 2025
@ppedrot ppedrot added the request: full CI Use this label when you want your next push to trigger a full CI. label Feb 20, 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 Feb 20, 2025
@ppedrot ppedrot added the request: full CI Use this label when you want your next push to trigger a full CI. label Feb 28, 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 Feb 28, 2025
@ppedrot ppedrot added the request: full CI Use this label when you want your next push to trigger a full CI. label Mar 7, 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 Mar 7, 2025
@ppedrot ppedrot added the request: full CI Use this label when you want your next push to trigger a full CI. label Mar 10, 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 Mar 10, 2025
@ppedrot ppedrot added the request: full CI Use this label when you want your next push to trigger a full CI. label Mar 11, 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 Mar 11, 2025
@ppedrot ppedrot modified the milestones: 9.0.0, 9.0.1 Mar 11, 2025
@ppedrot ppedrot added the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 4, 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 Sep 4, 2025
@ppedrot ppedrot added the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 5, 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 Sep 5, 2025
@ppedrot ppedrot added the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 5, 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 Sep 5, 2025
SkySkimmer
SkySkimmer reviewed Sep 25, 2025
View reviewed changes
Comment thread doc/sphinx/changes.rst
(`#19842 <https://github.com/coq/coq/pull/19842>`_,
by Gaëtan Gilbert).

Changes in 9.0.1

@SkySkimmer SkySkimmer Sep 25, 2025

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

this should be in a PR on master which would then get backported here

@ppedrot ppedrot Sep 25, 2025

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

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

Let's do that then.

@ppedrot ppedrot Sep 25, 2025

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

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

See #21120. I assume I also have to remove the corresponding rst files when backporting?

@SkySkimmer SkySkimmer Sep 25, 2025

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

yes

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@SkySkimmer SkySkimmer SkySkimmer left review comments

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@ppedrot @SkySkimmer