_CoqProject is only searched in first workspace folder - it should be searched in the workspace folder the current file is in

[MSoegtropIMC]

VSCoq seems to look for a _CoqProject file only in the root folder of the first workspace folder. It does not look into subfolders of the first workspace folder nor does it look into other workspace folders.

IMHO the searching of the _CoqProject file should start with the file opened and search in the containing folders and upwards. This is what CoqIDE seems to do (since it doesn't have a concept of workspaces CoqIDE doesn't have much of another option anyway).

In general it would be preferable if all editors search/interpret _CoqProject files in the same way. See also my other 2 issues on the topic: coq-community/vscoq-legacy#49 and coq-community/vscoq-legacy#56

[Blaisorblade]

True, that'd be consistent with CoqIDE and Proof General. OTOH, that behavior is a problem with project composition — for other editors, we end up having to rename away most _CoqProject files except the outermost "composed" _CoqProject. Long-term, dune coq top is a better idea for composition, but we're far from there.

As a workaround, at least #179 lets you override the location by hand, which is more flexible.

[MSoegtropIMC]

My main problem is that I sometimes have several projects loaded which are not intended to be composed. The typical case is a complete rework of a project, where I load the original and reworked variant. I then want to step through some proof in the old and new variant in parallel. I need 2 VSCode instances for this - which is not nice, but OK.

[Blaisorblade]

Oh that would require an extra change: dealing with multiple _CoqProjects. Not rocket science, but the code seems to use a singleton.

[MSoegtropIMC]

I think the main question is where what we want to be eventually:

• VSCode centric workspace based setup with VSCode configuration files (like the launch.json files one has in VSCode C)
• A system which picks up _CoqProject or dune created configuration files in a way compatible with other editors
• Make the choice between the two configurable

I think eventually we will need both. The casual user is probably more happy with an "auto pick up" solution a la CoqIDE. The expert user probably prefers a works space oriented setup with json configuration files. If we go for JSON config files, I think we should follow common VSCode practice and allow multiple such files in multiple folders.

[MSoegtropIMC]

See also #683