Run lean to type check a file

Stream: lean4

[Haniel Barbosa]

Hello. In lean3 I could run the lean binary on a lean file to typecheck it modulo a set of imports. I've only managed to do this in lean4 for files without imports (other than the stdlib). Looking through other topics it seems that the way to do this is by manually setting LEAN_PATH and LEAN4_DIR, but it was not so clear to me how exactly I should set them. What is the best way to do this?

[Sebastian Ullrich]

The standard way is to use leanpkg build with a leanpkg.toml

[Sebastian Ullrich]

For more information on LEAN_PATH, see https://github.com/leanprover/lean4/blob/master/src/Lean/Util/Path.lean#L6-L9

[Haniel Barbosa]

Thanks! I have been using leanpkg build already but it's a bit cumbersome for my use case (where I've deep embedded a calculus and I'm checking whether a derivation in this calculus type checks). I'll try to figure out LEAN_PATH from the link you sent.

[Mario Carneiro]

Would it be possible for leanpkg to support building a single file specified at the command line plus its dependencies? That would allow getting back some of the functionality of lean --make

[Sebastian Ullrich]

Yes, leanpkg print-paths A.B will build A.B. This is what the server is running automatically when you open that file.