perf: put the compiler off the critical path (#12335)

src/Lean/Compiler/IR/AddExtern.lean

@@ -12,6 +12,7 @@ import Lean.Compiler.IR.RC
 import Lean.Compiler.LCNF.ToImpureType
 import Lean.Compiler.LCNF.ToImpure
 import Init.While
+import Lean.Compiler.LCNF.PhaseExt
 
 public section
 

src/Lean/Compiler/IR/CompilerM.lean

@@ -8,7 +8,7 @@ module
 prelude
 public import Lean.Compiler.IR.Format
 public import Lean.Compiler.ExportAttr
-public import Lean.Compiler.LCNF.PhaseExt
+public import Lean.Compiler.LCNF.PublicDeclsExt
 import Lean.Compiler.InitAttr
 import Init.Data.Format.Macro
 

src/Lean/Compiler/IR/ToIR.lean

@@ -14,7 +14,7 @@ public section
 namespace Lean.IR
 
 open Lean.Compiler (LCNF.Alt LCNF.Arg LCNF.Code LCNF.Decl LCNF.DeclValue LCNF.LCtx LCNF.LetDecl
-  LCNF.LetValue LCNF.LitValue LCNF.Param LCNF.getMonoDecl? LCNF.FVarSubst LCNF.MonadFVarSubst
+  LCNF.LetValue LCNF.LitValue LCNF.Param LCNF.FVarSubst LCNF.MonadFVarSubst
   LCNF.MonadFVarSubstState LCNF.addSubst LCNF.normLetValue LCNF.normFVar LCNF.getType LCNF.CtorInfo)
 
 namespace ToIR

src/Lean/Compiler/ImplementedByAttr.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Lean.Elab.InfoTree
-public import Lean.Compiler.LCNF.PhaseExt
 
 public section
 

src/Lean/Compiler/LCNF/PhaseExt.lean

@@ -7,29 +7,12 @@ module
 
 prelude
 public import Lean.Compiler.LCNF.PassManager
+public import Lean.Compiler.LCNF.PublicDeclsExt
 
 public section
 
 namespace Lean.Compiler.LCNF
 
-/-- Creates a replayable local environment extension holding a name set. -/
-private def mkDeclSetExt : IO (EnvExtension (List Name × NameSet)) :=
-  registerEnvExtension
-    (mkInitial := pure ([], {}))
-    (asyncMode := .sync)
-    (replay? := some <| fun oldState newState _ s =>
-      let newEntries := newState.1.take (newState.1.length - oldState.1.length)
-      newEntries.foldl (init := s) fun s n =>
-        if s.1.contains n then
-          s
-        else
-          (n :: s.1, if newState.2.contains n then s.2.insert n else s.2))
-
-/--
-Set of declarations to be exported to other modules; visibility shared by base/mono/IR phases.
--/
-private builtin_initialize publicDeclsExt : EnvExtension (List Name × NameSet) ← mkDeclSetExt
-
 -- The following extensions are per-phase as e.g. a declaration may be inlineable in the mono phase
 -- because it directly unfolds to a `_redArg` call, but making its body in the base phase available
 -- as well may lead to opportunistic inlining there, exposing references to declarations that we did
@@ -55,23 +38,6 @@ private def getTransparencyExt : Phase → EnvExtension (List Name × NameSet)
   | .mono => monoTransparentDeclsExt
   | .impure => impureTransparentDeclsExt
 
-def isDeclPublic (env : Environment) (declName : Name) : Bool := Id.run do
-  if !env.header.isModule then
-    return true
-  -- The IR compiler may call the boxed variant it introduces after we do visibility inference, so
-  -- use same visibility as base decl.
-  let inferFor := match declName with
-    | .str n "_boxed" => n
-    | n               => n
-  let (_, map) := publicDeclsExt.getState env
-  map.contains inferFor
-
-def setDeclPublic (env : Environment) (declName : Name) : Environment :=
-  if isDeclPublic env declName then
-    env
-  else
-    publicDeclsExt.modifyState env fun s =>
-      (declName :: s.1, s.2.insert declName)
 
 def isDeclTransparent (env : Environment) (phase : Phase) (declName : Name) : Bool := Id.run do
   if !env.header.isModule then

src/Lean/Compiler/LCNF/PublicDeclsExt.lean

@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+
+prelude
+public import Lean.Environment
+
+namespace Lean.Compiler.LCNF
+
+/-- Creates a replayable local environment extension holding a name set. -/
+public def mkDeclSetExt : IO (EnvExtension (List Name × NameSet)) :=
+  registerEnvExtension
+    (mkInitial := pure ([], {}))
+    (asyncMode := .sync)
+    (replay? := some <| fun oldState newState _ s =>
+      let newEntries := newState.1.take (newState.1.length - oldState.1.length)
+      newEntries.foldl (init := s) fun s n =>
+        if s.1.contains n then
+          s
+        else
+          (n :: s.1, if newState.2.contains n then s.2.insert n else s.2))
+
+/--
+Set of declarations to be exported to other modules; visibility shared by base/mono/IR phases.
+-/
+private builtin_initialize publicDeclsExt : EnvExtension (List Name × NameSet) ← mkDeclSetExt
+
+public def isDeclPublic (env : Environment) (declName : Name) : Bool := Id.run do
+  if !env.header.isModule then
+    return true
+  -- The IR compiler may call the boxed variant it introduces after we do visibility inference, so
+  -- use same visibility as base decl.
+  let inferFor := match declName with
+    | .str n "_boxed" => n
+    | n               => n
+  let (_, map) := publicDeclsExt.getState env
+  map.contains inferFor
+
+public def setDeclPublic (env : Environment) (declName : Name) : Environment :=
+  if isDeclPublic env declName then
+    env
+  else
+    publicDeclsExt.modifyState env fun s =>
+      (declName :: s.1, s.2.insert declName)
+
+end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/Visibility.lean

@@ -9,6 +9,8 @@ prelude
 public import Lean.Compiler.ImplementedByAttr
 import Lean.ExtraModUses
 import Lean.Compiler.Options
+import Lean.Compiler.LCNF.PhaseExt
+public import Lean.Compiler.LCNF.PassManager
 
 public section
 

src/Lean/Elab/BuiltinNotation.lean

@@ -11,6 +11,7 @@ public import Lean.Elab.Eval
 public import Lean.Elab.Binders
 public import Lean.IdentifierSuggestion
 meta import Lean.Parser.Do
+import Lean.Compiler.BorrowedAnnotation
 
 public section
 

src/Lean/Elab/ComputedFields.lean

@@ -9,6 +9,7 @@ prelude
 public import Lean.Meta.Constructions.CasesOn
 public import Lean.Compiler.ImplementedByAttr
 public import Lean.Elab.PreDefinition.WF.Eqns
+import Lean.Compiler.ExternAttr
 
 public section
 

src/Lean/Elab/Declaration.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Lean.Elab.MutualDef
 public import Lean.Elab.MutualInductive
+import Lean.Compiler.ExternAttr
 
 public section
 namespace Lean.Elab.Command

src/Lean/Util/TestExtern.lean

@@ -12,6 +12,7 @@ public meta import Lean.Compiler.ImplementedByAttr
 public meta import Lean.Elab.Command
 public import Init.Notation
 import Lean.Exception
+public meta import Lean.Compiler.ExternAttr
 
 public section
 

src/lake/Lake/Load/Lean/Elab.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Lake.Load.Config
-import Lean.Compiler.IR
+import Lean.Compiler.IR.CompilerM
 import Lean.Elab.Frontend
 import Lake.DSL.Extensions
 import Lake.Util.JsonObject

tests/lean/1021.lean.expected.out

@@ -1,8 +1,8 @@
 some
   {
     range :=
-      { pos := { line := 213, column := 0 }, charUtf16 := 0, endPos := { line := 218, column := 31 },
+      { pos := { line := 214, column := 0 }, charUtf16 := 0, endPos := { line := 219, column := 31 },
         endCharUtf16 := 31 },
     selectionRange :=
-      { pos := { line := 213, column := 46 }, charUtf16 := 46, endPos := { line := 213, column := 58 },
+      { pos := { line := 214, column := 46 }, charUtf16 := 46, endPos := { line := 214, column := 58 },
         endCharUtf16 := 58 } }