Parsing no longer seems to use vos files

[tchajed]

I believe this used to work so it's a recent regression.

If you clone https://github.com/tchajed/sys-verif-fa24-proofs, run git submodule update --init --recursive and make vos, then open in VS Code (you can ignore the dev container prompt) and try opening src/sys_verif/program_proof/demos/hashmap_proof.v it gives a bunch of parsing errors. Stepping through the file at this point is also very broken.

Sorry I don't have a more minimal example. However, this whole repo is also a good stress test of VsCoq.

[gares]

The only change that comes to mind is that now vscoq loads the _CoqProject closer to source files, while before id only loaded the same _CoqProject at the root of the repo. Do you happen to have multiple (and possibly broken) _CoqProject files?

[tchajed]

Yes, we have _CoqProject files for dependencies that are in submodules. They aren't broken but are insufficient. Only the top-level file should be used, in the root of the repository, and it has all the configuration needed for the dependencies.

[rtetley]

In fact I checked earlier and it is the root file _CoqProject that seems to be loaded. I'll check tomorrow to see if the arguments are correct.

[gares]

@rtetley only Coq master has support for loading different _CoqProject, I guess @tchajed is using that right?

[gares]

Only the top-level file should be used

This is not what CoqIDE does.
Is PG loading the root one only?

Also, are you building with dune? (If so, support for that would solve your issue since we would ask dune the "right" flags)

[tchajed]

I am not using Coq master, 8.20 is working.
Proof General works and has always worked with this setup.
I'm not using dune or even coq_makefile, it's a custom setup only using coqdep + make (very similar to Perennial).

[SkySkimmer]

@rtetley only Coq master has support for loading different _CoqProject, I guess @tchajed is using that right?

No, IIRC only the vscoq server version matters for this (but on older Coq more settings may be carried over from the root project file)

[SkySkimmer]

However I don't think this is an issue about opening the wrong coqproject as https://github.com/tchajed/sys-verif-fa24-proofs/tree/main/src/sys_verif/program_proof/demos does not seem to have any _CoqProject files between it and the root.

[gares]

No, IIRC only the vscoq server version matters for this (but on older Coq more settings may be carried over from the root project file)

No, it is the second time I got his by this:

vscoq/language-server/vscoqtop/lspManager.ml

Lines 259 to 269 in 8333f37

	[%%if coq = "8.18" || coq = "8.19" || coq = "8.20"]
	(* in these coq versions init_runtime called globally for the process includes init_document
	this means in these versions we do not support local _CoqProject except for the effect on injections
	(eg -noinit) *)
	let init_document _ vst = vst
	[%%else]
	let init_document local_args vst =
	let () = Vernacstate.unfreeze_full_state vst in
	let () = Coqinit.init_document local_args in
	Vernacstate.freeze_full_state ()
	[%%endif]

But anyway, as you noticed, there is no other _CoqProject so it is loading the root one, so my diagnoses is wrong.

[SkySkimmer]

Ah only the injections are taken from the local coqproject in older coq

[SkySkimmer]

It seems vscoq just doesn't set Flags.load_vos_libraries
I don't think this is a recent change but coqidetop does set it so vscoq legacy used it

[gares]

Thanks gaetan, this is likely to be the culprit.

[rtetley]

So after working on #1020, I noticed that setting the flag works, but only if you open the root folder in vscode (the one containing the _CoqProject). If you open the file from a folder that is higher in the file hierarchy, the _CoqProject still seems to load (form the logs) but we go back to the errors mentioned above (namely Cannot find a physical path bound to logical path, which leads to all the parse errors). Is this expected ?

[rtetley]

Since this is a one line fix (disregarding the behaviour discussed above) I will include it in the next release.

[SkySkimmer]

So after working on #1020, I noticed that setting the flag works, but only if you open the root folder in vscode (the one containing the _CoqProject). If you open the file from a folder that is higher in the file hierarchy, the _CoqProject still seems to load (form the logs) but we go back to the errors mentioned above (namely Cannot find a physical path bound to logical path, which leads to all the parse errors). Is this expected ?

Do you get the error only if you did make vos or also if you did regular make?

[rtetley]

Well disregard my previous comment, it seems to work actually. Idk what I messed up in my earlier tests.