Stream: Dune devs & users

Topic: Workaround on OS X


view this post on Zulip Matthieu Sozeau (May 04 2021 at 16:15):

Is there a workaround now for those of us on OS X that do not have flock? It seems I cannot build the coq.dev package...

view this post on Zulip Théo Zimmermann (May 04 2021 at 16:16):

Good question. The answer is probably no, unless you pin from the Coq git repo, in which case, it's the fully Dunerized build that you get.

view this post on Zulip Matthieu Sozeau (May 04 2021 at 16:17):

I'd be fine with that

view this post on Zulip Matthieu Sozeau (May 04 2021 at 16:17):

Can't we just update the coq.dev package though?

view this post on Zulip Théo Zimmermann (May 04 2021 at 16:18):

What do you mean?

view this post on Zulip Matthieu Sozeau (May 04 2021 at 16:19):

Well, make the opam coq.dev package use the full dune build to avoid relying on flock

view this post on Zulip Matthieu Sozeau (May 04 2021 at 16:21):

opam pin add coq-core https://github.com/coq/coq.git works fine

view this post on Zulip Emilio Jesús Gallego Arias (May 04 2021 at 16:22):

We can add a workaround for the missing flock , but isn't it quite easy to install from ports brew etc?

view this post on Zulip Gaëtan Gilbert (May 04 2021 at 16:22):

can't we fix the legacy build to work on osx ?

view this post on Zulip Emilio Jesús Gallego Arias (May 04 2021 at 16:22):

@Gaëtan Gilbert it works but you need to do brew install flock

view this post on Zulip Emilio Jesús Gallego Arias (May 04 2021 at 16:23):

I didn't find a locking primitive that is accessible from shell standard in OSX

view this post on Zulip Matthieu Sozeau (May 04 2021 at 16:23):

Nope, that's not flock on my system

view this post on Zulip Théo Zimmermann (May 04 2021 at 16:23):

Apparently, to install flock with brew, you need to install a specific tap first.

view this post on Zulip Théo Zimmermann (May 04 2021 at 16:23):

And with MacPorts, it's not even available.

view this post on Zulip Théo Zimmermann (May 04 2021 at 16:23):

So that's indeed quite a problem.

view this post on Zulip Emilio Jesús Gallego Arias (May 04 2021 at 16:24):

https://github.com/coq/coq/blob/6d08729ab58ce90b3c62df83609b47b6e0da6ebc/.github/workflows/ci.yml#L37

view this post on Zulip Emilio Jesús Gallego Arias (May 04 2021 at 16:24):

I see, ok, let's add a workaround then

view this post on Zulip Matthieu Sozeau (May 04 2021 at 16:24):

Flock is a messaging system on brew by default

view this post on Zulip Théo Zimmermann (May 04 2021 at 16:24):

@Michael Soegtrop has recommended using shlock on OS X because the bugs you see in the man for flock are Linux specific and do not apply to the BSD version.

view this post on Zulip Emilio Jesús Gallego Arias (May 04 2021 at 16:24):

shlock does not work IIUC

view this post on Zulip Emilio Jesús Gallego Arias (May 04 2021 at 16:25):

let me cook the PR

view this post on Zulip Matthieu Sozeau (May 04 2021 at 16:25):

Why do we need these file locks in the first-place? Couldn't we just force -j1 if it's not available?

view this post on Zulip Théo Zimmermann (May 04 2021 at 16:26):

Why do we need these file locks in the first-place? Couldn't we just force -j1 if it's not available?

Good idea.

view this post on Zulip Michael Soegtrop (May 04 2021 at 16:50):

@Emilio Jesús Gallego Arias : as far as I can tell there is no way to install flock via MacPorts and I prefer it over Homebrew.

view this post on Zulip Michael Soegtrop (May 04 2021 at 16:51):

Why do you say shlock does not work? The issues discussed doesn't seem to apply to BSD.

view this post on Zulip Emilio Jesús Gallego Arias (May 04 2021 at 17:56):

@Michael Soegtrop they don't even do the same thing, as far as I can see, how do you implement flock 's blocking mode with shlock?

view this post on Zulip Michael Soegtrop (May 05 2021 at 06:59):

@Emilio Jesús Gallego Arias : can you describe what exactly you are doing with flock - e.g. what command line you use in dune?
For waiting until a lock becomes free with shlock, one would have to resort to busy waiting, which should not that bad (in the sense of better than -j 1 ). If you tell me how you call flock, I can see if I can come up with a shlock based shell script which works on macOS.

view this post on Zulip Emilio Jesús Gallego Arias (May 05 2021 at 12:35):

thanks @Michael Soegtrop , we use flock to guard all calls to dune, flock.dune.lock dune ....

view this post on Zulip Emilio Jesús Gallego Arias (May 05 2021 at 12:35):

so they are serialized

view this post on Zulip Emilio Jesús Gallego Arias (May 05 2021 at 12:36):

All note the PR https://github.com/coq/coq/pull/14249 which is simple enough to work well too IMO.

view this post on Zulip Michael Soegtrop (May 05 2021 at 17:09):

The OCaml + C flock wrapper is in my opinion the best solution.


Last updated: Oct 16 2021 at 09:07 UTC