Beginner Questions

Stream: lean4 dev

[Hanting Zhang]

Hello, I hope this is the right place to post some beginner-level questions about the compiler. I've tried asking in #lean4 but they mostly just get buried.

I was playing around with the LCNF compiler, and wondered if there is any way to run Compiler.compile on an input file? I want to try something like Elab.runFrontend, where I give the function a filename and it will parse the file and compile it for me, then return the output. I did try hacking around a bit and discovered that LCNF declarations are saved in a persistent env extension, which was really helpful, but I'm confused as to where exactly these declarations are being added to the env? It seems like they are as soon as each definition command is elaborated -- that's my best guess at least. If someone could shed some light on this, I would really appreciate it!

Also, is there any way to turn off a compiler pass entirely? (Like specialize for example)

[Sebastian Ullrich]

It seems like they are as soon as each definition command is elaborated

That is correct, as they might be used by a #eval or other metaprogram as the next command

[Sebastian Ullrich]

Hanting Zhang said:

Also, is there any way to turn off a compiler pass entirely? (Like specialize for example)

That might be possible with PassInstaller.replacePass, though I've never used that API before

[Hanting Zhang]

Sebastian Ullrich said:

It seems like they are as soon as each definition command is elaborated

That is correct, as they might be used by a #eval or other metaprogram as the next command

Is there a specific function in CommandElabM where this happens?

[Mario Carneiro]

I think the entry point is addAndCompile

[Mario Carneiro]

at least, that's the entry point for the old compiler, presumably the new compiler runs there as well

[Hanting Zhang]

Ah, ok I see why this was so weird now. There's an @[extern "lean_lcnf_compile_decls"] that points to back Compiler.LCNF.main... thank you!

[Hanting Zhang]

Hmm, it doesn't seem like there's an easy way to turn off a compiler pass. The PassManager is registered as a builtin and as far as I understand these are stored to persist in memory somewhere (?) -- please correct me if I'm wrong. I guess is there any possible way to tweak builtin options before running the frontend? Could I also just recompile all of Lean 4 with that specific option deleted?

[Mario Carneiro]

looking at the code, it seems like you can set a PassInstaller, which is passed an array of passes and can do whatever it wants to it, not just add things but also remove them

[Mario Carneiro]

Look for uses of the @[cpass] attribute in the tests

[Hanting Zhang]

Ok, I see. However, all of the tests still use #eval in the end to check their results. Is there any way to not rely on #eval and run the compiler on a new file completely? Ideally something like

def Lean.compileFrontend (file : FilePath) (passes : Array Pass) : IO $ Array Decl <+ other info> :=
  ... <something?>

[Hanting Zhang]

One issue with my approach is that everything is running in MetaM, CoreM, or CompilerM, which I can't reconstruct from IO. But I'm not sure how to deal with this, is there a better approach for what I want here?

[Mario Carneiro]

It's a bit annoying to work directly from IO, but you can do it, after all that's what lean itself does. You have to load an environment and work inside it using withImportModules. There are even some compiler tests that use this function, like ctor_layout.lean

[Mario Carneiro]

You can't make a function with exactly that signature though because withImportModules works in a callback, and it is not safe to use any lean objects obtained from the environment after the callback terminates, so it usually has to encompass the entire program

[Hanting Zhang]

Ok, this looks interesting, I'll take a look. Thank you!