Opam using: warn users that you need to install CoqIDE with opam if you want it to know about Coq packages.

[Zimmi48]

A very frequent error users do is that they start installing Coq + CoqIDE with their preferred package manager, then they install opam and coq packages through opam. These packages depend on Coq but not on CoqIDE, so when they launch CoqIDE, it will be the system-wide installation that they use.

Depending how CoqIDE locates coqtop / coqidetop, several scenarios can then happen:

• CoqIDE locates the system-wide coqtop / coqidetop. In this case, everything works fine but the installed packages are not available (even if they might be when compiling through the console).
• CoqIDE locates the opam installed coqtop / coqidetop. In this case, if the versions match, it will work fine and the installed packages will be available. If the versions do not match, it will fail at launch.

The opam-using page should warn users about this caveat and recommend installing CoqIDE with opam and removing any previous installation. Additionally, the advanced section of the opam-using page could mention the possibility to keep using the system install of CoqIDE provided that the user make sure that they pin the right version of Coq when installing through opam.

This problem would also be resolved, in a much nicer way for the user, if the opam installation procedure could detect that the dependency on coq is already satisfied by a system-wide installation (see also discussion in coq/opam-coq-archive#595 but this is also a much more complex solution to implement, that could require changes to opam itself).

[gares]

I understand this problem, but I also think of scenarios is simply unfixable so I would not add complexity to the software in order to detect ... what exactly?

The scenario makes sense, it is just about having multiple versions of Coq installed and starting the wrong one. How can Coq possibly know this is not what the user wanted?

About making the doc more clear, why not, but I'm afraid it won't be effective either (nobody reads it, users just copy/paste snippets in their terminals).

[Zimmi48]

About making the doc more clear, why not, but I'm afraid it won't be effective either (nobody reads it, users just copy/paste snippets in their terminals).

Well at least you can then tell to people to go read the doc again.

I didn't get what exactly you asked in your first two paragraphs, but here is the basic idea: opam is able to use a system-wide installed OCaml if you tell it so; it would be great if it had the same ability for Coq. Even better: when you try to install a Coq package with opam but Coq has not been set up before, it would fail with an error message telling you either to pin Coq to the version of your choosing, or to explicitly tell it to use the system-wide install (if it exists). Note that this really is just wishful thinking.

[gares]

To me the system switch was a very, very, very bad idea in the first place.

Would you you make nix use stuff not installed via nix but just happening to be in the path?

[Zimmi48]

People like to criticize the system switch because it makes things messy / less pure, but you need to have casual users in mind to see the benefits. Opam with no system switch forces you to rebuild OCaml (and then Coq). CoqIDE has dependencies that opam cannot track and lots of users have no idea how to get them. Nix has none of these problems: it has a binary cache, it has all the dependencies of CoqIDE, and thus it is trivial, and quick, to install Coq and CoqIDE.

[gares]

Sure, but it is also the casual user that may get into trouble when dependencies/assumptions are broken, and the system switch can cause that. Frankly the casual user does not care about 3 extra minutes of compile time, since any problem in the setup process will take way more than that to be solved. I'm against suggesting them to install coq with opam and using the system switch.

And sure, having a binary cache is a plus, but either you have it, or you don't: the system switch is not a cache since you (package manager) are not the one filling it in, so its contents are random. You have to live with that for gtk, since opam cannot built it, but you can surely avoid it for ocaml.

[ejgallego]

Indeed please avoid the system switch, using it is a 100% guarantee your system will become broken at some point. Compiling modern OCaml is pretty quick now that the multicore build is enabled.

[Blaisorblade]

Thanks for creating an issue on this. I've wondered multiple times if I was doing something wrong.