Resolve import dependencies into a flat file

Stream: lean4 dev

[Alex D]

Is it possible to compile a .lean file into a format where all imports are replaced recursively with their contents (e.g. import Mathlib.Algebra.CharP.Basic should be replaced with the contents of https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Algebra/CharP/Basic.lean, and so on recursively), somehow similarly to the output of the C++ preprocessor with all headers replaced with instructions?

[Jannis Limperg]

Almost, but not quite. The meaning of import is indeed essentially, 'pretend that the imported file (and its dependencies, etc.) has been pasted here'. However, there are special initialize blocks which are executed only when a file is imported, and these are used quite pervasively under the hood.

[Alex D]

Thank you for the quick reply Jannis!