Stream: Coq users

Topic: problem with sudo make install

view this post on Zulip Ralph Matthes (Apr 28 2022 at 08:43):

On Ubuntu 22.04, with Ocaml 4.13.0 installed through OPAM, I tried the "legacy build" of Coq 8.15.1 from sources, with installation into the default system directories. make world went fine, but sudo make install fails very early, simply because dune - installed through OPAM in my user space - cannot be found when doing sudo: sudo env | grep PATH shows the path where sudo is looking for binaries, and local OPAM installations are invisible. Is there a safe and generic way to include the path to dune for this make invocation ? For the time being, I extended the setting for the variable secure_path by the binary directory of the currently used OPAM switch, through the dedicated editorvisudo. Unless I missed something, it would be good to have a warning in the installation instructions, in particular for point 5 of the detailed installation procedure.

view this post on Zulip Paolo Giarrusso (Apr 28 2022 at 08:50):

I’m not sure sudo make install is a good idea on Coq… How badly do you really need to install Coq in system directories?

view this post on Zulip Paolo Giarrusso (Apr 28 2022 at 08:50):

Among other problems, it seems Coq libraries would have to be installed as root as well.

view this post on Zulip Paolo Giarrusso (Apr 28 2022 at 08:52):

And I don’t know if they should all be trusted, given https://opam.ocaml.org/blog/camlp5-system/… that kind of thing got fixed by opam sandboxing instead.

view this post on Zulip Guillaume Melquiond (Apr 28 2022 at 08:52):

Ralph Matthes said:

Is there a safe and generic way to include the path to dune for this make invocation ?

Since you are willing to run sudo dune anyway, you could just install dune in the first place. This might be the simplest solution.

view this post on Zulip Ralph Matthes (Apr 28 2022 at 08:56):

Okay, I do not really need Coq in system directories. And I understand from your reactions that I better not do an installation there already for security reasons. But then, the default values proposed through the configure script are somewhat misleading.

view this post on Zulip Ralph Matthes (Apr 28 2022 at 08:59):

Paolo Giarrusso said:

And I don’t know if they should all be trusted, given https://opam.ocaml.org/blog/camlp5-system/… that kind of thing got fixed by opam sandboxing instead.

There seems to be a problem with that link.

view this post on Zulip Paolo Giarrusso (Apr 28 2022 at 10:16):

Sorry: https://opam.ocaml.org/blog/camlp5-system/

view this post on Zulip Paolo Giarrusso (Apr 28 2022 at 10:18):

Just to be sure, that happened once 4 years ago. But I don’t think install scripts are meant to run as root directly.

view this post on Zulip Paolo Giarrusso (Apr 28 2022 at 10:23):

I’m just a user, but if others agree adjusting docs might indeed be a good idea

view this post on Zulip Ralph Matthes (Apr 28 2022 at 13:18):

Paolo Giarrusso said:

Sorry: https://opam.ocaml.org/blog/camlp5-system/

Thank you, that is strong ancedotal evidence of risks related to installations with sudo.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2022 at 13:29):

Thanks for the feedback @Ralph Matthes ; indeed we need to improve documentation. As of today, some parts of it assume that the preferred install method is old-school "/usr/local" with sudo, and some assume user-local opam or nix switches, etc...

view this post on Zulip Emilio Jesús Gallego Arias (Apr 28 2022 at 13:29):

So indeed it is a bit confusing, I wonder what we should take as the default?

view this post on Zulip Paolo Giarrusso (Apr 28 2022 at 14:00):

The unprivileged version is what opam uses so it's the most tested; and many opam users would install into their opam switch... Not sure what Nix provides.

view this post on Zulip Théo Zimmermann (Apr 29 2022 at 08:09):

Ralph Matthes said:

Okay, I do not really need Coq in system directories. And I understand from your reactions that I better not do an installation there already for security reasons. But then, the default values proposed through the configure script are somewhat misleading.

These default values are mostly meant for uses in packaging scripts in fact. It is expected that users will install Coq through a package manager rather than manually (especially if they are already using opam to get the dependencies).

view this post on Zulip Ralph Matthes (Apr 29 2022 at 11:48):

Do I have control over which Ocaml version (and flags) was used for compilation when working with a packaged version of Coq? I do not see this in the output of coqc --version and coqc --config.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2022 at 12:10):

@Ralph Matthes it depends on the packaging system you are using. If it is one that distributes binary packages, you don't have control.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2022 at 12:10):

I guess we should reshape the install section of the manual by use cases

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2022 at 12:11):

or target audicences: packagers, users willing to do a global install, users willing to do a local install, or multiple local installs

view this post on Zulip Ralph Matthes (Apr 29 2022 at 18:01):

Maybe the word control was not chosen well. Can I at least know what I have? If I install Ocaml and Coq with the same package manager and I do ocamlc -config, I'll see the flags for Ocaml and would then hope that the very same ocamlc has been used to compile the Coq binaries. But this is not for sure. Or is there a way to know as the user of coqc?

view this post on Zulip Gaëtan Gilbert (Apr 29 2022 at 18:04):

$ coqc --version
The Coq Proof Assistant, version $COQ_VERSION
compiled on $SOME_DATE with OCaml $OCAML_VERSION

view this post on Zulip Ralph Matthes (Apr 29 2022 at 21:04):

I am sorry, but I hoped for the compilation flags of Ocaml, in particular flambda.

view this post on Zulip Paolo Giarrusso (Apr 29 2022 at 21:14):

since you installed ocaml through opam, have you considered opam install coq.8.15.1 in the appropriate switch? The flags in a switch can be inferred from opam list…

view this post on Zulip Paolo Giarrusso (Apr 29 2022 at 21:15):

For instance:

$ opam list|egrep 'ocaml( |-variants|-option)'
ocaml                4.14.0                    The OCaml compiler (virtual package)
ocaml-option-flambda 1                         Set OCaml to be compiled with flambda activated
ocaml-variants       4.14.0+options            Official release of OCaml 4.14.0

view this post on Zulip Paolo Giarrusso (Apr 29 2022 at 22:36):

Other use cases might require/warrant patches, but it's not obvious if there are different requirements, or if the instructions were overall misleading.

view this post on Zulip Ralph Matthes (Apr 30 2022 at 07:37):

@Paolo Giarrusso My use case is working with UniMath. I have all interest in shorter compilation times. It seems that option flambda gives a two-digit gain in percent. To be sure to have this option enabled, I compile Coq myself, on the basis of a local OPAM installation of Ocaml. The installation instructions suggest to make a system-wide installation with sudo - which fails as I mentioned before for a local Ocaml installation (with local Dune). I agree now that a local OPAM installation should be used to make a local Coq installation, and I do this. But all of my self-compilation efforts are only for the purpose of ensuring the flambda option of ocamlc when compiling Coq. I would be happy to install Coq binaries if I could detect myself that a given coqtop had been compiled with such an ocamlc. And I see no documented way to achieve this "control".

view this post on Zulip Paolo Giarrusso (Apr 30 2022 at 07:49):

that’s a good use case I also use flambda for the same reason; I have been installing it with opam for the past few years.

view this post on Zulip Paolo Giarrusso (Apr 30 2022 at 07:58):

thankfully, the instructions on the website seem less misleading; https://coq.inria.fr/download recommends the Coq platform which enables flambda automatically AFAICT (that might be hard to confirm, I was browsing the sources); https://coq.inria.fr/opam-using.html suggest using opam — it does not suggest flambda, but you can choose the appropriate compiler.

view this post on Zulip Paolo Giarrusso (Apr 30 2022 at 08:03):

clearly the instructions in the source code led you astray, but at least https://github.com/coq/coq#installation does link to the website.

view this post on Zulip Ana de Almeida Borges (Apr 30 2022 at 21:10):

If you use opam and create a switch based on whichever OCaml version you prefer (eg using flambda) and then install Coq in that switch, doesn't the resulting Coq installation use precisely that OCaml version?

view this post on Zulip Paolo Giarrusso (Apr 30 2022 at 22:13):

Yep. And since (IIRC) Coq 8.15, it'll even enable flambda automatically.

view this post on Zulip Paolo Giarrusso (Apr 30 2022 at 22:13):

The main opportunity for error is in selecting the right opam switch if you're not careful (say, forget to eval $(opam env)).

view this post on Zulip Paolo Giarrusso (Apr 30 2022 at 22:14):

But if you look at the instructions trying to find out how to get flambda, the instructions aren't very explicit.

view this post on Zulip Karl Palmskog (May 01 2022 at 11:06):

my view: Coq core devs should explicitly recommend an OCaml compiler+options for each major version release ("dev choice"). The closest we get to this currently is the choice of compiler+options in the Coq Platform, but this choice is not documented explicitly (just says that some compiler-related packages that set options are part of the Platform)

Last updated: Oct 05 2023 at 02:01 UTC