lean --run unknown package

Stream: lean4

[Logan Murphy]

I have no problems with imports (using VSCode) but when I try to use lean -- run from command line I'm getting

Foo.lean:1:0: error: unknown package 'Foo'
You might need to open '/path/to/project' as a workspace in your editor
Foo.lean:3:11: error: unknown identifier 'IO'
Foo.lean:3:11: error: unknown constant 'sorryAx'

I tried opening the folder as a workspace in VSCode (i.e. file>open Workspace) but nothing seems to have changed.

Any clue what I'm doing wrong?

[Wojciech Nawrocki]

You're not doing anything wrong, lean is just currently a bit bad at locating things :) The quick fix is to set LEAN_PATH=/path/to/project/build/, so e.g. LEAN_PATH=/path/to/project/build/ lean --run Whatever.lean should work. VSCode works because the server uses leanpkg to locate files and sets LEAN_PATH for you.

[Logan Murphy]

Ah, I see. Thank you!

[Wojciech Nawrocki]

Note the edit, I got the path wrong -- it should be the directory containing .oleans, which is project/build/.