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

Fix HB 1.7.1 #3298

Merged
merged 2 commits into from
Jan 16, 2025
Merged

Fix HB 1.7.1 #3298

merged 2 commits into from
Jan 16, 2025

Conversation

palmskog
Copy link
Collaborator

cc: @gares

@palmskog palmskog merged commit 2e4ec47 into coq:master Jan 16, 2025
3 checks passed
@palmskog palmskog deleted the fix-hb-1.7.1 branch January 16, 2025 20:17
@erikmd
Copy link
Member

erikmd commented Jan 19, 2025

@palmskog @gares what was the incentive of this upper bound?

FYI, this broke the following build:

https://gitlab.inria.fr/math-comp/docker-mathcomp/-/jobs/5183944#L406

while coq-mathcomp-character built fine before this PR:

https://gitlab.inria.fr/math-comp/docker-mathcomp/-/jobs/5165018#L412

@palmskog
Copy link
Collaborator Author

@erikmd it was to fix crashes with Coq-Elpi 2.4, which as the latest stable version was getting installed. You can see the same fix for HB 1.8 here: #3294

@palmskog
Copy link
Collaborator Author

@erikmd from what I can tell, the build you are referring to (https://gitlab.inria.fr/math-comp/docker-mathcomp/-/jobs/5183944#L406) is actually broken because of the combination of HB 1.7.1 and Coq-Elpi 2.4.0, which is ruled out by this PR.

@erikmd
Copy link
Member

erikmd commented Jan 19, 2025

@palmskog OK!

Thanks for your answer, and apologies for skimming the PR and not realizing earlier that it specifically addressed the issue, not the other way around!

So, I restarted the build and I confirm that the correct dependencies were picked then!

https://gitlab.inria.fr/math-comp/docker-mathcomp/-/jobs/5194087

Thanks

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