Stream: Coq users

Topic: opam install coq fails with "flock: permission denied"

Pierre Courtieu (Jan 26 2022 at 14:47):

Hi, I have a permission problem with flock when trying to install or update to coq-8.15 or 8.14.1 (did no try other versions).
Any clue?

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[ERROR] The compilation of coq failed at "/home/courtieu/.opam/opam-init/hooks/sandbox.sh build make COQ_USE_DUNE= -j15".

#=== ERROR while compiling coq.8.14.1 =========================================#
# context     2.0.10 | linux/x86_64 | ocaml-base-compiler.4.12.0 | https://opam.ocaml.org#10a48cb9
# path        ~/.opam/full-coq/.opam-switch/build/coq.8.14.1
# command     ~/.opam/opam-init/hooks/sandbox.sh build make COQ_USE_DUNE= -j15
# exit-code   2
# env-file    ~/.opam/log/coq-800031-06fa5f.env
# output-file ~/.opam/log/coq-800031-06fa5f.out
### output ###
# [...]
# make --warn-undefined-variable --no-builtin-rules -f Makefile.build
# make[1]: Entering directory '/home/courtieu/.opam/full-coq/.opam-switch/build/coq.8.14.1'
# MKDIR     BUILD_OUT
# DUNE      _build/install/default/bin/coqdep
# make[1]: flock: Permission denied

Paolo Giarrusso (Jan 26 2022 at 15:40):

More info about your system would be useful... What is your host operating system? Which filesystems are you using? Does disabling opam sandboxing make a difference? Do you have any configuration in ~/.config/dune/config?

Paolo Giarrusso (Jan 26 2022 at 15:42):

AFAIK, you're testing the combination of (1) dune (which is used in parts of the Coq build, even with COQ_USE_DUNE=) (2) opam sandboxing (3) the flock helper for file locking (but I don't know why Coq's build system builds and uses that program)

Gaëtan Gilbert (Jan 26 2022 at 15:44):

dune can't be run in parallel so we serialize calls with flock

Michael Soegtrop (Jan 26 2022 at 15:48):

Wasn't this replaced with something else, because flock is not available on Mac? I thought dune (or whoever calls flock) now uses an OCaml bases solution (flock is available as C function on macOS).

Possibly updating dune or opam helps.

Paolo Giarrusso (Jan 26 2022 at 15:49):

I've seen Coq include its own flock binary

Michael Soegtrop (Jan 26 2022 at 15:50):

Search for "flock" in the Coq devs zulip stream.

Gaëtan Gilbert (Jan 26 2022 at 15:50):

we compile our own flock only if there isn't one in PATH

Michael Soegtrop (Jan 26 2022 at 15:51):

I don't have flock - and I have macOS and Coq Platform in path and building Coq 8.14.1 and 8.15.0 works (via opam).

Paolo Giarrusso (Jan 26 2022 at 15:51):

@Pierre Courtieu what does shell command -v flock say?

Michael Soegtrop (Jan 26 2022 at 15:52):

Ah no:

coq-platform-main$ find ~/.opam -name flock
/Users/msoegtrop/.opam/__coq-platform.2022.01.0~dev/.opam-switch/sources/coq.dev/tools/flock
/Users/msoegtrop/.opam/__coq-platform.2022.01.0~dev/.opam-switch/sources/coqide.dev/tools/flock
/Users/msoegtrop/.opam/__coq-platform.2022.01.0~8.15~beta1/.opam-switch/sources/coqide.8.15.0/tools/flock
/Users/msoegtrop/.opam/__coq-platform.2022.01.0~8.15~beta1/.opam-switch/sources/coq.8.15.0/tools/flock

So 8.14 doesn't have one. But it still builds for me by some magic.

Michael Soegtrop (Jan 26 2022 at 15:52):

Well and still I don't have binaries ...

Gaëtan Gilbert (Jan 26 2022 at 15:53):

it's called coq_flock.exe and isn't installed, just used for building

Michael Soegtrop (Jan 26 2022 at 15:54):

@Pierre Courtieu : as I said, I don't have a flock binary in path - still building works for me.

Gaëtan Gilbert (Jan 26 2022 at 15:54):

I don't think flock: permission denied is a coq_flock error, it seems like a normal flock binary

Michael Soegtrop (Jan 26 2022 at 15:57):

to me "flock: permission denied" more looks like there is a file flock which bash tries to execute but it is not executable.

Michael Soegtrop (Jan 26 2022 at 15:58):

test$ echo bla > flock
test$ ./flock
-bash: ./flock: Permission denied

Michael Soegtrop (Jan 26 2022 at 15:59):

P.S.: zsh gives a permission denied with lower case p - bash with upper case P.

Gaëtan Gilbert (Jan 26 2022 at 16:00):

but that has the ./ prefix
PATH lookups only try executables so that wouldn't happen

Michael Soegtrop (Jan 26 2022 at 16:01):

@Pierre Courtieu : possibly you have some relics lying around from trying to work around this a few months back ...

Pierre Courtieu (Jan 26 2022 at 17:28):

Thanks for the answers. I will try from a clean config. FTR I am under debian and I don't think I did anything with opam config. I ll let you know. Thanks again.

Pierre Courtieu (Jan 26 2022 at 17:43):

Nothing changed. I just erased the .opam directory. Then reinstalled from scratch:

opam init
eval $(opam env)
echo $PATH
==> /home/courtieu/.opam/default/bin:home/courtieu/.sdkman/candidates/gradle/current/bin:.:/usr/local/jdk1.8.0_171/bin:/usr/local/netbeans-8.2/bin:/home/courtieu/coq/actual/bin:/home/courtieu/coq/actual/tools:/home/courtieu/src/why3-inst/bin:/home/courtieu/.bin:/home/courtieu/config/scripts:/home/courtieu/.local/bin:/home/courtieu/bin:/usr/local/bin:/usr/bin:/bin:/usr/local/games:/usr/games:/snap/bin:/sbin:/usr/sbin::/home/courtieu/.local/bin)
opam install coq
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
∗ installed conf-findutils.1
∗ installed conf-gmp.4
∗ installed ocamlfind.1.9.3
∗ installed zarith.1.12
∗ installed dune.2.9.2
[ERROR] The compilation of coq failed at "/home/courtieu/.opam/opam-init/hooks/sandbox.sh build make COQ_USE_DUNE= -j15".

#=== ERROR while compiling coq.8.15.0 =========================================#
# context     2.0.10 | linux/x86_64 | ocaml-base-compiler.4.13.1 | https://opam.ocaml.org#b3f8647a
# path        ~/.opam/default/.opam-switch/build/coq.8.15.0
# command     ~/.opam/opam-init/hooks/sandbox.sh build make COQ_USE_DUNE= -j15
# exit-code   2
# env-file    ~/.opam/log/coq-871287-abfa5b.env
# output-file ~/.opam/log/coq-871287-abfa5b.out
### output ###
# [...]
# make --warn-undefined-variable --no-builtin-rules -f Makefile.build
# make[1]: Entering directory '/home/courtieu/.opam/default/.opam-switch/build/coq.8.15.0'
# MKDIR     BUILD_OUT
# DUNE      _build/install/default/bin/coqdep
# make[1]: flock: Permission denied
# DUNE      sources

Interestingly when I clone coq master and try "configure -profile devel ; make" it fails the same way. When I do dune build it does not fail.

Gaëtan Gilbert (Jan 26 2022 at 17:50):

If you run flock foo echo hello what happens?

Gaëtan Gilbert (Jan 26 2022 at 17:51):

(foo is an arbitrary file name)

Paolo Giarrusso (Jan 26 2022 at 18:01):

if that works, please also test ~/.opam/opam-init/hooks/sandbox.sh build flock foo echo hello to see if the sandbox makes a difference

Pierre Courtieu (Jan 26 2022 at 18:03):

Gaëtan Gilbert said:

If you run flock foo echo hello what happens?

gives

hello

and

~/.opam/opam-init/hooks/sandbox.sh build flock foo echo hello

prints nothing.

Pierre Courtieu (Jan 26 2022 at 18:04):

but again when I do make in coq sources I get the same error.

Pierre Courtieu (Jan 26 2022 at 18:11):

In coq sources, make -f Makefile.dune world succeeds,
but (on fresh sources) $ ./configure -profile devel followed by make fails with the same flock error. I don't think this ha something to do with sandbox.sh but with the legacy makefile build.
Which build system does opam use for coq?

Guillaume Melquiond (Jan 26 2022 at 18:12):

From the top directory of the Coq sources, you can try flock .dune.lock echo foo.

Pierre Courtieu (Jan 26 2022 at 18:13):

Guillaume Melquiond said:

From the top directory of the Coq sources, you can try flock .dune.lock echo foo.

Hi, it shows foo.

Paolo Giarrusso (Jan 26 2022 at 18:13):

@Pierre Courtieu COQ_USE_DUNE= means opam's package uses dune only where unavoidable (IIRC, for the OCaml code).

Gaëtan Gilbert (Jan 26 2022 at 18:13):

what about flock .dune.lock dune --version?

Paolo Giarrusso (Jan 26 2022 at 18:14):

the .opam packages in Coq itself already use dune fully

Pierre Courtieu (Jan 26 2022 at 18:14):

$ flock .dune.lock dune --version
2.9.2

Gaëtan Gilbert (Jan 26 2022 at 18:14):

what about make VERBOSE=1 after configure?

Pierre Courtieu (Jan 26 2022 at 18:14):

Maybe we should switch to another channel? Sould I fill a bug?

Gaëtan Gilbert (Jan 26 2022 at 18:15):

here is fine until we've got something reproducible IMO

Pierre Courtieu (Jan 26 2022 at 18:16):

$ ./configure -profile devel
You have OCaml 4.13.1. Good!
You have OCamlfind 1.9.3. Good!
You have native-code compilation. Good!
You have the Zarith library 1.12 installed. Good!
...
$ make VERBOSE=1
make --warn-undefined-variable --no-builtin-rules -f Makefile.build
make[1]: Entering directory '/home/courtieu/coq/master'
flock .dune.lock dune build --display=quiet --profile=dev _build/install/default/bin/coqdep
make[1]: flock: Permission denied
flock .dune.lock dune build --display=quiet --profile=dev _build/install/default/bin/coqc
make[1]: flock: Permission denied
make[1]: *** [Makefile.common:131: _build/install/default/bin/coqc] Error 127
make[1]: Leaving directory '/home/courtieu/coq/master'
make: *** [Makefile.make:122: submake] Error 2

Pierre Courtieu (Jan 26 2022 at 18:19):

doing by hand flock .dune.lock dune build --display=quiet --profile=dev _build/install/default/bin/coqdep does not fail.

Pierre Courtieu (Jan 26 2022 at 18:21):

really strange. I am currently stuck out of opam :-(

Paolo Giarrusso (Jan 26 2022 at 18:23):

Since this problem is specific to flock, using opam install ./coq-core.opam should build Coq bypassing this problem

Pierre Courtieu (Jan 26 2022 at 18:25):

ha. That we unstuck me. What does it do exactly?

Paolo Giarrusso (Jan 26 2022 at 18:25):

or even opam install . to install all the packages, apparently (I'm not sure that's the perfect way of doing this).

Paolo Giarrusso (Jan 26 2022 at 18:25):

well you said that pure dune builds (make -f Makefile.dune world) succeed, and those opam packages use the pure dune builds

Pierre Courtieu (Jan 26 2022 at 18:27):

OK. But then installing coq packages depending on coq won't work.

Pierre Courtieu (Jan 26 2022 at 18:28):

ho yes it will with opam install .

Paolo Giarrusso (Jan 26 2022 at 18:29):

there's also a coq.opam package; they claim to have version dev, but even that can be changed

Paolo Giarrusso (Jan 26 2022 at 18:29):

(at least by editing the version field; I forget the syntax for doing it on the cmd line)

Pierre Courtieu (Jan 26 2022 at 18:31):

OK this seems to work a bit. I still don't understand the initial problem. I will investigate a bit more.

Pierre Courtieu (Jan 10 2023 at 19:11):

FTR one year later, I understood this flock problem...

If I have in my PATH a directory containing <sources of coq>/tools, then it messes with opam compilation because then flock is actually seen as the directory <sources of coq>/tools/flock instead of a binary.

This is perfectly expectable but was hard to pinpoint from the error (flock permission denied), because which flock gives the path of the correct executable (citing its doc: "The command works by locating the executable file matching the given command")...

Don't know if this is worth a bug report for opam, or coq: I guess flock executable should be detected consistently with the system.

Paolo Giarrusso (Jan 10 2023 at 19:13):

Wait, searching for a binary finds a folder?

Paolo Giarrusso (Jan 10 2023 at 19:14):

It seems definitely worth a bug report

Paolo Giarrusso (Jan 10 2023 at 19:16):

I'd have expected executable search to be implemented once and for all in OCaml, making this an OCaml bug? If not, why not?

Pierre Courtieu (Jan 10 2023 at 19:35):

Or mayb my config is definitely broken :-)

Guillaume Melquiond (Jan 10 2023 at 20:12):

Paolo Giarrusso said:

Wait, searching for a binary finds a folder?

As dumb as it might seem, this behavior complies with the posix standard. You can try it for yourself with a command like:

$ dash -c 'PATH=/usr bin'
dash: 1: bin: Permission denied

(More evolved shells such as Bash exclude directories from their search for directory entries with the executable bit set, which is a much saner behavior.)

Pierre Courtieu (Jan 10 2023 at 21:36):

I still don’t know if this is a bug and (if yes) of what it would be a bug :-). opam, dune, coq, bash?

Paolo Giarrusso (Jan 10 2023 at 22:14):

:man_facepalming: oh I have a guess, sorry. Can you run ls -l /bin/sh, confirm that it points to dash (maybe indirectly?), then reproduce @Guillaume Melquiond 's example? My advice then is to make /bib/sh point to bash or the like

Paolo Giarrusso (Jan 10 2023 at 22:16):

The error was thrown when make executed flock. Make's spec demands that, by default, make runs commands via /bin/sh. Debian decided to make that point to dash. And dash... Dunno, made what seems here the unfortunate choice to follow the standard instead of do something smarter?

Gaëtan Gilbert (Jan 10 2023 at 22:26):

are we sure it's a choice and not just a bug?

Paolo Giarrusso (Jan 11 2023 at 03:50):

I'd consider just reporting a bug to dash: https://pubs.opengroup.org/onlinepubs/9699919799/functions/exec.html on execvp seems
terribly vague here, but Debian's dash seems to not use execvp anyway https://salsa.debian.org/debian/dash/-/blob/debian/unstable/src/exec.c.

Last updated: Oct 13 2024 at 01:02 UTC