"Read-only file system" on opam install · Coq users

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

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

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.

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?

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...

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"

Paolo Giarrusso (Jan 04 2023 at 05:51):

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?

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.

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:

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".

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

Paolo Giarrusso (Jan 04 2023 at 23:05):

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

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).

Stefan Haan (Jan 05 2023 at 01:21):

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