install Coq through opam fails on Arch Linux if ocaml-findlib package is installed

[e00E]

Following the official instructions on installing Coq through opam does not work on Arch Linux if the ocaml-findlib Arch Linux package is installed. For me, the package was installed because I previously installed the Arch Linux coq package. I decided to install Coq through opam and removed the Arch Linux Coq package, but I did not uninstall ocaml-findlib.

You can easily reproduce this issue with a clean Arch installation through Docker.

docker run --rm -it archlinux
# We're in the container now.
pacman -Sy base-devel ocaml ocaml-findlib opam
opam init
eval $(opam env)
opam pin add coq 8.19.0

The last command errors with the following message.

[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     /usr/sbin/make dunestrap COQ_DUNE_EXTRA_OPT=-split DUNESTRAPOPT=-p coq-stdlib
# exit-code   2
# env-file    ~/.opam/log/coq-stdlib-433-d41818.env
# output-file ~/.opam/log/coq-stdlib-433-d41818.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

Note that if you don't install ocaml-findlib, the installation succeeds.

At this point you can run more investigative commands like ocamlfind list:

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

This issue has been discussed on Zulip.

[MSoegtropIMC]

We should check this before Coq Platform starts setup in the upfront sanity checks - that is before even installing opam.

Can you suggest a piece of shell script to detect this situation say using pacman? I would test if pacman itself exists to see if this is applicable and add similar tests for a few other platforms.

[e00E]

If your goal is to check whether ocaml-findlib is installed, then you can do pacman -Q ocaml-findlibs. If ocaml-findlibs is installed, the command will return status code 0. If it is not installed, it will return status code 1.

However, a more correct check might need to rely directly on ocaml and opam since those are the tools that are confused by ocaml-findlibs already existing. The installation of Coq should succeed, even if ocaml-findlibs is installed. It is a bug that they don't.

We should check this before Coq Platform starts setup in the upfront sanity checks - that is before even installing opam.

Note that in my case, I install opam through the Arch Linux package manager. In this case a like what you propose doesn't make sense. But it might make sense for Coq Platform.

[MSoegtropIMC]

Note that in my case, I install opam through the Arch Linux package manager.

Coq Platform does install opam if it is not installed yet - if it finds a usable (not too old) opam, it will use it (but always create a new switch). But Coq Platform does the sanity checks before it starts installing anything. It is quite annoying if scripts run half through and then find that there is an issue and you have to restart from scratch.

In the end this needs to be fixed in opam, probably by supplying a patched findlib which ignores system installed OCaml and Coq packages. There is already a patched findlib in opam, but its purpose is to supply switch local libraries. But doing upfront sanity checks has proven to be very effective.