coq-stdlib.8.17.0 is affected by OCAMLPATH

[Alizter]

When you have an OCAMLPATH variable set and you try to install coq-stdlib the build will fail in the following way:

[ERROR] The compilation of coq-stdlib.8.17.0 failed at "make dunestrap COQ_DUNE_EXTRA_OPT=-split".

#=== ERROR while compiling coq-stdlib.8.17.0 ==================================#
# context     2.1.4 | linux/x86_64 | coq-core.8.17.0 | https://opam.ocaml.org#256625cb
# path        ~/.opam/coq-core.8.17.0/.opam-switch/build/coq-stdlib.8.17.0
# command     ~/.opam/opam-init/hooks/sandbox.sh build make dunestrap COQ_DUNE_EXTRA_OPT=-split
# exit-code   2
# env-file    ~/.opam/log/coq-stdlib-672455-587bbe.env
# output-file ~/.opam/log/coq-stdlib-672455-587bbe.out
### output ###
# [...]
# 41 |   (source_tree theories)
# 42 |   (source_tree plugins))
# 43 |  (action
# 44 |   (with-stdout-to %{targets}
# 45 |    (run tools/dune_rule_gen/gen_rules.exe Coq theories %{env:COQ_DUNE_EXTRA_OPT=}))))
# [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_rule
s.ml", line 56, characters 6-89
# Called from Coq_dune__Coq_rules.Context.make in file "tools/dune_rule_gen/coq_rules.ml", line 171
, characters 25-63
# Called from Dune__exe__Gen_rules.main in file "tools/dune_rule_gen/gen_rules.ml", line 72, charac
ters 13-109
# Called from Dune__exe__Gen_rules in file "tools/dune_rule_gen/gen_rules.ml", line 107, characters
 6-13
#
# make: *** [Makefile:124: .dune-stamp] Error 1

This is because Coq generates its own Dune rules for building the stdlib which requires using findlib to detect Coq plugins. If the Coq plugins are not found in OCAMLPATH then you get the error above.

The workaround is to simply unset OCAMLPATH and try installing again.

However, OCAMLPATH should ideally be coming from however the switch is configured and not be affected from the outside.

cc @kit-ty-kate

[FCsacsa]

Hi,

I have the same error with 8.18.0. I wasn't able to fix it. Can you give me a bit more detail on how to fix it?

[Alizter]

@FCsacsa did you unset the OCAMLPATH variable?

[FCsacsa]

I checked my environment and there was no OCAMLPATH set.

[Alizter]

@FCsacsa there is not much I can help with without knowing more information. Try asking on Coq's Zulip.

[proto-h]

I had the similar issue, here is like it was solved for me. During opam init it suggests to add to your shell script something like this (example for Fish shell):

source ~/.opam/opam-init/init.fish > /dev/null 2> /dev/null; or true

Ensure that this line at the end of your shell initialization scripts, otherwise variables can be overwritten accidentally.