Stream: Coq users

Topic: CoqIDE 8.18.0 can't open after install from opam


view this post on Zulip Sheldon Huang (Feb 09 2024 at 14:07):

I encounter this issue after successfully running thisopam install coqide.8.18.0

image.png

image.png
'coqidetop.opt' -q -nois -batch

image.png
cannot guess a path for Coq libraries; please use -coqlib option or ensure you have installed the package containing Coq's stdlib (coq-stdlib in OPAM) If you intend to use Coq without a standard library, the -boot -noinit options must be used.

view this post on Zulip Yann Leray (Feb 09 2024 at 14:11):

As it says, you most probably want to have coq-stdlib installed so the automatically imported Coq.Init.Prelude module is found. The other possibility is to use Coq without a standard library using the given flags -boot -noinit.

view this post on Zulip Sheldon Huang (Feb 09 2024 at 14:30):

Yann Leray said:

As it says, you most probably want to have coq-stdlib installed so the automatically imported Coq.Init.Prelude module is found. The other possibility is to use Coq without a standard library using the given flags -boot -noinit.

Thank you Yann so much, your suggestion very helpful !

view this post on Zulip Sheldon Huang (Feb 09 2024 at 14:31):

coq opam verision manage should be very very very very careful, make sure the dependency lib must be very consistent
for example: 8.18.0, must lib and others all need to be same !

view this post on Zulip Yann Leray (Feb 09 2024 at 14:53):

This constraint is present in the relevant opam files, so it should be respected by opam. Did you have any issues with incompatible packages using opam ?

view this post on Zulip Sheldon Huang (Feb 09 2024 at 15:05):

Yann Leray said:

This constraint is present in the relevant opam files, so it should be respected by opam. Did you have any issues with incompatible packages using opam ?

yes, I did, for example I did opam install coqide.8.18.0 to force the environment to keep consistent.

btw, when to use opam switch what context do we use?

view this post on Zulip Li-yao (Feb 09 2024 at 15:11):

you would typically use opam switch if you have multiple projects with different version of coq

view this post on Zulip Yann Leray (Feb 09 2024 at 15:12):

I'm not sure I understand what issue you faced. If everything works correctly, as soon as you install one version of coq-core in your switch, there is only one version of coq-stdlib and coqide than can be installed. So simply doing opam install coqide should find that unique version and shouldn't be able to install another one.

I don't understand your second question either. A switch is a development environment, it contains your installation of Coq and all other packages and libraries for OCaml and Coq. If you use a single version of Coq (and no incompatible packages), you should have a single switch, and thus never have to call opam switch to change between them

view this post on Zulip Sheldon Huang (Feb 09 2024 at 15:32):

Thank you Li-yao and Yann, it's quite clear for me already !

My issue has solved it was how to solve the inconsistency in different version, not I learn verison controls, it works for me now

and yes @Yann Leray thank you , I have success after install proper version of coq-stdlib :+1:


Last updated: Jun 13 2024 at 19:02 UTC