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

update extra-dev package of mathcomp-analysis #1971

Merged
merged 4 commits into from
Dec 9, 2021

Conversation

affeldt-aist
Copy link
Contributor

@palmskog
Copy link
Collaborator

palmskog commented Dec 6, 2021

@affeldt-aist it looks like the whole build fails on coq.dev due to coq-mathcomp-bigenough.dev being broken on Coq master. Do you still want me to merge? See for example: https://gitlab.com/coq/opam-coq-archive/-/jobs/1852652993

Do we want to ping bigenough maintainers?

@proux01
Copy link
Contributor

proux01 commented Dec 6, 2021

@palmskog I'm opening a PR on bigenough, so let's wait a bit.

@affeldt-aist
Copy link
Contributor Author

At least, I guess that @CohenCyril would like to know.

@proux01
Copy link
Contributor

proux01 commented Dec 6, 2021

Here it is math-comp/bigenough#5

@palmskog
Copy link
Collaborator

palmskog commented Dec 6, 2021

math-comp/bigenough#5 looks good to me. It would be nice to have it merged so we can test that this package works in CI, but again because we are in extra-dev I can just merge this PR if you want me to.

@proux01
Copy link
Contributor

proux01 commented Dec 8, 2021

Thanks @palmskog , math-comp/bigenough#5 is now merged, feel free to relaunch the CI/merge at your discretion.

@palmskog
Copy link
Collaborator

palmskog commented Dec 8, 2021

@affeldt-aist @proux01 now the build process starts properly, but we are getting the following error:

# File "./theories/topology.v", line 1037, characters 0-67:
# Error: Anomaly "Uncaught exception Not_found."
# Please report at http://coq.inria.fr/bugs/.

Do you still want me to merge?

@proux01
Copy link
Contributor

proux01 commented Dec 9, 2021

@palmskog the error doesn't seem OPAM related, so I would say let's merge this and I'll investigate upstream

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.

3 participants