-
Notifications
You must be signed in to change notification settings - Fork 414
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
pkg: Zarith doesn't build #8931
Comments
The issue here is really that |
Yeah, that's a shame. There's a few packages like that we're going to add workarounds for. I think the simplest thing to do for now is to introduce our own overlay system like duniverse. We will need very few overlays in comparison to duniverse. Also, it would be nice if we had a way to mark packages as being incompatible with dune's package management. cc @Leonidas-from-XIV who worked with something like this in duniverse already. |
Zarith is able to be packaged up for Nix, but obviously that doesn't use the opam file. They configure with the correct paths which is perhaps something we could do. Or at least modify the OPAM file for Zarith to allow. I think that is a non controversial change. Duniverse had a stronger constraint of using dune to build everything whereas we don't really have that. Therefore I am not yet convinced an overlay systems is needed yet. |
Or we can use the dune build system Hugo write. Any of those options will require an overlay until the upstream package is updated. |
Overall I'd say the UX for this is pretty bad at large. What we would need is
The other UX hiccup is when users fail to add the repository locking fails in annoying ways, so if we wanted to support this I would strongly suggest |
Is the latest error after fixing |
I can't reproduce this issue anymore. My experiment is to take this empty dune project that depends on zarith: https://github.com/gridbugs/dune-pkg-dashboard/tree/main/bonsai-deps/zarith There's a chance that you'll get this error:
...which is #10080 and will be fixed in #10122 and affects all packages (seemingly non-deterministically), not just zarith. |
Here is the error I get when trying to build:
|
You have to build zarith |
Another way to trigger this is to try to build Coq with PM. |
Oh interesting, so it seems like it works when it's built as a dependency in some cases and not others, and it doesn't build when referred to as the target? Any idea why zarith is special in this regard? |
If I make an empty project (with |
@Alizter W.r.t to the |
To help understand this issue I made a small library that installs with bare |
Building Zarith fails with:
This is using
DUNE_PKG_OVERRIDE_OCAML=1
for the lock and build. And the following dune-project:The text was updated successfully, but these errors were encountered: