Matthieu Sozeau (May 04 2021 at 16:15): 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...
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.
Matthieu Sozeau (May 04 2021 at 16:17):I'd be fine with that
Matthieu Sozeau (May 04 2021 at 16:17):Can't we just update the coq.dev package though?
Théo Zimmermann (May 04 2021 at 16:18):What do you mean?
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
Matthieu Sozeau (May 04 2021 at 16:21):opam pin add coq-core https://github.com/coq/coq.git works fine
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?
Gaëtan Gilbert (May 04 2021 at 16:22):can't we fix the legacy build to work on osx ?
Emilio Jesús Gallego Arias (May 04 2021 at 16:22):@Gaëtan Gilbert it works but you need to do brew install flock
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
Matthieu Sozeau (May 04 2021 at 16:23):Nope, that's not flock on my system
Théo Zimmermann (May 04 2021 at 16:23):Apparently, to install flock with brew, you need to install a specific tap first.
Théo Zimmermann (May 04 2021 at 16:23):And with MacPorts, it's not even available.
Théo Zimmermann (May 04 2021 at 16:23):So that's indeed quite a problem.
Emilio Jesús Gallego Arias (May 04 2021 at 16:24): Emilio Jesús Gallego Arias (May 04 2021 at 16:24):I see, ok, let's add a workaround then
Matthieu Sozeau (May 04 2021 at 16:24):Flock is a messaging system on brew by default
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.
Emilio Jesús Gallego Arias (May 04 2021 at 16:24):shlock does not work IIUC
Emilio Jesús Gallego Arias (May 04 2021 at 16:25):let me cook the PR
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?
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.
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.
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.
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?
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.
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 ....
Emilio Jesús Gallego Arias (May 05 2021 at 12:35):so they are serialized
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.
Michael Soegtrop (May 05 2021 at 17:09):The OCaml + C flock wrapper is in my opinion the best solution.
Last updated: Oct 13 2024 at 01:02 UTC