Creating Lean environment

Stream: lean4

[Joe Hendrix]

I'd like to have a function that created a Lean.Environment from a file and lean search path. The signature is something would be something like:

def loadEnv (filepath:String) (importSearchPath:[String]) : IO (Lean.Environment × MessageLog) := ...

I've tried some experiments by copying code from compileHeader from Lean.Server.FileWorker but seem to be missing some detail, because I get unknown package 'Init'.

[Jason Rute]

Forgive my naive question? What exactly is in this file you would be using to build an environment? A lean environment is a large thing since it contains all the declarations and proofs available . Do you plan to have another function which dumps the environment to a file?

[Joe Hendrix]

@Jason Rute I was planning on using this to more easily build initial environments that one could use to build fine-grained benchmarks that time simp and other tactics. This was based on an email thread with Adam Chlipala, so our interests may overlap. Another option is to script Lean itself, but that has startup and parsing overhead.
There are other uses potentially, e.g., I could use it to build a specialized compiler for some declarations. I known the Lean server and Lean itself have to do this, but that code was a bit complex for me to navigate initially. I'll probably do some more reading when I have time if there isn't a simple solution that I am overlooking.

[Jason Rute]

There are tricks in Lean 3 for setting the environment to what is was right before a particular declaration. Indeed, they have proven very useful for testing (in our case we were testing theorem proving AIs which generate proofs using only the premises available in the environment before that declaration was proved). I highly suspect these tricks were not ported to Lean 4, nor will they be, so I'd be curious to know if there is a more canonical way in Lean 4.

[Leonardo de Moura]

@Joe Hendrix Check the function runFrontend
https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Frontend.lean#L101
We used runFrondEnd for testing. You can implement loadEnv by copying this function and modifying the last few lines.

[Leonardo de Moura]

@Jason Rute You don't need any tricks to do that in Lean 4. Users can create standalone programs that import Lean.
The function runFrontend is processing a Lean file. Users can write their own version. It is all implemented in Lean.
https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Frontend.lean

[Joe Hendrix]

@Leonardo de Moura Thank you. This plus calling initSearchPath solved the problem for me.

[Sebastian Ullrich]

@Leonardo de Moura In light of this thread and https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/pure.20IO/near/231219371, should we make SearchPath an explicit parameter of importModules and remove searchPathRef?