Where is the equation compiler?

Stream: lean4

[nrs]

When people refer to the equation compiler, what part of source are they referring to?

[nrs]

Do we distinguish the element that compiles Lean to C from the one we call "equation compiler"?

[nrs]

The following is a possibility but I'm determining currently which of the two of these it is: https://leanprover-community.github.io/mathlib4_docs/Lean/Compiler/LCNF/Basic.html

[Kyle Miller]

I think the "equation compiler" is roughly everything in Lean/Elab/PreDefinition

Lean/Compiler is code generation (and watch out that there is the "old compiler", which is currently used, and the "new compiler", which is not yet), and it doesn't have to do with the equation compiler. It consumes PreDefinitions, which can be recursive.

The equation compiler is what takes PreDefinitions and turns them into non-recursive definitions that use recursors (brecOn) or well-founded recursion. The result is a term that the kernel can consume. These are also responsible for generating the equation lemmas.

[nrs]

Ah tyvm that clears up a lot! Was still digging through files

[Joachim Breitner]

I wish we had a better name for it that doesn't cause the confusion with the compiler.

[François G. Dorais]

A compiler is a function. For any function it is useful to specify the domain and codomain. The "equation compiler" yields terms that can be checked by the kernel. The "old/new compiler" yields executable code. If we were to come up with new names, I wish they would clearly indicate the codomain.

[Joachim Breitner]

I've used the term derecursifier, but mostly in jest.

[Edward van de Meent]

pre-kernel compiler?

[Edward van de Meent]

same issue, i guess

[Steve Dunham]

Perhaps "dispeller" if it is removing curses?