Stream: Coq users

Topic: ✔ metacoq install issue: coq-equations not found


view this post on Zulip Notification Bot (Dec 10 2023 at 00:14):

Mario Carneiro has marked this topic as resolved.

view this post on Zulip Ana de Almeida Borges (Dec 11 2023 at 12:41):

@Mario Carneiro according to what you showed us above, Coq hadn't actually been installed in your opam switch (see the list of installed packages given by opam after <><> Processing actions). You probably had a preexisting Coq installation, which might not play nice with whatever you end up installing via opam.

view this post on Zulip Mario Carneiro (Dec 11 2023 at 12:42):

well I nuked my installation before the example

view this post on Zulip Mario Carneiro (Dec 11 2023 at 12:43):

because the only thing worse than debugging a fresh installation is debugging an installation with random stuff from a previous install

view this post on Zulip Ana de Almeida Borges (Dec 11 2023 at 12:47):

You told us you nuked the opam installation, but not necessarily any other Coq installations. For example, if you had at some point done sudo apt install coq, removing opam wouldn't affect that.

view this post on Zulip Mario Carneiro (Dec 11 2023 at 12:48):

Fair. Is that something I should do? (I'm guessing not...)

view this post on Zulip Karl Palmskog (Dec 11 2023 at 12:48):

no, system packages of Coq are a last resort, always

view this post on Zulip Karl Palmskog (Dec 11 2023 at 12:49):

the Snap might work for your use case, though. But if opam Coq is already working well, there is no need to try anything else.

view this post on Zulip Ana de Almeida Borges (Dec 11 2023 at 12:50):

I only meant to point out that trying sudo apt remove coq might be good, specially if you're running into problems. And it should be part of an attempt to nuke any previous Coq installations

view this post on Zulip Karl Palmskog (Dec 11 2023 at 12:52):

right, I think nearly all Coq installation problems we see on the Zulip these days are when people have a host of different Coq installations, and there is no obvious way to tell by single command where and what they are

view this post on Zulip Paolo Giarrusso (Dec 11 2023 at 14:27):

which coqc at least tells you which coqc is used by the current shell. But debugging shell/editor configs is a mess.


Last updated: Jun 23 2024 at 05:02 UTC