Stream: Coq users

Topic: setup

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.".

Emilio Jesús Gallego Arias (Oct 15 2020 at 11:09):

Hi @Jonathan Cubides , platform and Coq version?

Emilio Jesús Gallego Arias (Oct 15 2020 at 11:09):

What command are you issuing?

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

Emilio Jesús Gallego Arias (Oct 15 2020 at 11:11):

And the command failing?

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.

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?

Jonathan Cubides (Oct 15 2020 at 11:22):

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

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

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.

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.

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

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.

Jonathan Cubides (Oct 15 2020 at 12:00):

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

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.

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

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.

Paolo Giarrusso (Oct 15 2020 at 13:10):

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

Paolo Giarrusso (Oct 15 2020 at 13:11):

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

Paolo Giarrusso (Oct 15 2020 at 13:12):

(wonder if that's relevant)

Last updated: Oct 13 2024 at 01:02 UTC