Config not read unless directory is under cwd?

[mtzguido]

I have directories a and b in my home. In b/ there is a file and a config to admit queries. If I start VS code in b/ and open the file, it passes (as expected). The same happens if I start VS code in my home. But it fails if I start VS code inside A, the config does not seem to be read.
 

[gebner]

This is somewhat expected. VS Code generally follows the philosophy that you should open the whole repository. Opening subdirectories is not recommended and lots of other extensions will break too (for example the git integration will break).

What was the actual issue that you ran into? Did you go-to-definition from a file in pulse to ulib, and then the extension failed to pick up the config file in the fstar repo?

[mtzguido]

What was the actual issue that you ran into? Did you go-to-definition from a file in pulse to ulib, and then the extension failed to pick up the config file in the fstar repo?

Yes, some cross-repo jumping. If this is acceptable and expected could we just not start the extension or print a big warning?

[gebner]

Going from pulse to ulib should definitely work out of the box, without having the user to open the fstar repo/installation as a separate workspace folder.

This probably means we should read config.json files from outside the workspace. I believe that we only look inside workspace folders at the moment.