vscode lean-mode for non-standard project structure?

Stream: lean4

[Andrew Kent]

TL;DR Is it possible to get the nice VSCode lean-mode integration for a project with non-standard structure? (E.g., no leanpkg.toml, complicated Makefile, etc) If so... any pointers and/or examples of this working somewhere? xD

I was hoping I could do something like make sure for each of the project's pkgs Foo we include an entry :path/to/foo in LEAN_PATH where a directory Foo resides and contains all of Foo's *.olean files, and this would be enough to get all the type/documentation/etc info available when you visit the files... but so far I've only been able to get a Loading... message under a file's name in the Lean Infoview when I visit it and some orange vertical bars (which I assume indicate something is running in the background...?)

[Sebastian Ullrich]

The server will call leanpkg print-paths when opening a file, but that should do exactly nothing if there is no leanpkg.toml (give it a try on the cmdline). For a manual setup, setting LEAN_PATH is the correct way, plus you will need LEAN_SRC_PATH in the same format (but pointing at the .leans) for "go to definition". Not sure why it would hang, I'd have to give it a try. Does it print anything to the Output panel?

[Andrew Kent]

Switching from relative to absolute file paths in LEAN_PATH got things working as expected :tada:

(When using relative file paths instead of absolute file paths, the server/VSCode extension worked as expected if VSCode was launched by executing code . at the root of the project, but not if it was launched by executing code path/to/file.lean.)