Hello, I am unable to install coq-stdlib 8.{18,17} on a clean switch with opam 2.1.5. It errors out in the same manner as this issue : https://github.com/ocaml/opam-repository/issues/23635.
However, for me, OCAMLPATH is not set and the workarounds provided for the related https://github.com/ocaml/opam/issues/5505 did not help either. Any idea ?
Any chance you have custom path configuration for ocaml or coq in some other variable?
Paolo Giarrusso said:
Any chance you have custom path configuration for ocaml or coq in some other variable?
Could be, how can I figure this out ?
If I use printenv
and look for something coq/ocaml related I have
OCAML_TOPLEVEL_PATH=/home/terence/.opam/default/lib/toplevel
OPAM_SWITCH_PREFIX=/home/terence/.opam/default
CAML_LD_LIBRARY_PATH=/home/terence/.opam/default/lib/stublibs:/home/terence/.opam/default/lib/ocaml/stublibs:/home/terence/.opam/default/lib/ocaml
if your switch is named default
, that's normal. But did you create a new switch and omit eval $(opam env)
?
No I didn't forget it (I have a hook that does it automatically) but just to be sure, I executed it manually. All I do is :
opam switch create . --repositories=default,coq-released
eval $(opam env)
opam install coq
Here is the error log : error.txt
@Térence Clastres the settings you report are only fine for the default
switch — seeing them after opam switch create .
seems broken. OTOH, maybe the new switch isn't enabled.
which also seems very strange, maybe the hook is misbehaving? But I think opam's default shell hook wouldn't give this behavior.
Sorry I checked after having removed the switch, I'll update it with what I get when the switch is created when I get back to the computee
@Paolo Giarrusso here it is when I create the switch :
OPAM_SWITCH_PREFIX=/home/terence/Documents/Scolarite/Universite/M1/S2/TER/formalisation/_opam
CAML_LD_LIBRARY_PATH=/home/terence/Documents/Scolarite/Universite/M1/S2/TER/formalisation/_opam/lib/stublibs:/usr/lib/ocaml/stublibs:/usr/lib/ocaml
OCAML_TOPLEVEL_PATH=/home/terence/Documents/Scolarite/Universite/M1/S2/TER/formalisation/_opam/lib/toplevel
That looks alright. I wonder if using a local switch might make a difference... I'm testing this myself:
opam switch create . --repositories=default,coq-released
eval $(opam env)
opam install -j10 coq.8.18.0 ocaml-variants.4.14.1+options ocaml-option-flambda
I wonder if the Coq platform scripts (https://github.com/coq/platform) could help, since they have extra sanity checking (and "preliminary" support for Coq 8.18 — which I'm sure is pretty robust).
AFAIK they wouldn't install in a local switch, but IMHO opam sw link
makes local switches unnecessary.
my test just worked, so no idea.
I wonder if the Coq platform scripts (https://github.com/coq/platform) could help, since they have extra sanity checking (and "preliminary" support for Coq 8.18 — which I'm sure is pretty robust).
AFAIK they wouldn't install in a local switch, but IMHO opam sw link makes local switches unnecessary.
They do install in a local switch ; I just tried installing the dev version and it worked! Thanks for the suggestion.
my test just worked, so no idea.
That's annoying, clearly there is a problem with my configuration but what...
Last updated: Oct 13 2024 at 01:02 UTC