Stream: Coq users

Topic: setup


view this post on Zulip Jonathan Cubides (Oct 15 2020 at 11:05):

Hi guys, I just installed Coq. How can I install the standard library?, I'm getting this error message 'Unable to locate library Arith.".

view this post on Zulip Emilio Jesús Gallego Arias (Oct 15 2020 at 11:09):

Hi @Jonathan Cubides , platform and Coq version?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 15 2020 at 11:09):

What command are you issuing?

view this post on Zulip Jonathan Cubides (Oct 15 2020 at 11:10):

On OSX v10.15.1
$ coqc --version
The Coq Proof Assistant, version 8.10.1 (November 2019)
compiled on Nov 14 2019 21:47:34 with OCaml 4.08.1
$ opam --version
2.0.7

view this post on Zulip Emilio Jesús Gallego Arias (Oct 15 2020 at 11:11):

And the command failing?

view this post on Zulip Jonathan Cubides (Oct 15 2020 at 11:13):

Well, I'm using VSCode + VSCoq 0.3.2. Then I got "Unable to locate library Arith." when checking one file from a Coq project I want to read.

view this post on Zulip Gaëtan Gilbert (Oct 15 2020 at 11:19):

if you just installed coq with opam shouldn't it say "compiled $today" instead of some 2019 date?

view this post on Zulip Jonathan Cubides (Oct 15 2020 at 11:22):

That's actually right, I'm might have two installations now, let me check.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 15 2020 at 11:33):

You may want to ask in the vscoq devs & users stream, but we still need to see what the concrete line of Coq code you are trying to run

view this post on Zulip Jonathan Cubides (Oct 15 2020 at 11:45):

Thanks @Gaëtan Gilbert for make me aware of my older Coq installation. I didn't notice that. So, as I said, I installed Coq but I did that using $ brew install coq. But it was not visible because brew put my binaries in a place that it was not exposed by my env variable $PATH. OSX decided in the last version Catalina to change the default shell from bash to zsh. My bad was I never updated my stuff. Anyway, I give here my solution that worked for me, maybe someone else can get benefit.

view this post on Zulip Jonathan Cubides (Oct 15 2020 at 11:50):

Fix ".zshrc" by adding at the end "export PATH=/usr/local/bin:$PATH".
Make sure in VSCode you set "terminal.integrated.shell.osx": "/bin/zsh" in your configuration file.
Then, you should be able to see:

$ coqc --version
The Coq Proof Assistant, version 8.12.0 (July 2020)
compiled on Jul 26 2020 6:47:02 with OCaml 4.09.0

If you did $ brew install coq, the standard library should work out of the box.

view this post on Zulip Jonathan Cubides (Oct 15 2020 at 11:54):

The code I was trying to check was:

Global Set Asymmetric Patterns.

Require Import Arith.
Require Import EqNat.

from https://github.com/coq-contribs/euler-formula

view this post on Zulip Karl Palmskog (Oct 15 2020 at 11:57):

beware that the euler-formula project does not work with Coq 8.12, last version known to work is 8.10.

view this post on Zulip Jonathan Cubides (Oct 15 2020 at 12:00):

@Karl Palmskog , yes, I'm seeing the file Euler3.v raises an error message.

view this post on Zulip Jonathan Cubides (Oct 15 2020 at 12:01):

What do these files *.vo, *.vok, *.glob stand for? I got these files after run coqc $filename.v.

view this post on Zulip Karl Palmskog (Oct 15 2020 at 12:09):

see here for .vos: https://coq.inria.fr/refman/practical-tools/coq-commands.html#compiled-interfaces

.vo are serialized complete proofs/terms, .glob is metadata used by, e.g., coqdoc

view this post on Zulip Paolo Giarrusso (Oct 15 2020 at 13:08):

FWIW, it's unlikely VsCode will see your changes to the PATH, ditto for any graphical app. Luckily, you can go to its settings and give the path to coqc.

view this post on Zulip Paolo Giarrusso (Oct 15 2020 at 13:10):

But none of that explains why Arith is not found...

view this post on Zulip Paolo Giarrusso (Oct 15 2020 at 13:11):

OTOH, that code does not have a _CoqProject file...

view this post on Zulip Paolo Giarrusso (Oct 15 2020 at 13:12):

(wonder if that's relevant)


Last updated: Mar 29 2024 at 12:02 UTC