Coq: Reset command does not use newly installed libraries

[cas-haaijman]

If I remember correctly, it was previously possible to use the Coq: Reset command to reload Coq after you installed new libraries. This no longer seems to work, if a library is added after starting loading a file in VS Code, the only way seems to load the library seems to be to close and re-open VS Code.

[gares]

Reset does not really restart the language server, and Rocq library subsystem scans the file system for libraries only at boot.
I'm afraid this is really hard to fix without changing Rocq.

In the meanwhile, you can use reload window.

[SkySkimmer]

Rocq library subsystem scans the file system for libraries only at boot

Not true, at least in coqtop it works fine to do a failing Require foo, compile foo.vo then try again

[gares]

What I meant is that the loadpath corresponding to user-contribs is populated at boot time.
If the directory in which foo will be is not there at boot, then Rocq does not find it.
Or at least, this is my diagnoses of the problem.

[SkySkimmer]

That seems correct, I guess this could be considered a Coq bug.