(cache enabled) in
~/.config/dune/config + opam's sandboxing prevents installing Coq 8.14.1, and this seems a general bug for any opam package using dune. The quickfix would be adding
--cache disabled in the opam packages, or documenting this as a known issue. Preferences?
Details on https://github.com/coq/platform/issues/189, but this is not a Coq platform-specific issue.
what's the problem exactly? does it happen with all dune-using packages?
... In fact, since the cache and opam can't coexist today,
--cache disabled seems the correct fix.
@Gaëtan Gilbert _If_ you enable dune caching and opam sandboxes (and everybody should), then the sandbox stops dune from accessing the cache.
with errors like
Error: connect: : Operation not permitted. I'd _guess_ it's for all packages, but haven't tried; @rgrinberg might know.
but I've used opam with sandbox while cache is enabled
elpi had an issue because they had some hack but now it's fine, and many other packages were always fine
Maybe the issue is mac-specific?
or even mac-version specific!
The sandboxing mechanism used by opam is https://github.com/containers/bubblewrap
It's implemented in a completely different way on macos and linux so I'm not surprised if that's the case
Bubblewrap is Linux-only but the point stands. https://github.com/ocaml/opam/issues/3659 shows past issues with @Guillaume Melquiond 's build system, which confirm it's stricter on Mac.
Looking at bubblewrap and
https://github.com/ocaml/opam/blob/8b31550c1a8596c26aedf714a3add8d31743af9d/src/state/shellscripts/bwrap.sh, connecting to an existing cache daemon might be a problem, but starting one and connecting to isn't: on Linux this should use CLOME_NEWNET, creating a separate loopback interface, Instead, it seems on Mac most network access is just denied.
And as Rudi suggested, dune 3.0 caching will probably need something else.
Yes sorry, bubblewrap is linux only and opam uses sandbox-exec on mac.
Perhaps you should just disable the sandbox for now? It was introduced after that camlp5 rm -rf nightmare IIRC, but if you stick to dune built packages you should be pretty safe
I can't stick to dune-built packages, but I can test that option. Yet somehow,
opam reinstall doesn't benefit from caching (guess because not all of the build is dune-based, but I'm not sure even the dune-based parts show speedups?)
$ time opam reinstall coq.8.14.1 real 2m27.413s user 6m21.114s sys 1m21.380s $ time opam reinstall coq.8.14.1 real 2m26.284s user 6m20.515s sys 1m21.502s
Coq 8.14 builds with dune right?
Check if the cache is being populated
AFAICT, it seems it's an hybrid build, and the main opam package still prefers the old build system where possible. But enough pieces rely on dune that it must work.
I also see that the sandbox already whitelists dune's cache directory; so cache direct access could be a workaround, and dune 3 should just work.
IIRC configure puts a timestamp somewhere so you won't get cache
Right, no caching without
SOURCE_DATE_EPOCH. So should the Coq opam package just disable dune caching? But you'd have to use
DUNEOPT more often for that.
Oh, duplicate of https://github.com/coq/coq/issues/15138 / https://github.com/ocaml/dune/issues/4575; @Tej Chajed run into this.
I posted a summary of the workarounds I see in https://github.com/coq/coq/issues/15138#issuecomment-986014533.
Since I have a solution and multiple workarounds, and since there is at least one documenting issue, I'll stop pursuing this for now, and I guess you could, but I'm happy to help testing if needed — say if you think this has enough impact for further action (as e.g. Emilio felt earlier).
At the very least, installing Coq on Mac doesn't run into problems by default, but only for those who enable dune caching.
Last updated: Oct 04 2023 at 19:01 UTC