Compile file using `lean` without a lake project

Stream: lean4

[Tanner Reese]

As I understand it, to use imports in a lean file one needs to setup a package and build with lake. The process of setting up a lake project and writing a lakefile is somewhat difficult, though. Is there a way to compile a file (inside or outside a package) containing some import Mathlib statement using only lean and not lake?

[Eric Wieser]

The process of setting up a lake project and writing a lakefile is somewhat difficult, though.

Are you aware of lake new $Proj math which does most of this for you? The alternative of not using lake is much more difficult!

[Tanner Reese]

Yes, I was aware of lake new. Perhaps, I should have phrased it as "I feel setting up a whole lake project is overkill for a single file". Many languages have compilers that allow one to provide a search path for dependencies as a command line argument. I was wondering if lean had such an option.
Also, it seems that there is a built-in libraries path provided by lean --print-libdir. Is it possible (and would it cause issues) to place Mathlib or other packages directly in this folder?

[Ruben Van de Velde]

I really would recommend against trying to work around lake

[Tanner Reese]

Does lean have the ability to deal with packages independently of lake, though?

[Eric Wieser]

Everything that you are likely to want to do can be done by invoking lean manually and setting LEAN_PATH to point to the locations of the dependencies; but if you are using Mathlib, this amounts to 4000 separate invocations, which you certainly don't want to do manually

[Eric Wieser]

(If your goal is to add cmake / nix/ SCons / bazel / brazil / ... support for Lean 4 for some reason or another, then this is viable)

[Tanner Reese]

Is there a way to run a single file outside of a project with lake such that it will use the appropriate dependencies?

[Eric Wieser]

The other useful trick is using lean --deps file to have it locate the dependencies of a lean file

[Kim Morrison]

Tanner Reese said:

Is there a way to run a single file outside of a project with lake such that it will use the appropriate dependencies?

From the project that sets up the dependencies, you can lake env lean ../../path/to/single/file/outside/project.lean.