Li-yao (Nov 04 2020 at 17:35): Li-yao (Nov 04 2020 at 17:35):Trying to opam install coq-flocq, the install step somehow fails with
# mkdir: cannot create directory ‘/usr/local/lib64/Core’: Read-only file system
Any clue what I am missing?
Paolo Giarrusso (Nov 04 2020 at 19:54):I don't know why it's trying to write to that folder, but assuming that's correct, and that it has the right privileges, it sounds like you have /usr mounted read-only?
Paolo Giarrusso (Nov 04 2020 at 19:56):I'm skeptical of why it'd try, but maybe opam-depext is installing some native dep?
Li-yao (Nov 04 2020 at 20:04):The "read-only" part is probably some opam shenanigans. What I find puzzling is that it's trying to do anything with /usr/local in the first place, as opposed to writing to my switch in $HOME/.opam/. It's not doing anything special with that directory, that's just the location to install the .vo files, and it's wrong.
Li-yao (Nov 04 2020 at 20:07):I've managed to make the installation "work" manually by adding a -prefix flag to ./configure before compiling, but then I don't get why the opam script does not include that flag.
Paolo Giarrusso (Nov 04 2020 at 20:39):Ah, I had forgot opam's sandboxing!
Paolo Giarrusso (Nov 04 2020 at 20:40):Which version are you installing? Any chance it's a dev version, flocq changed, but the opam script didn't?
Li-yao (Nov 04 2020 at 20:51):3.3.1, also tried 3.3.0
Li-yao (Nov 04 2020 at 20:53):Just the latest officially released stuff, which has been out for months, which is why I'm assuming something in my config is wrong, but no idea what.
Guillaume Melquiond (Nov 05 2020 at 06:41):It seems you have set the libdir environment variable (or exec_prefix) before calling opam. Flocq respects this variable when installing its files. Make sure to unset this variable beforehand.
If you have not set this variable, then it means Flocq is severely confused about where Coq libraries should be installed. Please tell us more about your setup.
Paolo Giarrusso (Nov 05 2020 at 08:36):But is that correct? Opam packages should respect the opam config variables (https://opam.ocaml.org/doc/Manual.html#Switch-variables), which are not environment variables and which are passed explicitly to configure in the opam scripts
Paolo Giarrusso (Nov 05 2020 at 08:38):Using the environment variables also seems a bit surprising anyway... https://www.gnu.org/prep/standards/html_node/Directory-Variables.html recommends using makefile variables by convention, but everything on that page suggests those are not meant to inherit values from environment variables either
Guillaume Melquiond (Nov 05 2020 at 08:40):If a Coq library was respecting the Opam lib configuration variable, then its files would get installed into the OCaml library directory, which is definitely not the place you want to install Coq libraries.
Paolo Giarrusso (Nov 05 2020 at 08:40):E.g. they suggest, to override them, "make prefix=/usr install" (which sets the makefile variable), not "prefix=/usr make install" (which sets the env variable)
Paolo Giarrusso (Nov 05 2020 at 08:43):I'd expect installations in ${lib}/user-contrib/..., but I might be misremembering.
Paolo Giarrusso (Nov 05 2020 at 08:43):But let me ask why does flocq respect libdir? Which convention is that following?
Guillaume Melquiond (Nov 05 2020 at 08:44):You are assuming that it is the makefile that is reading libdir from the environment. That is not what is happening. It is the configure script, which is the documented behavior of autoconf. If environment variables are set at configure time, then they are preserved at build time.
Guillaume Melquiond (Nov 05 2020 at 08:46):Let us be clear, Flocq installs its files into the directory obtained by calling coqc -where (same as coq_makefile). But it does so only if the user did not explicitly set libdir. If the user set it, then Flocq respects it.
Paolo Giarrusso (Nov 05 2020 at 08:57):I was less assuming and more googling. But even with the hint, I've been unable to find documentation for his particular aspect of autoconf.
Paolo Giarrusso (Nov 05 2020 at 08:59):I am also not sure whether "how to pick install locations" should be up to individual packages, even if that were a documented autoconf behavior.
Paolo Giarrusso (Nov 05 2020 at 09:03):looking at https://www.gnu.org/software/autoconf/manual/autoconf-2.69/html_node/Installation-Names.html#Installation-Names and https://www.gnu.org/software/autoconf/manual/autoconf-2.69/html_node/Compilers-and-Options.html#Compilers-and-Options might or might not "document" this behavior, tho I should check what configure --help says (when I'm back in front of a computer).
Karl Palmskog (Nov 05 2020 at 09:07):picking "arbitrary" install locations have always been a possibility with opam, and I don't think that's going to change.
Karl Palmskog (Nov 05 2020 at 09:09):we could impose more strict requirements in the Coq opam archive CI, but this would probably require quite a lot of scripting work
Paolo Giarrusso (Nov 05 2020 at 09:11):Before discussing how to enforce a rule, it'd be good to know if it is a rule, or it should be.
Paolo Giarrusso (Nov 05 2020 at 09:13):That scripting work could be replaced by having opam clear those variables, but that depends on the actual requirements
Paolo Giarrusso (Nov 05 2020 at 09:14):In SwEng terms, we're at the phase where a potential clueless stakeholder (?) proposes a new requirement, and you negotiate it.
Paolo Giarrusso (Nov 05 2020 at 09:16):And my requirement is I didn't know that opam install coq-foo is (conventionally) allowed/encouraged to take arbitrary steps, so that I need to read its documentation. And possibly the documentation of tools used in its opam script?
Karl Palmskog (Nov 05 2020 at 09:33):the opam definition is basically just a thin layer on top of whatever lower-level installation mechanism a piece of software wants to use. Clearing environment variables and the like is to me not the job of opam or the Coq opam archive. If anything, this is an issue that is related to Flocq itself, and how it handles building/installation (and thus the proper place for discussion may be as a Flocq GitLab issue). We could say in the Coq opam archive that we only want packages to accept such-and-such environment variables, but given the difficulty of enforcing this I don't see that we will anytime soon.
Guillaume Melquiond (Nov 05 2020 at 09:34):As far as I am concerned, I have always considered it was the job of Opam to sanitize the environment rather than passing any random variable lying around to the build scripts. But then it would break the use case of several users who want to set COQEXTRAFLAGS before installing a Coq library through Opam.
Guillaume Melquiond (Nov 05 2020 at 09:36):Anyway, I should modify the Flocq packages so that they unset libdir and a few other Autoconf variables before calling configure.
Guillaume Melquiond (Nov 05 2020 at 09:39):By the way, since you were wondering, here is what configure --help says for Flocq:
$ ./configure --help
Configuration of Flocq 3.3.1:
Fine tuning of the installation directory:
--libdir=DIR library [DIR=`$COQC -where`/user-contrib/Flocq]
...
I tend to agree with @Guillaume Melquiond that opam should restrict the environment it passes to build scripts. If people explicitly want to have such side effects, they should be able to explicitly tell opam to pass on certain variables - possibly only to certain packages.
Li-yao (Nov 05 2020 at 13:45):@Guillaume Melquiond Thanks for the response! How can I tell whether libdir is set, or unset it? At the very least opam config list doesn't point anywhere outside my $HOME https://dpaste.org/T3PT
Karl Palmskog (Nov 05 2020 at 13:52):maybe: printenv | grep libdir
or just grepping for the /usr/local in printenv?
Li-yao (Nov 05 2020 at 14:02):Thanks for the tip. Nothing has /usr/local though (other than MANPATH and PATH)
Li-yao (Nov 05 2020 at 14:22):ok so ./configure calls coqc if $libdir == ${exec_prefix}/lib but before that it runs a site script which on my system sets libdir to ${exe_prefix}/lib64.
Guillaume Melquiond (Nov 05 2020 at 14:26):Ouch, I never expected configure to execute some random file that would surreptitiously modify libdir.
Guillaume Melquiond (Nov 05 2020 at 14:27):I will have to modify the way a few libraries are being configured. Unfortunately, there is no workaround I can suggest right now.
Li-yao (Nov 05 2020 at 14:29):I see. Well with your help I at least know enough to fix it on my side! (I'll just let ./configure run the coqc -where unconditionally)
Paolo Giarrusso (Nov 05 2020 at 17:07):ah, I think I found mentions of such site scripts in the autoconf docs?
Paolo Giarrusso (Nov 05 2020 at 17:10):not what I had found earlier, but https://www.gnu.org/software/autoconf/manual/autoconf-2.69/html_node/Site-Defaults.html#Site-Defaults documents $prefix/share/config.site / $prefix/etc/config.site
Michael Soegtrop (Nov 09 2020 at 09:51):I just run into this issue testing Coq platform on a freshly created OpenSuse Leap 15.2. The default is to have this environment definition:
CONFIG_SITE=/usr/share/site/x86_64-unknown-linux-gnu
The referenced script does set libdir unless it is already set.
As a result I would say any plain automake based package is broken in opam on OpenSuse unless the opam file sets the prefix explicitly.
Any idea how this could be fixed? Possibly clear the CONFIG_SITE environment variable? Should I create an issue at opam for this? Other suggestions?
Michael Soegtrop (Nov 09 2020 at 10:15):P.S.: I now unset CONFIG_SITE in the coq platform build script and this fixes the issues for Coquelicot and Flocq on OpenSuse 15.2.
Michael Soegtrop (Nov 09 2020 at 10:39):I created (https://github.com/ocaml/opam/issues/4423) - more to discuss the topic with the opam team than stating that unsetting CONFIG_SITE is the solution.
Last updated: Oct 03 2023 at 02:34 UTC