Paolo Giarrusso (Dec 03 2021 at 20:08): Paolo Giarrusso (Dec 03 2021 at 20:08):(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?
Paolo Giarrusso (Dec 03 2021 at 20:09):Details on https://github.com/coq/platform/issues/189, but this is not a Coq platform-specific issue.
Gaëtan Gilbert (Dec 03 2021 at 20:14):what's the problem exactly? does it happen with all dune-using packages?
Paolo Giarrusso (Dec 03 2021 at 20:15):... In fact, since the cache and opam can't coexist today, --cache disabled seems the correct fix.
Paolo Giarrusso (Dec 03 2021 at 20:16):@Gaëtan Gilbert _If_ you enable dune caching and opam sandboxes (and everybody should), then the sandbox stops dune from accessing the cache.
Paolo Giarrusso (Dec 03 2021 at 20:17):with errors like Error: connect: : Operation not permitted. I'd _guess_ it's for all packages, but haven't tried; @rgrinberg might know.
Gaëtan Gilbert (Dec 03 2021 at 20:18):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
Paolo Giarrusso (Dec 03 2021 at 22:05):Maybe the issue is mac-specific?
Paolo Giarrusso (Dec 03 2021 at 22:05):or even mac-version specific!
Rudi Grinberg (Dec 04 2021 at 04:10):The sandboxing mechanism used by opam is https://github.com/containers/bubblewrap
Rudi Grinberg (Dec 04 2021 at 04:10):It's implemented in a completely different way on macos and linux so I'm not surprised if that's the case
Paolo Giarrusso (Dec 04 2021 at 04:21):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.
Paolo Giarrusso (Dec 04 2021 at 04:32):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.
Paolo Giarrusso (Dec 04 2021 at 04:33):And as Rudi suggested, dune 3.0 caching will probably need something else.
Rudi Grinberg (Dec 04 2021 at 05:01):Yes sorry, bubblewrap is linux only and opam uses sandbox-exec on mac.
Rudi Grinberg (Dec 04 2021 at 05:04):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
Paolo Giarrusso (Dec 04 2021 at 06:30):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?
Rudi Grinberg (Dec 04 2021 at 07:30):Check if the cache is being populated
Paolo Giarrusso (Dec 04 2021 at 09:18):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.
Paolo Giarrusso (Dec 04 2021 at 09:21):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.
Gaëtan Gilbert (Dec 04 2021 at 09:59):IIRC configure puts a timestamp somewhere so you won't get cache
Paolo Giarrusso (Dec 04 2021 at 11:34):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.
Paolo Giarrusso (Dec 04 2021 at 11:36):Oh, duplicate of https://github.com/coq/coq/issues/15138 / https://github.com/ocaml/dune/issues/4575; @Tej Chajed run into this.
Paolo Giarrusso (Dec 04 2021 at 11:48):I posted a summary of the workarounds I see in https://github.com/coq/coq/issues/15138#issuecomment-986014533.
Paolo Giarrusso (Dec 04 2021 at 11:50):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).
Paolo Giarrusso (Dec 04 2021 at 11:51):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: Apr 20 2024 at 15:01 UTC