How does Lean get the right CoreM in the following example?

Stream: lean4

[nrs]

open Lean Lean.Expr

def myCoreM : CoreM Unit := do
  let env ← getEnv
  for (n,c) in env.constants do
    if let none := env.getModuleIdxFor? n then println! n

The above code will work out of the box without any additional declaration. How does Lean get exactly the right CoreM (and not, e.g., the default CoreM with an empty environment) such that env ← getEnv gets the current environment? Any reading in the Lean4 source that could help me figure this out?

[Mario Carneiro]

There is only one CoreM, the monad constructs a function that accepts an environment. So myCoreM is actually a function, and when you call it you have to provide the environment to run on

[Mario Carneiro]

when you use #eval or run_meta to evaluate things in CoreM, it implicitly passes the current environment. But you can call myCoreM under an empty environment if you want

[nrs]

ah I see, that makes a lot of sense, ty! I will look into #eval

[nrs]

Mario Carneiro said:

when you use #eval or run_meta to evaluate things in CoreM, it implicitly passes the current environment. But you can call myCoreM under an empty environment if you want

hm, would you know if elabEvalCoreUnsafe presupposes CommandElabM Unit is already given a context?

[Mario Carneiro]

yes, it's all a bit metacircular, #eval itself is a command running in CommandElabM which is given an environment to run on and modify

[nrs]

hm ok I see, does context-giving have any clear entry-point I could take a look at?

[Mario Carneiro]

and it evaluates the provided code by elaborating it to a value of type CommandElabM Unit (give or take) and then running it using regular monad bind, which runs the user code in the context of the environment available to the #eval command

[Mario Carneiro]

what kind of thing are you looking for specifically?

[Mario Carneiro]

the main body of a lean file is exactly commands like this, since the environment is not just context but mutable state of the CommandElabM monad

[Mario Carneiro]

so you start from an empty* environment, run all the commands, which each add something to the environment and chain together, then you take the resulting environment and write it to a file

[Mario Carneiro]

if you are looking for something that does things to the environment rather than just passing it around like a token, that would be docs#Lean.Environment.addDecl, which kernel-checks and adds a declaration to the environment

[nrs]

Mario Carneiro said:

what kind of thing are you looking for specifically?

I'm trying to sketch what the pipeline looks like when you start with a pure .lean file with commands, and obtain an environment where there are inhabitants to [Lean.ConstantInfo](https://leanprover-community.github.io/mathlib4_docs/Lean/Declaration.html#Lean.ConstantInfo) corresponding to each command.

So I'm trying to sketch the pipeline that goes from having a pure text file to having an environment filled with declarations

[Mario Carneiro]

You may also be interested in the server state, which contains a bunch of Snapshot objects which contain environments in them, so that when you make a modification in the middle of the file it can easily roll back to the right parent environment to re-elaborate the current command

[Mario Carneiro]

nrs said:

So I'm trying to sketch the pipeline that goes from having a pure text file to having an environment filled with declarations

Okay so my addDecl comment was the right response

[Mario Carneiro]

that's the piece that actually modifies the hashmaps containing constantinfos

[nrs]

ah yes addDecl does exactly what I'm looking for. I'll be delving deeper into it to figure out how it works, thank you very much for the comments!

[nrs]

server state also seems relevant, I'll slowly be reading through all of this, thank you very much!!