From 611337ecee3632fcfaba834d3048914ce3618090 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Tue, 10 Feb 2026 09:48:36 +0100 Subject: [PATCH] doc: the different chunks of the pass manager (#12400) --- src/Lean/Compiler/LCNF/PassManager.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/Lean/Compiler/LCNF/PassManager.lean b/src/Lean/Compiler/LCNF/PassManager.lean index ca7983c6e7..0390bbcfad 100644 --- a/src/Lean/Compiler/LCNF/PassManager.lean +++ b/src/Lean/Compiler/LCNF/PassManager.lean @@ -101,9 +101,16 @@ The `PassManager` used to store all `Pass`es that will be run within pipeline. -/ structure PassManager where + /-- Passes that happen during the LCNF base phase -/ basePasses : Array Pass + /-- Passes that happen during the LCNF mono phase before lambda lifting -/ monoPasses : Array Pass + /-- + Passes that happen during the LCNF mono phase after lambda lifting. Note that lifted lambdas will + have been lifted out of the SCC they originated from if possible. + -/ monoPassesNoLambda : Array Pass + /-- Passes that happen during the LCNF impure phase. -/ impurePasses : Array Pass deriving Inhabited