Stream: Coq users

Topic: ✔ Can't install Coq due to an undefined reference error


view this post on Zulip Hiroki Tokunaga (Sep 19 2023 at 01:25):

Using Coq Platform I installed Coq without any problems, and on the opam switch that the platform script installed, I installed my project by opam install . without any issues. Thank you @Michael Soegtrop , though I still can't figure out the differences between the default opam switch and the one installed by the script, and what problems the default one has.

view this post on Zulip Hiroki Tokunaga (Sep 19 2023 at 01:48):

Sorry, but reinstalling Zarith by opam uninstall zarith and opam install zarith resolved the error on the default opam switch.

view this post on Zulip Notification Bot (Sep 19 2023 at 01:49):

Hiroki Tokunaga has marked this topic as resolved.

view this post on Zulip Michael Soegtrop (Sep 19 2023 at 05:25):

@Hiroki Tokunaga : possible differences between opam switches are:

view this post on Zulip Michael Soegtrop (Sep 19 2023 at 05:29):

One more note: the contents of the opam dev repo changes daily and there are no guarantees that the results are consistent. This is very unlike the release opam repo. If you have the dev opam repo linked, typically dev packages take precedence. If these build or not can change from one day to the next. So the repo configuration of a switch is very important and one should not pull in the dev repo without a very good reason (like working on Coq 8.18).


Last updated: Jun 13 2024 at 19:02 UTC