You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
When you have an OCAMLPATH variable set and you try to install
coq-stdlib
the build will fail in the following way: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
The text was updated successfully, but these errors were encountered: