Stream: Coq users

Topic: installation of coq on arch linux through opam fails


view this post on Zulip Valentin (May 09 2024 at 12:32):

I am failing to install Coq on Arch Linux. I am following the guide https://coq.inria.fr/opam-using.html . I run the following commands:

pacman -S opam
rm -rf ~/.opam # get rid of left overs from previous attempts
opam init
eval (opam env) # note I'm using fish shell
opam pin add coq 8.19.0

The last step fails with

[ERROR] The compilation of coq-stdlib.8.19.0 failed at "make dunestrap
        COQ_DUNE_EXTRA_OPT=-split DUNESTRAPOPT=-p coq-stdlib".
 installed coqide-server.8.19.0

#=== ERROR while compiling coq-stdlib.8.19.0 ==================================#
# context     2.1.5 | linux/x86_64 | ocaml.5.1.1 | https://opam.ocaml.org#2b6e600e
# path        ~/.opam/default/.opam-switch/build/coq-stdlib.8.19.0
# command     ~/.opam/opam-init/hooks/sandbox.sh build make dunestrap COQ_DUNE_EXTRA_OPT=-split DUNESTRAPOPT=-p coq-stdlib
# exit-code   2
# env-file    ~/.opam/log/coq-stdlib-113513-3c8d13.env
# output-file ~/.opam/log/coq-stdlib-113513-3c8d13.out
### output ###
# [...]
# 43 |  (action
# 44 |   (with-stdout-to %{targets}
# 45 |    (run tools/dune_rule_gen/gen_rules.exe Coq theories %{env:COQ_DUNE_EXTRA_OPT=}))))
# (cd _build/default && tools/dune_rule_gen/gen_rules.exe Coq theories -split) > _build/default/theories_dune
# [gen_rules] Fatal error: Invalid_argument("failed to locate Coq plugins in split build mode: coq-core.plugins.number_string_notation")
# Raised at Coq_dune__Coq_rules.FlagUtil.findlib_plugin_flags in file "tools/dune_rule_gen/coq_rules.ml", line 56, characters 6-89
# Called from Coq_dune__Coq_rules.FlagUtil.plugin_flags in file "tools/dune_rule_gen/coq_rules.ml" (inlined), line 59, characters 18-41
# Called from Coq_dune__Coq_rules.Context.make in file "tools/dune_rule_gen/coq_rules.ml", line 172, characters 25-56
# Called from Dune__exe__Gen_rules.main in file "tools/dune_rule_gen/gen_rules.ml", line 71, characters 13-109
# Called from Dune__exe__Gen_rules in file "tools/dune_rule_gen/gen_rules.ml", line 106, characters 6-13
#
# make: *** [Makefile:132: .dune-stamp] Error 1

This error is inscrutable to me so I don't know what to do.

view this post on Zulip Emilio Jesús Gallego Arias (May 09 2024 at 12:34):

@Valentin the problem is that coq-stdlib cannot find the coq-core plugins package.

What do opam list and ocamlfind list say in your system after the command fails?

view this post on Zulip Valentin (May 09 2024 at 12:35):

opam list
# Packages matching: installed
# Name              # Installed # Synopsis
base-bigarray       base
base-domains        base
base-nnp            base        Naked pointers prohibited in the OCaml heap
base-threads        base
base-unix           base
conf-gmp            4           Virtual package relying on a GMP lib system installation
conf-linux-libc-dev 0           Virtual package relying on the installation of the Linux kernel
coq-core            8.19.0      The Coq Proof Assistant -- Core Binaries and Tools
coqide-server       8.19.0      The Coq Proof Assistant, XML protocol server
dune                3.15.2      Fast, portable, and opinionated build system
ocaml               5.1.1       The OCaml compiler (virtual package)
ocaml-config        3           OCaml Switch Configuration
ocaml-system        5.1.1       The OCaml compiler (system version, from outside of opam)
ocamlfind           1.9.6       A library manager for OCaml
zarith              1.13        Implements arithmetic and logical operations over arbitrary-pre
> ocamlfind list
findlib: [WARNING] Package findlib has multiple definitions in /usr/lib/ocaml/findlib/META, /home/e/.opam/default/lib/findlib/META
findlib: [WARNING] Package bytes has multiple definitions in /usr/lib/ocaml/bytes/META, /home/e/.opam/default/lib/bytes/META
bytes               (version: [distributed with OCaml 4.02 or above])
compiler-libs       (version: 5.1.1)
compiler-libs.bytecomp (version: 5.1.1)
compiler-libs.common (version: 5.1.1)
compiler-libs.native-toplevel (version: 5.1.1)
compiler-libs.optcomp (version: 5.1.1)
compiler-libs.toplevel (version: 5.1.1)
coq-core            (version: n/a)
coq-core.boot       (version: dev)
coq-core.clib       (version: dev)
coq-core.config     (version: dev)
coq-core.coqworkmgrapi (version: dev)
coq-core.engine     (version: dev)
coq-core.gramlib    (version: dev)
coq-core.interp     (version: dev)
coq-core.kernel     (version: dev)
coq-core.lib        (version: dev)
coq-core.library    (version: dev)
coq-core.parsing    (version: dev)
coq-core.perf       (version: dev)
coq-core.plugins    (version: n/a)
coq-core.plugins.btauto (version: dev)
coq-core.plugins.cc (version: dev)
coq-core.plugins.derive (version: dev)
coq-core.plugins.extraction (version: dev)
coq-core.plugins.firstorder (version: dev)
coq-core.plugins.funind (version: dev)
coq-core.plugins.ltac (version: dev)
coq-core.plugins.ltac2 (version: dev)
coq-core.plugins.micromega (version: dev)
coq-core.plugins.nsatz (version: dev)
coq-core.plugins.number_string_notation (version: dev)
coq-core.plugins.ring (version: dev)
coq-core.plugins.rtauto (version: dev)
coq-core.plugins.ssreflect (version: dev)
coq-core.plugins.ssrmatching (version: dev)
coq-core.plugins.tauto (version: dev)
coq-core.plugins.tutorial (version: n/a)
coq-core.plugins.tutorial.p0 (version: dev)
coq-core.plugins.tutorial.p1 (version: dev)
coq-core.plugins.tutorial.p2 (version: dev)
coq-core.plugins.tutorial.p3 (version: dev)
coq-core.plugins.zify (version: dev)
coq-core.pretyping  (version: dev)
coq-core.printing   (version: dev)
coq-core.proofs     (version: dev)
coq-core.stm        (version: dev)
coq-core.sysinit    (version: dev)
coq-core.tactics    (version: dev)
coq-core.top_printers (version: dev)
coq-core.toplevel   (version: dev)
coq-core.vernac     (version: dev)
coq-core.vm         (version: dev)
coqide-server       (version: n/a)
coqide-server.core  (version: dev)
coqide-server.protocol (version: dev)
dune                (version: n/a)
dune.configurator   (version: 3.15.2)
dynlink             (version: 5.1.1)
findlib             (version: 1.9.6)
findlib.dynload     (version: 1.9.6)
findlib.internal    (version: 1.9.6)
findlib.top         (version: 1.9.6)
ocamldoc            (version: 5.1.1)
runtime_events      (version: 5.1.1)
stdlib              (version: 5.1.1)
str                 (version: 5.1.1)
threads             (version: 5.1.1)
threads.posix       (version: [internal])
unix                (version: 5.1.1)
zarith              (version: 1.13)
zarith.top          (version: 1.13)

view this post on Zulip Valentin (May 09 2024 at 12:41):

I should note I had previously done pacman -S coq and Installed the vscoq vscode extension before I found the instructions I'm following now. Maybe this caused some interference. I did uninstall the arch coq package afterwards.

view this post on Zulip Emilio Jesús Gallego Arias (May 09 2024 at 13:56):

Indeed there is something strange, note how coq-core versions are not the same in both listings

view this post on Zulip Emilio Jesús Gallego Arias (May 09 2024 at 13:57):

What does opam repos output?

What does opam show coq-core output?

view this post on Zulip Valentin (May 09 2024 at 13:59):

opam repos --all
# Repository # Url                  # Switches(rank)
default      https://opam.ocaml.org <default> default
opam repos
[NOTE] These are the repositories in use by the current switch. Use
       '--all' to see all configured repositories.

<><> Repository configuration for switch default <><><><><><><><><><><><>
 1 default https://opam.ocaml.org
opam show coq-core

<><> coq-core: information on all versions <><><><><><><><><><><><><><><>
name                   coq-core
all-installed-versions 8.19.0 [default]
all-versions           8.17.0  8.17.1  8.18.0  8.19.0  8.19.1

<><> Version-specific details ><><><><><><><><><><><><><><><><><><><><><>
version      8.19.0
repository   default
url.src      "https://github.com/coq/coq/releases/download/V8.19.0/coq-8.19.0.tar.gz"
url.checksum
          "md5=64b49dbc3205477bd7517642c0b9cbb6"
          "sha512=02fb5b4fb575af79e092492cbec6dc0d15a1d74a07f827f657a72d4e6066532630e5a6d15be4acdb73314bd40b9a321f9ea0584e0ccfe51fd3a56353bd30db9b"
...

view this post on Zulip Michael Soegtrop (May 10 2024 at 07:49):

@Emilio Jesús Gallego Arias : do we test in CI if installing just coq via opam without adding the coq opam repo actually works?

@Valentin : I would say very few people try to install coq via opam without opam repo add coq-released "https://coq.inria.fr/opam/released" - theoretically it should work without it since coq itself is hosted on the main opam repo, but I would guess that this is untested. Since all coq library packages (except the standard library) or hosted on the separate coq opam repo, you will most likely need this anyway. IMHO it is worth a try (and an interesting data point).

view this post on Zulip Michael Soegtrop (May 10 2024 at 07:54):

Btw.: it might work to install Coq using the Coq Platform from sources script. It would be interesting to try it. It might fail for two reasons:
1.) it installs opam via the official opam installs script - not sure if this works on arch linux
2.) some opam conf packages for system supplied prerequisites might not have instructions for arch linux - this should be easy to fix.

If you want, we can work together on this - you tell me what fails and I tell you how to fix it.

view this post on Zulip Karl Palmskog (May 10 2024 at 07:58):

if I'm reading it right, this looks very much like a classic case of where Coq is installed via some Linux system package manager (or manually at system level) and then another opam installation of Coq fails. I don't see any way Platform scripts could avoid this, since system-installed packages (e.g., of Coq-related OCaml libraries) are typically hard to block out

view this post on Zulip Emilio Jesús Gallego Arias (May 10 2024 at 07:59):

@Michael Soegtrop that is tested by OPAM's own CI, AFAICT they do pretty good testing

view this post on Zulip Karl Palmskog (May 10 2024 at 08:00):

(so I think this is unrelated to coq-released repo, I regularly install Coq in opam without adding this repo)

view this post on Zulip Michael Soegtrop (May 10 2024 at 08:02):

@Karl Palmskog : Valentin did run eval $(opam env) - which should puts opam installed tools first in the path. An issue would be exported COQ or OCAML environment variables.

view this post on Zulip Karl Palmskog (May 10 2024 at 08:04):

right, I think it's known that eval $(opam env) is not necessarily enough, depending on the Linux system package manager

view this post on Zulip Michael Soegtrop (May 10 2024 at 08:04):

I think opam env sets all OCaml critical variables. Maybe we should see if we can set Coq relevant variables this way as well.

view this post on Zulip Michael Soegtrop (May 10 2024 at 08:08):

I just checked that Coq Platform build scripts don't set COQLIB either - I think I should check for this and warn. But various scripts Coq Platform produces set it, e.g. the "Coq shell" scripts and the smoke test scripts. Are there other variables I should take care of?

view this post on Zulip Michael Soegtrop (May 10 2024 at 08:09):

@Karl Palmskog : I don't think this is a question of the system package manager. IMHO the only thing which can go wrong after eval $(opam env) is a bad definition of COQLIB - and possibly other COQ related variables.

view this post on Zulip Karl Palmskog (May 10 2024 at 08:10):

but as seen above, findlib and opam report different libraries

view this post on Zulip Karl Palmskog (May 10 2024 at 08:12):

findlib: [WARNING] Package findlib has multiple definitions in /usr/lib/ocaml/findlib/META, /home/e/.opam/default/lib/findlib/META
findlib: [WARNING] Package bytes has multiple definitions in /usr/lib/ocaml/bytes/META, /home/e/.opam/default/lib/bytes/META

So clearly there are competing OCaml libraries in /usr/lib/ocaml/ and /home/e/.opam/default/lib/. I don't know how these competitions are resolved.

view this post on Zulip Michael Soegtrop (May 10 2024 at 08:12):

yes, OK. In Coq Platform I have a patched findlib which works reliably.

view this post on Zulip Karl Palmskog (May 10 2024 at 08:14):

OK, if a user has a patched findlib that should rule out this particular scenario

view this post on Zulip Michael Soegtrop (May 10 2024 at 08:14):

But reagrding the OCaml library: opam env does set an environment variable which tells OCaml exactly where to look.

view this post on Zulip Michael Soegtrop (May 10 2024 at 08:20):

I need to review this - it has been a while. But thinking about it I believe the patched findlib is in opam. What is Coq Platform specific is a patch to ocamlfind which helps to find things after a reloaction - one does not need this patch in non installer scenarios.

view this post on Zulip Michael Soegtrop (May 10 2024 at 08:25):

Afair the change in opam findlib was that opam has its own findlib repo for things which are not installed system wide but e.g. compiled from sources. Opam supplies its own switch specific findlib binary to handle this. But I am not sure if this is used for the OCaml library itself.

view this post on Zulip Karl Palmskog (May 10 2024 at 08:30):

I think the problem seemingly occurs when the opam-delivered findlib starts to look into places where the system-delivered findlib has placed its data. One probably has to delve into findlib's source to figure out where findlib searches and how to blacklist certain directories

view this post on Zulip Valentin (May 10 2024 at 08:31):

Thank you for pointing out /usr/lib/ocaml/findlib/. The arch linux coq package depends on the arch linux ocaml-findlib package. When I uninstalled coq, I did not uninstall findlib. I have now uninstalled ocaml-findlib and installing coq through opam has worked. This problem is easy to reproduce. If you'd like I can open issue about it.

view this post on Zulip Valentin (May 10 2024 at 08:33):

Michael Soegtrop said:

Valentin : I would say very few people try to install coq via opam without opam repo add coq-released "https://coq.inria.fr/opam/released"

This is confusing to me because the instructions I am following on the Coq website don't mention this.

view this post on Zulip Karl Palmskog (May 10 2024 at 08:34):

it's further down on the page, after Coq itself is installed

view this post on Zulip Valentin (May 10 2024 at 08:34):

You're right. I didn't get to that part yet because installation failed.

view this post on Zulip Karl Palmskog (May 10 2024 at 08:35):

@Valentin since users are seemingly hitting this problem again and again in Linux, and the best place to deal with it is likely the Coq Platform, maybe you can write an issue here with the error message and your fix: https://github.com/coq/platform/issues

view this post on Zulip Karl Palmskog (May 10 2024 at 08:36):

I don't use Arch, but I suspect it could be reproducible on Arch even using Platform scripts

view this post on Zulip Valentin (May 10 2024 at 08:38):

If you're on a different Linux flavor, you can easily reproduce this with the Arch Linux Docker image. I'm going to create an issue with the details. Although someone might say it's the wrong place since I was not using the platform script? Anyway, creating the issue.

view this post on Zulip Michael Soegtrop (May 10 2024 at 08:38):

@Valentin : what I would do in Coq Platform about this is adding sanity checks and warn the user if these fail - I already have quite a few of those. So please add whatever information is important to write such a sanity check.

view this post on Zulip Michael Soegtrop (May 10 2024 at 08:39):

@Valentin : the Coq Platform script should work always and if people fail to install Coq in other ways we frequently recommend to try Coq Platform. It is fairly battle proven in a lot of lectures, but one can always improve on it.

view this post on Zulip Karl Palmskog (May 10 2024 at 08:40):

the reason for the Platform issue (in my view) is that we are focusing our installation documentation and streamlining efforts in the Platform, and from there we can update other documentation, such as on the Coq website. This is not really something that the tool Coq itself can solve - it just assumes some findlib is available

view this post on Zulip Valentin (May 10 2024 at 08:53):

https://github.com/coq/platform/issues/415


Last updated: Jun 13 2024 at 19:02 UTC