search

coq / vscoq

Visual Studio Code extension for Coq
MIT License
337 stars 69 forks source link

"Cannot find a physical path bound to logical path" for my entire library #635

Closed arnoudvanderleer closed 1 year ago

arnoudvanderleer commented 1 year ago

Hi, I just upgraded the extension, but I cannot get it to import the library I am working on: image I tried teling it where the library is located by adding the following piece of configuration, but to no avail:

    "vscoq.args": [
        "-R", "/the/absolute/path/UniMath/UniMath", "UniMath"
    ]
rtetley commented 1 year ago

Hi, thanks for your feedback ! Currently we don't support dune builds which explains why it initially hangs. However when I your "vscoq.args" to my set up, everything seems to work fine ! Are you sure the error message is the same when you add the vscoq.args ?

arnoudvanderleer commented 1 year ago

Ah, I'm sorry for raising this issue. I now realized that I copied my global settings instead of workspace settings (which were very different). Thank you for creating and maintaining the plugin! It looks awesome.

dimpase commented 7 months ago

I am seeing the a very similar problem, but I seem to be unable to understand how to tweak the settings. Where are these "workspace settings", and how are they being set up?

I have two libraries FOO and BAR, in /home/dima/work/software/coq/, and in the latter directory I have .vscode/settings.json, which has

{
    "vscoq.args": [
        "-R",
        "/home/dima/work/software/coq/foo",
        "FOO",
        "-R",
        "/home/dima/work/software/coq/bar",
        "BAR"
    ]
}

and I am trying to 

From FOO Require Import Baz.

but it gives me

Cannot find a physical path bound to logical path Baz with prefix FOO.

I must say I'm unfamiliar with the toolchain here, and I find it weird that I cannot specify something akin to C compilers' -I directory option to look up FOO and BAR. OTOH

From Coq Require Import Arith List.

works. As well, the (VSCode's) concept of "workspace" is quite fuzzy to me, as well as the difference between user settings and workspace settings. I'm starting vscode as vscode . in /home/dima/work/software/coq/. Shouldn't it load .vscode/settings.json ?

dimpase commented 7 months ago

It turns out one should use "-Q" rather than "-R" (with coq 8.19). Then it all works. It seems that "-R" is outdated.

I figured it out by looking at a Makefile in the project and seeing COQMFFLAGS := -Q . FOO there.