search

coq-community / vscoq-legacy

Legacy Visual Studio Code extension for Coq [maintainers=@huynhtrankhanh,@thery,@Blaisorblade]
MIT License
1 stars 0 forks source link

Paths in _CoqProject file are taken relative to the Workspace root, not the path of the _CoqProject file #56

Open MSoegtropIMC opened 2 years ago

MSoegtropIMC commented 2 years ago

I have some workspaces where a Coq project and the corresponding _CoqProject file is in a subfolder under the workspace root. In CoqIDE this works fine, but VSCoq interprets the paths for -Q options relative to the workspace root and not relative to the root of the _CoqProject file.

I think what CoqIDE does is to search upwards from a loaded .v file until it finds a _CoqProject file and takes this as root. It would be nice if VSCoq would be compatible with CoqIDE here.

MSoegtropIMC commented 2 years ago

A workaround is to create a separate workspace, where the Coq folder is the root.

Blaisorblade commented 1 year ago

How do you even get VsCoq to load an out-of-root _CoqProject file? Is this relying on coq-community/vscoq#179, so a bug report in that feature?

MSoegtropIMC commented 1 year ago

Honestly I don't remember, but I guess I must have used coq-community/vscoq#179.