feat: make sure base phase contains an entry for each declaration being compiled at `init

This commit is contained in:
Leonardo de Moura 2022-09-23 16:31:38 -07:00
parent 2be8cb93ac
commit 0c82e8bd0d

View file

@ -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,