Stream: Coq users

Topic: "Read-only file system" on opam install


view this post on Zulip Stefan Haan (Jan 04 2023 at 03:01):

I'm getting a "Read-only file system" error when I try to install coq-mathcomp-ssreflect via opam:

$ opam install coq-mathcomp-ssreflect
The following actions will be performed:
  ∗ install coq-mathcomp-ssreflect 1.15.0

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
⬇ retrieved coq-mathcomp-ssreflect.1.15.0  (https://github.com/math-comp/math-comp/archive/mathcomp-1.15.0.tar.gz)
[ERROR] The installation of coq-mathcomp-ssreflect failed at "make -C mathcomp/ssreflect install".

#=== ERROR while installing coq-mathcomp-ssreflect.1.15.0 =====================#
# context     2.1.4 | linux/x86_64 | ocaml.4.14.0 | https://coq.inria.fr/opam/released#2023-01-03 09:30
# path        ~/.opam/default/.opam-switch/build/coq-mathcomp-ssreflect.1.15.0
# command     ~/.opam/opam-init/hooks/sandbox.sh install make -C mathcomp/ssreflect install
# exit-code   2
# env-file    ~/.opam/log/coq-mathcomp-ssreflect-37245-a03fbe.env
# output-file ~/.opam/log/coq-mathcomp-ssreflect-37245-a03fbe.out
### output ###
# [...]
# install: cannot create directory ‘/home/dev/.local/share/coq/mathcomp’: Read-only file system
# install: cannot create directory ‘/home/dev/.local/share/coq/mathcomp’: Read-only file system
# install: cannot create directory ‘/home/dev/.local/share/coq/mathcomp’: Read-only file system
# install: cannot create directory ‘/home/dev/.local/share/coq/mathcomp’: Read-only file system
# install: cannot create directory ‘/home/dev/.local/share/coq/mathcomp’: Read-only file system
# install: cannot create directory ‘/home/dev/.local/share/coq/mathcomp’: Read-only file system
# install: cannot create directory ‘/home/dev/.local/share/coq/mathcomp’: Read-only file system
# install: cannot create directory ‘/home/dev/.local/share/coq/mathcomp’: Read-only file system
# install: cannot create directory ‘/home/dev/.local/share/coq/mathcomp’: Read-only file system
# make[1]: *** [Makefile.coq:575: install] Error 1
# make: *** [../Makefile.common:119: install] Error 2
# make: Leaving directory '/home/dev/.opam/default/.opam-switch/build/coq-mathcomp-ssreflect.1.15.0/mathcomp/ssreflect'



<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ ∗ install coq-mathcomp-ssreflect 1.15.0
└─
╶─ No changes have been performed

However I can create the directory manually just fine:

$ mkdir /home/dev/.local/share/coq/mathcomp
$ echo $?
0

The env-file and output-file files:

I have been trying to avoid opam for as long as possible, but trying to build all the dependencies required for graph-theory was a task I clearly underestimated.

view this post on Zulip Paolo Giarrusso (Jan 04 2023 at 05:21):

Maybe that directory is outside the opam sandbox, because opam install only writes into ~/.opam normally. Which suggests you have customized the installation path somehow?

view this post on Zulip Paolo Giarrusso (Jan 04 2023 at 05:48):

If you want to keep your custom config, you might need to edit ~/.opam/opam-init/hooks/sandbox.sh. And maybe file a bug report if your configuration is documented as supported...

view this post on Zulip Paolo Giarrusso (Jan 04 2023 at 05:48):

I'm on Mac and have a different script, but for instance my version must explicitly whitelist the opam switch during installations via add_mounts ro "$OPAM_SWITCH_PREFIX/.opam-switch"

view this post on Zulip Paolo Giarrusso (Jan 04 2023 at 05:51):

err, add_mounts rw "$OPAM_SWITCH_PREFIX" is more relevant: https://github.com/ocaml/opam/blob/f93526d411e6f7ef0b4c9d5190ff6d98cf624d28/src/state/shellscripts/bwrap.sh#L113-L122
(Mac uses https://github.com/ocaml/opam/blob/f93526d411e6f7ef0b4c9d5190ff6d98cf624d28/src/state/shellscripts/sandbox_exec.sh#L68-L74 but this code is in sync)

view this post on Zulip Guillaume Melquiond (Jan 04 2023 at 08:03):

You have defined a variable COQLIBINSTALL in your environment, which overrides the default installation path of Opam/Coq. Is that on purpose?

view this post on Zulip Stefan Haan (Jan 04 2023 at 17:28):

Yes, it's on purpose. It's a library lookup path of coq that does not require root to write. COQLIBINSTALL is also respected by the default make install.

view this post on Zulip Stefan Haan (Jan 04 2023 at 18:06):

I have now unset COQLIBINSTALL and indeed opam succeeds in installing the coq-mathcomp-ssreflect depedency. :smile:
However opam install coq-graph-theory then runs into other problems immediately:

#=== ERROR while compiling coq-mathcomp-finmap.1.5.2 ==========================#
# context     2.1.4 | linux/x86_64 | ocaml.4.14.0 | https://coq.inria.fr/opam/released#2023-01-03 09:30
# path        ~/.opam/default/.opam-switch/build/coq-mathcomp-finmap.1.5.2
# command     ~/.opam/opam-init/hooks/sandbox.sh build make -j3
# exit-code   2
# env-file    ~/.opam/log/coq-mathcomp-finmap-7090-f37c05.env
# output-file ~/.opam/log/coq-mathcomp-finmap-7090-f37c05.out
### output ###
# [...]
# ssreflect with prefix mathcomp.
#
# make[2]: *** [Makefile.coq:764: set.vo] Error 1
# make[2]: *** Waiting for unfinished jobs....
# File "./finmap.v", line 5, characters 0-72:
# Error: Cannot find a physical path bound to logical path
# ssreflect with prefix mathcomp.
#
# make[2]: *** [Makefile.coq:764: finmap.vo] Error 1
# make[1]: *** [Makefile.coq:387: all] Error 2
# make[1]: Leaving directory '/home/dev/.opam/default/.opam-switch/build/coq-mathcomp-finmap.1.5.2'
# make: *** [Makefile.common:51: this-build] Error 2

Is the opam build for coq-graph-theory currently broken or is it still just my system? :thinking:

view this post on Zulip Guillaume Melquiond (Jan 04 2023 at 19:22):

Note that it is not even coq-graph-theory, it is one of its transitive dependencies that is failing: coq-mathcomp-finmap. My guess is that is your system again. You can take a look at .opam/default/.opam-switch/install/coq-mathcomp-ssreflect.changes and see which files got installed. In particular, there should be a line "lib/coq/user-contrib/mathcomp/ssreflect/ssreflect.vo".

view this post on Zulip Paolo Giarrusso (Jan 04 2023 at 23:03):

After unsetting COQLIBINSTALL, it's quite likely you'll need more than rerunning opam. In doubt, I'd clear any other non-standard settings, move away the old .opam, and setup opam and coq again

view this post on Zulip Paolo Giarrusso (Jan 04 2023 at 23:05):

I'd also disable/remove any other coq installation.

view this post on Zulip Paolo Giarrusso (Jan 04 2023 at 23:06):

OTOH, installing ocaml via other package managers can work; ocaml is even able to use such a "system" ocaml installation

view this post on Zulip Paolo Giarrusso (Jan 04 2023 at 23:07):

(quicker approaches might be possible, but I can't guess without extra info; kudos to Guillaume's deductions).

view this post on Zulip Stefan Haan (Jan 05 2023 at 01:21):

OK, I could install coq-graph-theory now. :smile:
For reference, here is what I did:


Last updated: Jun 20 2024 at 12:02 UTC