Stream: Coq users

Topic: dune cache breaks Coq 8.14(.1) (on Mac?)


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Dec 03 2021 at 20:14):

what's the problem exactly? does it happen with all dune-using packages?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Dec 03 2021 at 22:05):

Maybe the issue is mac-specific?

view this post on Zulip Paolo Giarrusso (Dec 03 2021 at 22:05):

or even mac-version specific!

view this post on Zulip Rudi Grinberg (Dec 04 2021 at 04:10):

The sandboxing mechanism used by opam is https://github.com/containers/bubblewrap

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Dec 04 2021 at 04:33):

And as Rudi suggested, dune 3.0 caching will probably need something else.

view this post on Zulip Rudi Grinberg (Dec 04 2021 at 05:01):

Yes sorry, bubblewrap is linux only and opam uses sandbox-exec on mac.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Rudi Grinberg (Dec 04 2021 at 07:30):

Coq 8.14 builds with dune right?

view this post on Zulip Rudi Grinberg (Dec 04 2021 at 07:30):

Check if the cache is being populated

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Dec 04 2021 at 09:59):

IIRC configure puts a timestamp somewhere so you won't get cache

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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: Jan 27 2023 at 01:03 UTC