Stream: Coq users

Topic: Trouble installing Coq with opam


view this post on Zulip Dominik Stolz (voidc) (Nov 27 2023 at 13:02):

Hi, installing Coq with opam pin add coq 8.17.1 results in an error failed to locate Coq plugins in split build mode: coq-core.plugins.number_string_notation. I found a previous topic where the problem seemed to be an externally set OCAMLPATH variable. However, in my case, there is no such variable. I tried installing both versions 8.17.1 and 8.18.0 but got the same error.

Full Error:

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

#=== ERROR while compiling coq-stdlib.8.17.1 ==================================#
# context     2.1.5 | linux/x86_64 | ocaml-system.5.0.0 | https://opam.ocaml.org#b176d244
# path        ~/.opam/default/.opam-switch/build/coq-stdlib.8.17.1
# command     ~/.opam/opam-init/hooks/sandbox.sh build make dunestrap COQ_DUNE_EXTRA_OPT=-split
# exit-code   2
# env-file    ~/.opam/log/coq-stdlib-337922-1aa8e6.env
# output-file ~/.opam/log/coq-stdlib-337922-1aa8e6.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_rules.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, characters 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

Env vars:

CAML_LD_LIBRARY_PATH=/home/dominik/.opam/default/lib/stublibs:/usr/lib/ocaml/stublibs:/usr/lib/ocaml
OCAML_TOPLEVEL_PATH=/home/dominik/.opam/default/lib/toplevel
OPAMCLI=2.0
OPAMROOT=/home/dominik/.opam
OPAMSWITCH=default
OPAM_PACKAGE_NAME=coq-stdlib
OPAM_PACKAGE_VERSION=8.17.1
OPAM_SWITCH_PREFIX=/home/dominik/.opam/default

Any clues?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 27 2023 at 15:51):

Hi @Dominik Stolz (voidc) , it seems that your coq-core package is not properly installed, or at the wrong version. What does ocamlfind list and opam list display in your system?

view this post on Zulip Dominik Stolz (voidc) (Nov 27 2023 at 15:56):

opam list shows coq-core 8.17.1 but ocamlfind list shows version: n/a

ocamlfind list

view this post on Zulip Paolo Giarrusso (Nov 27 2023 at 20:25):

I've already seen this issue here, I think from another user?

view this post on Zulip Karl Palmskog (Nov 27 2023 at 21:53):

hmm, was it the case with the system-installed ocamlfind?

view this post on Zulip Paolo Giarrusso (Nov 28 2023 at 00:56):

https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/coq-stdlib.20installation.20problem


Last updated: Jun 13 2024 at 19:02 UTC