Understanding the Lean build pipeline

Stream: lean4

[Louis Cabarion]

When building a Lean file such as ChevalleyComplexity.lean using lake build, it appears that precisely eight files are generated:

• ChevalleyComplexity.setup.json
• ChevalleyComplexity.c + ChevalleyComplexity.c.hash
• ChevalleyComplexity.trace
• ChevalleyComplexity.olean + ChevalleyComplexity.olean.hash
• ChevalleyComplexity.ilean + ChevalleyComplexity.ilean.hash

The files ending in .hash each contain a numeric checksum (such as 6944499953131117393), presumably used for cache invalidation.

As I understand it, the only file that Lean actually reads when I import ChevalleyComplexity is ChevalleyComplexity.olean. Is that correct?

If so, what roles do the remaining files play during the build process? How is the build pipeline structured: that is, which distinct build steps are executed to produce the final .olean file?

Example build:

% lake build Mathlib/RingTheory/Spectrum/Prime/ChevalleyComplexity.lean
% find .lake/ -type f -name "ChevalleyComplexity.*" | xargs file
.lake/build/ir/Mathlib/RingTheory/Spectrum/Prime/ChevalleyComplexity.c.hash:           ASCII text, with no line terminators
.lake/build/ir/Mathlib/RingTheory/Spectrum/Prime/ChevalleyComplexity.setup.json:       JSON data
.lake/build/ir/Mathlib/RingTheory/Spectrum/Prime/ChevalleyComplexity.c:                c program text, ASCII text, with very long lines (420)
.lake/build/lib/lean/Mathlib/RingTheory/Spectrum/Prime/ChevalleyComplexity.trace:      JSON data
.lake/build/lib/lean/Mathlib/RingTheory/Spectrum/Prime/ChevalleyComplexity.olean.hash: ASCII text, with no line terminators
.lake/build/lib/lean/Mathlib/RingTheory/Spectrum/Prime/ChevalleyComplexity.olean:      data
.lake/build/lib/lean/Mathlib/RingTheory/Spectrum/Prime/ChevalleyComplexity.ilean.hash: ASCII text, with no line terminators
.lake/build/lib/lean/Mathlib/RingTheory/Spectrum/Prime/ChevalleyComplexity.ilean:      JSON data

[Louis Cabarion]

Perhaps this question would be better suited for the #lean4 channel? I don’t have permission to move it over there.

[Notification Bot]

This topic was moved here from #new members > Understanding the Lean build pipeline by Michael Rothgang.

[Mac Malone]

Isak Colboubrani said:

How is the build pipeline structured: that is, which distinct build steps are executed to produce the final .olean file?

The general steps to build a module m are:

• Lake computes and emits the <m>.setup.json
• Lake runs lean <m>.lean --setup <m>.setup.json -o <m>.olean -i <m>.ilean -c <m>.c
• On success, Lake emits the <m>.trace and the .hash files for future no-op builds and invalidations.

Isak Colboubrani said:

If so, what roles do the remaining files play during the build process?

The .c file is used to generate native code for a Lean module, so that it can be compiled into, .e.g, an executable. The .ilean file is used by the Lean LSP server (and thus the VS Code extension) for various interactivity features.

[Louis Cabarion]

@Mac Malone Thanks! That clarifies a lot.

[Louis Cabarion]

If I understand correctly, the combination of <m>.setup.json (the environment in some sense) and <m>.lean together captures exactly all the inputs that can influence the output <m>.olean. Is there a way to make lake output <m>.setup.json given <m>.lean (without doing the following steps)?