Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
MSoegtropIMC opened this issue Oct 7, 2022 · 3 comments
Assignees

Comments

@MSoegtropIMC
Copy link

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
Copy link
Author

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

@Blaisorblade
Copy link
Collaborator

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

@MSoegtropIMC
Copy link
Author

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

@maximedenes maximedenes self-assigned this Jul 31, 2023
@gares gares transferred this issue from coq/vscoq Oct 10, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants