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 CI by reverting to coq_makefile #90

Merged
merged 3 commits into from
Jul 15, 2024
Merged

Fix CI by reverting to coq_makefile #90

merged 3 commits into from
Jul 15, 2024

Conversation

pi8027
Copy link
Member

@pi8027 pi8027 commented Jul 11, 2024

Let me run CI here since the multinomials package does not seem to compile with coq-master.

Closes #75
Closes #76

@pi8027
Copy link
Member Author

pi8027 commented Jul 11, 2024

Does anyone know how to fix this error? @gares @proux01

  # File "./src/xfinmap.v", line 2, characters 0-68:
  # Error: Cannot load elpi_elpi.dummy: no physical path bound to elpi_elpi

@proux01
Copy link
Contributor

proux01 commented Jul 12, 2024

Unforunately, I fear this is a dune related issue and I have no clue what dune is doing wrong.
The easiest and fastest fix is probably to revert to coq_makefile here for now.

src/dune Outdated Show resolved Hide resolved
@pi8027
Copy link
Member Author

pi8027 commented Jul 15, 2024

Also, this patch breaks the build of multinomials with Coq <= 8.18...

@Alizter
Copy link
Contributor

Alizter commented Jul 15, 2024

Does the version of elpi change between Coq versions? It seems strange that the coq.theory elpi_elpi is missing only for older versions?

@Alizter
Copy link
Contributor

Alizter commented Jul 15, 2024

Looks like the version of coq-elpi is changing between the mathcomp versions. In 2.2.0 is requires the extra elpi_elpi theory that was added. I don't really have time to help hacking around this and dune doesn't really support the way elpi requires things to be built (nor do we have the manpower to improve this at the moment). So perhaps the best thing to do is revert to coq_makefile here.

@pi8027
Copy link
Member Author

pi8027 commented Jul 15, 2024

@proux01 @Alizter Thanks for the feedback.

Since I couldn't find a way to make the build of multinomials compatible both with Coq 8.18 and master, I'm going to revert it to coq_makefile now. CC: @strub.

@pi8027 pi8027 changed the title Remove mathcomp-dev:coq-8.16 and mathcomp-dev:coq-8.17 from CI Fix CI by reverting to coq_makefile Jul 15, 2024
@pi8027
Copy link
Member Author

pi8027 commented Jul 15, 2024

This PR should also close #75 and #76. @haansn08

@pi8027
Copy link
Member Author

pi8027 commented Jul 15, 2024

Since this PR is blocking the merge of coq-community/apery#24, I'm merging this now, but please let me know if you see any issues.

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.

make install fails
3 participants