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

[CI] Remove coq-bignums before CI #87

Merged
merged 4 commits into from
Feb 16, 2024
Merged

[CI] Remove coq-bignums before CI #87

merged 4 commits into from
Feb 16, 2024

Conversation

proux01
Copy link
Collaborator

@proux01 proux01 commented Feb 13, 2024

Otherwise the test are run with the bignums already in the Docker image rather than the one just built by the CI.

Cc @erikmd (could you check that this looks reasonnable?) @ppedrot (following #86 )

@proux01 proux01 force-pushed the fix_ci branch 2 times, most recently from 83c83b9 to 13e6c81 Compare February 13, 2024 16:34
Otherwise the test are run with the bignums already in the Docker
image rather than the one just built by the CI.
@proux01
Copy link
Collaborator Author

proux01 commented Feb 13, 2024

@erikmd I'm lost with the permissions in the Docker image here, could you have a look?

@erikmd
Copy link
Member

erikmd commented Feb 16, 2024

Thanks @proux01, indeed the opam remove -y coq-bignums before the pinning was the way to go.
However to avoid permission issues, I suggest not directly relying on make, but still using opam commands.

@erikmd erikmd merged commit e6085d6 into master Feb 16, 2024
1 check passed
@erikmd erikmd deleted the fix_ci branch February 16, 2024 14:11
@proux01
Copy link
Collaborator Author

proux01 commented Feb 16, 2024

Fixed, thanks @ppedrot for having noticed that stupid issue.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants