From 0c82e8bd0de1aef3065eaafd6c8e8b775477f10b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 23 Sep 2022 16:31:38 -0700
Subject: [PATCH] feat: make sure base phase contains an entry for each
 declaration being compiled at `init

---
 src/Lean/Compiler/LCNF/Passes.lean | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Compiler/LCNF/Passes.lean b/src/Lean/Compiler/LCNF/Passes.lean
index 795eede4eb..95b167d52f 100644
--- a/src/Lean/Compiler/LCNF/Passes.lean
+++ b/src/Lean/Compiler/LCNF/Passes.lean
@@ -17,9 +17,16 @@ namespace Lean.Compiler.LCNF
 
 open PassInstaller
 
+def init : Pass where
+  name  := `init
+  run   := fun decls => do
+    decls.forM (·.saveBase)
+    return decls
+  phase := .base
+
 def builtinPassManager : PassManager := {
   passes := #[
-    { name := `init, run := pure, phase := .base },
+    init,
     pullInstances,
     cse,
     simp,