Stream: Coq users

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


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

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

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

view this post on Zulip Gaëtan Gilbert (Jan 26 2022 at 15:44):

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

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

view this post on Zulip Paolo Giarrusso (Jan 26 2022 at 15:49):

I've seen Coq include its own flock binary

view this post on Zulip Michael Soegtrop (Jan 26 2022 at 15:50):

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

view this post on Zulip Gaëtan Gilbert (Jan 26 2022 at 15:50):

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

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

view this post on Zulip Paolo Giarrusso (Jan 26 2022 at 15:51):

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

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

view this post on Zulip Michael Soegtrop (Jan 26 2022 at 15:52):

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

view this post on Zulip Gaëtan Gilbert (Jan 26 2022 at 15:53):

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

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

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

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

view this post on Zulip Michael Soegtrop (Jan 26 2022 at 15:58):

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

view this post on Zulip Michael Soegtrop (Jan 26 2022 at 15:59):

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

view this post on Zulip Gaëtan Gilbert (Jan 26 2022 at 16:00):

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

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

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

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

view this post on Zulip Gaëtan Gilbert (Jan 26 2022 at 17:50):

If you run flock foo echo hello what happens?

view this post on Zulip Gaëtan Gilbert (Jan 26 2022 at 17:51):

(foo is an arbitrary file name)

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

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

view this post on Zulip Pierre Courtieu (Jan 26 2022 at 18:04):

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

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

view this post on Zulip Guillaume Melquiond (Jan 26 2022 at 18:12):

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

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

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

view this post on Zulip Gaëtan Gilbert (Jan 26 2022 at 18:13):

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

view this post on Zulip Paolo Giarrusso (Jan 26 2022 at 18:14):

the .opam packages in Coq itself already use dune fully

view this post on Zulip Pierre Courtieu (Jan 26 2022 at 18:14):

$ flock .dune.lock dune --version
2.9.2

view this post on Zulip Gaëtan Gilbert (Jan 26 2022 at 18:14):

what about make VERBOSE=1 after configure?

view this post on Zulip Pierre Courtieu (Jan 26 2022 at 18:14):

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

view this post on Zulip Gaëtan Gilbert (Jan 26 2022 at 18:15):

here is fine until we've got something reproducible IMO

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

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

view this post on Zulip Pierre Courtieu (Jan 26 2022 at 18:21):

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

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

view this post on Zulip Pierre Courtieu (Jan 26 2022 at 18:25):

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

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

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

view this post on Zulip Pierre Courtieu (Jan 26 2022 at 18:27):

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

view this post on Zulip Pierre Courtieu (Jan 26 2022 at 18:28):

ho yes it will with opam install .

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

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

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

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

view this post on Zulip Paolo Giarrusso (Jan 10 2023 at 19:13):

Wait, searching for a binary finds a folder?

view this post on Zulip Paolo Giarrusso (Jan 10 2023 at 19:14):

It seems definitely worth a bug report

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

view this post on Zulip Pierre Courtieu (Jan 10 2023 at 19:35):

Or mayb my config is definitely broken :-)

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

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

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

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

view this post on Zulip Gaëtan Gilbert (Jan 10 2023 at 22:26):

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

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