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.

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

Make Coqargs.parse_args pure #19757

Merged
merged 2 commits into from
Oct 30, 2024
Merged

Make Coqargs.parse_args pure #19757

merged 2 commits into from
Oct 30, 2024

Conversation

SkySkimmer
Copy link
Contributor

@SkySkimmer SkySkimmer commented Oct 23, 2024

We enforce it by removing the dependency on coq-core.lib (which
contains flags.ml) (just for the coqargs module).

Depends:

Overlays:

@SkySkimmer SkySkimmer added the needs: overlay This is breaking external developments we track in CI. label Oct 23, 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 Oct 23, 2024
@SkySkimmer SkySkimmer added this to the 9.0+rc1 milestone Oct 23, 2024
@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 Oct 23, 2024
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Oct 23, 2024
@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 Oct 23, 2024
SkySkimmer added a commit to SkySkimmer/vscoq that referenced this pull request Oct 25, 2024
SkySkimmer added a commit to SkySkimmer/coq-serapi that referenced this pull request Oct 25, 2024
@SkySkimmer SkySkimmer added request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: overlay This is breaking external developments we track in CI. labels Oct 25, 2024
We enforce it by removing the dependency on coq-core.lib (which
contains flags.ml) (just for the coqargs module).
@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 Oct 25, 2024
@SkySkimmer SkySkimmer marked this pull request as ready for review October 25, 2024 11:29
@SkySkimmer SkySkimmer requested review from a team as code owners October 25, 2024 11:29
Copy link
Member

@herbelin herbelin left a comment

Choose a reason for hiding this comment

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

I don't feel having a good overview of the consequences of the changes but ok on my side.

I can merge within a day or two if noone else has particular comments (e.g. regarding the implications it has in vscoq or serapi).

@herbelin herbelin self-assigned this Oct 28, 2024
@herbelin
Copy link
Member

@coqbot merge now

Copy link
Contributor

coqbot-app bot commented Oct 30, 2024

@herbelin: You cannot merge this PR because:

  • There is no kind: label.

@herbelin herbelin added the kind: cleanup Code removal, deprecation, refactorings, etc. label Oct 30, 2024
@herbelin
Copy link
Member

@coqbot merge now

@coqbot-app coqbot-app bot merged commit ed6896f into coq:master Oct 30, 2024
6 checks passed
Copy link
Contributor

coqbot-app bot commented Oct 30, 2024

@herbelin: Please take care of the following overlays:

  • 19757-SkySkimmer-coqargs-pure.sh

SkySkimmer added a commit to coq/vscoq that referenced this pull request Oct 30, 2024
SkySkimmer added a commit to rocq-archive/coq-serapi that referenced this pull request Oct 30, 2024
@SkySkimmer SkySkimmer deleted the coqargs-pure branch October 30, 2024 13:02
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: cleanup Code removal, deprecation, refactorings, etc.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants