Stream: Coq users

Topic: coq-stdlib installation problem


view this post on Zulip Térence Clastres (Nov 20 2023 at 14:46):

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 ?

view this post on Zulip Paolo Giarrusso (Nov 20 2023 at 14:49):

Any chance you have custom path configuration for ocaml or coq in some other variable?

view this post on Zulip Térence Clastres (Nov 20 2023 at 14:52):

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

view this post on Zulip Paolo Giarrusso (Nov 20 2023 at 15:03):

if your switch is named default, that's normal. But did you create a new switch and omit eval $(opam env)?

view this post on Zulip Térence Clastres (Nov 20 2023 at 15:09):

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

view this post on Zulip Paolo Giarrusso (Nov 20 2023 at 17:34):

@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.

view this post on Zulip Paolo Giarrusso (Nov 20 2023 at 17:36):

which also seems very strange, maybe the hook is misbehaving? But I think opam's default shell hook wouldn't give this behavior.

view this post on Zulip Térence Clastres (Nov 20 2023 at 18:18):

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

view this post on Zulip Térence Clastres (Nov 20 2023 at 22:13):

@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

view this post on Zulip Paolo Giarrusso (Nov 20 2023 at 22:23):

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.

view this post on Zulip Paolo Giarrusso (Nov 20 2023 at 22:29):

my test just worked, so no idea.

view this post on Zulip Térence Clastres (Nov 20 2023 at 22:53):

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: Jun 18 2024 at 20:02 UTC