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

[CI] Remove Stdlib dep from mathcomp #20291

Merged
merged 1 commit into from
Feb 25, 2025
Merged

[CI] Remove Stdlib dep from mathcomp #20291

merged 1 commit into from
Feb 25, 2025

Conversation

proux01
Copy link
Contributor

@proux01 proux01 commented Feb 25, 2025

@proux01 proux01 added kind: infrastructure CI, build tools, development tools. request: full CI Use this label when you want your next push to trigger a full CI. labels Feb 25, 2025
@proux01 proux01 added this to the 9.1+rc1 milestone Feb 25, 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 25, 2025
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Feb 25, 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 25, 2025
@proux01 proux01 marked this pull request as ready for review February 25, 2025 12:00
@proux01 proux01 requested a review from a team as a code owner February 25, 2025 12:00
@proux01
Copy link
Contributor Author

proux01 commented Feb 25, 2025

CI green

SkySkimmer
SkySkimmer reviewed Feb 25, 2025
View reviewed changes
dev/ci/scripts/ci-elpi_test.sh
Comment on lines -12 to +13
make test-core
make examples
make test-apps
make -j1 all-tests
make -j1 all-examples
Copy link
Contributor

Choose a reason for hiding this comment

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

What's going on here?

Copy link
Contributor

@SkySkimmer SkySkimmer Feb 25, 2025 •
edited
Loading

Choose a reason for hiding this comment

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

is there some reason not to do dune build --root . @runtest? or some elpi specific alias if they don't want to use runtest

Copy link
Contributor Author

Choose a reason for hiding this comment

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

make is calling dune multiple times in parallel and dune doesn't like it (I got error messages like "dune is already running, if you're sure, remove _build/.lock")

Copy link
Contributor Author

Choose a reason for hiding this comment

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

It wouldn't be just @runtest, there are a few diferent targets.

Copy link
Contributor

Choose a reason for hiding this comment

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

make is calling dune multiple times in parallel and dune doesn't like it (I got error messages like "dune is already running, if you're sure, remove _build/.lock")

The makefile should say .NOTPARALLEL: then

Copy link
Contributor Author

Choose a reason for hiding this comment

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

C.f. LPCIC/coq-elpi#785

@SkySkimmer SkySkimmer self-assigned this Feb 25, 2025
@SkySkimmer
Copy link
Contributor

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 0109537 into coq:master Feb 25, 2025
6 checks passed
@proux01 proux01 mentioned this pull request Feb 25, 2025
Merged
@proux01 proux01 deleted the ci-mathcomp-dep branch February 25, 2025 14:27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@SkySkimmer SkySkimmer SkySkimmer approved these changes

Assignees

@SkySkimmer SkySkimmer

Labels
kind: infrastructure CI, build tools, development tools.
Projects
None yet
Milestone
9.1+rc1
Development

Successfully merging this pull request may close these issues.
2 participants
@proux01 @SkySkimmer