Jovial Cheukam (Nov 25 2020 at 19:25): 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 ?
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)
Fabian Kunze (Nov 25 2020 at 19:32):Did you run make in the folder where the makefile is?
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 .
Fabian Kunze (Nov 25 2020 at 19:46):you can probably just run make.
Did make basics.vo indicate that everything went well?
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?
Jovial Cheukam (Nov 25 2020 at 19:48):Yes ! And all thoses file are in the same folder.
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.
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
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...
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
<> /
Fabian Kunze (Nov 25 2020 at 19:54):Hm, as I expected it does not see that the library LF is in that folder
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 ;) )
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"
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.
Fabian Kunze (Nov 25 2020 at 20:06):how did you install coq on macos?
Jovial Cheukam (Nov 25 2020 at 20:07):with Homebrew: brew install coq
Fabian Kunze (Nov 25 2020 at 20:08):on the new version of macos? (I heard that some update released a few weeks ago)
Jovial Cheukam (Nov 25 2020 at 20:09):No, I didn't update the mac.
Fabian Kunze (Nov 25 2020 at 20:12):hm, maybe as a workaround, can you start coqide in the folder?
Fabian Kunze (Nov 25 2020 at 20:14):Maybe @Michael Soegtrop or @Théo Winterhalter know more about macos, but I don't.
Jovial Cheukam (Nov 25 2020 at 20:16):coqide is not in the folder "lf".
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.
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
Fabian Kunze (Nov 25 2020 at 20:19):and that probably takes 30 minutes to compile coq
Paolo Giarrusso (Nov 25 2020 at 20:54):I wouldn't expect sandboxing tho?
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...
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/...
Paolo Giarrusso (Nov 25 2020 at 20:58):@Fabian Kunze is File -> open Folder... an actual thing? Not here..
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)
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
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.
Jovial Cheukam (Nov 26 2020 at 00:46):Thanks. I added /Users to the path and it's working well now.
Théo Zimmermann (Nov 26 2020 at 11:04):What about running code . from the console?
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: Apr 19 2024 at 04:02 UTC