Stream: Coq users

Topic: Error in Coq File


view this post on Zulip Jovial Cheukam (Nov 25 2020 at 19:25):

Hello, I got that error on Coq:"Cannot find a physical path bound to logical path matching suffix <> and prefix LF."
I follow all the instructions to make .vo file and create it, but the error still remain. This is on the file "Induction.v" on the line number 9 :"From LF Require Export Basics." of software fundation" for learning Coq. Please do you have an idea to fix this ?

view this post on Zulip Fabian Kunze (Nov 25 2020 at 19:30):

What editor/IDE are you using? And what Operating system? (Most likely the folder where Induction.v is located as well)

view this post on Zulip Fabian Kunze (Nov 25 2020 at 19:32):

Did you run make in the folder where the makefile is?

view this post on Zulip Jovial Cheukam (Nov 25 2020 at 19:45):

Thank for replying. I use MacOs and the editor is Vscode. And I ran make Basics.vo in directory of makefile .

view this post on Zulip Fabian Kunze (Nov 25 2020 at 19:46):

you can probably just run make.
Did make basics.vo indicate that everything went well?

view this post on Zulip Fabian Kunze (Nov 25 2020 at 19:47):

and you are opening the file Induction.v in the same folder where Basics.vo and _CoqProject are, do you?

view this post on Zulip Jovial Cheukam (Nov 25 2020 at 19:48):

Yes ! And all thoses file are in the same folder.

view this post on Zulip Fabian Kunze (Nov 25 2020 at 19:49):

does "Print LoadPath.", inserted and executed into the coq-file at the beginning, list something about LF.? It probably lists a lot of things about Coq.

view this post on Zulip Fabian Kunze (Nov 25 2020 at 19:51):

and is vscoq opened in the folder as well? You can just run code . from the terminal to open vscode in the right folder

view this post on Zulip Fabian Kunze (Nov 25 2020 at 19:52):

coq only sees the .vo file if _CoqProject is at the workspace root of vscode, which you can do by File -> open Folder...

view this post on Zulip Jovial Cheukam (Nov 25 2020 at 19:52):

This is what it shows:
Coq.Numbers.Cyclic
/usr/local/Cellar/coq/8.12.1/lib/coq/theories/Numbers/Cyclic
Coq.Numbers /usr/local/Cellar/coq/8.12.1/lib/coq/theories/Numbers
Coq.setoid_ring /usr/local/Cellar/coq/8.12.1/lib/coq/theories/setoid_ring
Coq.Compat /usr/local/Cellar/coq/8.12.1/lib/coq/theories/Compat
Coq.Strings /usr/local/Cellar/coq/8.12.1/lib/coq/theories/Strings
Coq.ssrsearch /usr/local/Cellar/coq/8.12.1/lib/coq/theories/ssrsearch
Coq.ssrmatching /usr/local/Cellar/coq/8.12.1/lib/coq/theories/ssrmatching
Coq.Init /usr/local/Cellar/coq/8.12.1/lib/coq/theories/Init
Coq.FSets /usr/local/Cellar/coq/8.12.1/lib/coq/theories/FSets
<> /

view this post on Zulip Fabian Kunze (Nov 25 2020 at 19:54):

Hm, as I expected it does not see that the library LF is in that folder

view this post on Zulip Fabian Kunze (Nov 25 2020 at 19:57):

Well, if opening vscode with that folder as workspace does not work, there is a "hacky" solution:
Add LoadPath "/path/to/lf" as LF.
Add this to the beginning of the coq file and at least it will work. (of course you need to adjust the path ;) )

view this post on Zulip Jovial Cheukam (Nov 25 2020 at 20:03):

I get now with "Add LoadPath" that error : "Cannot open /jovial/Documents/COQ-dossiers/lf [cannot-open-path,filesystem]coqtop"

view this post on Zulip Fabian Kunze (Nov 25 2020 at 20:05):

Oh, that seems somewhat macOs-specific, maybe the app does not have enough access rights because of sandboxing. Sorry, I can't help here.

view this post on Zulip Fabian Kunze (Nov 25 2020 at 20:06):

how did you install coq on macos?

view this post on Zulip Jovial Cheukam (Nov 25 2020 at 20:07):

with Homebrew: brew install coq

view this post on Zulip Fabian Kunze (Nov 25 2020 at 20:08):

on the new version of macos? (I heard that some update released a few weeks ago)

view this post on Zulip Jovial Cheukam (Nov 25 2020 at 20:09):

No, I didn't update the mac.

view this post on Zulip Fabian Kunze (Nov 25 2020 at 20:12):

hm, maybe as a workaround, can you start coqide in the folder?

view this post on Zulip Fabian Kunze (Nov 25 2020 at 20:14):

Maybe @Michael Soegtrop or @Théo Winterhalter know more about macos, but I don't.

view this post on Zulip Jovial Cheukam (Nov 25 2020 at 20:16):

coqide is not in the folder "lf".

view this post on Zulip Fabian Kunze (Nov 25 2020 at 20:17):

yes, that is toally ok. I thought that maybe homebrew installs the other ide, coqide as well, and that you could just start it from command line, but this was a wild guess.

view this post on Zulip Fabian Kunze (Nov 25 2020 at 20:18):

You could try installing with opam, the ocaml-packet-manager, but I'm not sure that helps: https://coq.inria.fr/opam-using.html

view this post on Zulip Fabian Kunze (Nov 25 2020 at 20:19):

and that probably takes 30 minutes to compile coq

view this post on Zulip Paolo Giarrusso (Nov 25 2020 at 20:54):

I wouldn't expect sandboxing tho?

view this post on Zulip Paolo Giarrusso (Nov 25 2020 at 20:56):

@Jovial Cheukam what is the exact LoadPath line you gave?I'd be surprised if the path /jovial/Documents/COQ-dossiers/lf were correct...

view this post on Zulip Paolo Giarrusso (Nov 25 2020 at 20:58):

I expect you need to add /Users at the beginning of the path, e.g. /Users/jovial/...

view this post on Zulip Paolo Giarrusso (Nov 25 2020 at 20:58):

@Fabian Kunze is File -> open Folder... an actual thing? Not here..

view this post on Zulip Paolo Giarrusso (Nov 25 2020 at 20:59):

What I have to do in VSCode is "File -> New Windows", then "File -> Open", and finally select the right folder (aka the one containing _CoqProject as Fabian said)

view this post on Zulip Fabian Kunze (Nov 25 2020 at 21:03):

Paolo Giarrusso said:

Fabian Kunze is File -> open Folder... an actual thing? Not here..

Under my linux-system, I have the option Open Folder in my file menu in vscoq

view this post on Zulip Théo Winterhalter (Nov 25 2020 at 21:36):

Yeah we don't have it on macOS, but you can just use open and select a folder and it works I think.

view this post on Zulip Jovial Cheukam (Nov 26 2020 at 00:46):

Thanks. I added /Users to the path and it's working well now.

view this post on Zulip Théo Zimmermann (Nov 26 2020 at 11:04):

What about running code . from the console?

view this post on Zulip Théo Zimmermann (Nov 26 2020 at 11:05):

It would be best to find a solution that doesn't require Add LoadPath because this is really hackish.


Last updated: Feb 08 2023 at 23:03 UTC