perf: reduce amount of symbols in DLLs (#10864)

This PR reduces the amount of symbols in our DLLs by cutting open a
linking cycle of the shape:

`Environment -> Compiler -> Meta -> Environment`

This is achieved by introducing a dynamic call to the compiler hidden
behind a `Ref` as previously
done in the pretty printer.

src/Init/Data/Format/Basic.lean

@@ -411,7 +411,6 @@ Renders a `Format` to a string.
 * `column`: begin the first line wrap `column` characters earlier than usual
   (this is useful when the output String will be printed starting at `column`)
 -/
-@[export lean_format_pretty]
 def pretty (f : Format) (width : Nat := defWidth) (indent : Nat := 0) (column := 0) : String :=
   let act : StateM State Unit := prettyM f width indent
   State.out <| act (State.mk "" column) |>.snd

src/Lean/Compiler/ExternAttr.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Lean.ProjFns
-public import Lean.Meta.Basic
+public import Lean.Attributes
 
 public section
 

src/Lean/Compiler/IR/EmitC.lean

@@ -15,7 +15,7 @@ public import Lean.Compiler.IR.Boxing
 public section
 
 namespace Lean.IR.EmitC
-open ExplicitBoxing (requiresBoxedVersion mkBoxedName isBoxedName)
+open ExplicitBoxing (isBoxedName)
 
 def leanMainFn := "_lean_main"
 

src/Lean/Compiler/LCNF/Main.lean

@@ -133,11 +133,13 @@ def showDecl (phase : Phase) (declName : Name) : CoreM Format := do
   let some decl ← getDeclAt? declName phase | return "<not-available>"
   ppDecl' decl
 
-@[export lean_lcnf_compile_decls]
 def main (declNames : Array Name) : CoreM Unit := do
   withTraceNode `Compiler (fun _ => return m!"compiling: {declNames}") do
     CompilerM.run <| discard <| PassManager.run declNames
 
+builtin_initialize
+  compileDeclsRef.set main
+
 builtin_initialize
   registerTraceClass `Compiler.init (inherited := true)
   registerTraceClass `Compiler.test (inherited := true)

src/Lean/CoreM.lean

@@ -684,9 +684,25 @@ def traceBlock (tag : String) (t : Task α) : CoreM α := do
     profileitM Exception "blocked" (← getOptions) do
       IO.wait t
 
--- Forward declaration
-@[extern "lean_lcnf_compile_decls"]
-opaque compileDeclsImpl (declNames : Array Name) : CoreM Unit
+/--
+This ref exists to break a linking cycle that goes as follows:
+- We start in `Environment.lean`, there we have functions referencing the compiler such as
+  `evalConst`
+- This pulls in the entire compiler transitively as well as all of its dependents
+- The compiler relies on things like WHNF to inspect types
+- WHNF in turn imports Environment
+
+On Windows this causes a large amount of symbols to be included in one DLL as everything that
+imports the Environment instantly requires a large chunk of the Meta stack to be linked. This ref
+breaks the cycle by making `compileDeclsImpl` a "dynamic" call through the ref that is not visible
+to the linker. In the compiler there is a matching `builtin_initialize` to set this ref to the
+actual implementation of compileDeclsRef.
+-/
+builtin_initialize compileDeclsRef : IO.Ref (Array Name → CoreM Unit) ←
+  IO.mkRef (fun _ => throwError m!"call to compileDecls with uninitialized compileDeclsRef")
+
+def compileDeclsImpl (declNames : Array Name) : CoreM Unit := do
+  (← compileDeclsRef.get) declNames
 
 -- `ref?` is used for error reporting if available
 partial def compileDecls (decls : Array Name) (logErrors := true) : CoreM Unit := do

src/Lean/PrettyPrinter.lean

@@ -68,7 +68,6 @@ def ppConstNameWithInfos (constName : Name) : MetaM FormatWithInfos := do
     let stx := (sanitizeSyntax stx).run' { options := (← getOptions) }
     formatCategory `term stx
 
-@[export lean_pp_expr]
 def ppExprLegacy (env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options) (e : Expr) : IO Format :=
   Prod.fst <$> ((withOptions (fun _ => opts) <| ppExpr e).run' { lctx := lctx } { mctx := mctx }).toIO
     { fileName := "<PrettyPrinter>", fileMap := default }

src/kernel/trace.cpp

@@ -157,33 +157,4 @@ def mkMetavarContext : Unit → MetavarContext := fun _ => {}
 */
 extern "C" lean_object* lean_mk_metavar_ctx(lean_object*);
 
-/*
-@[export lean_pp_expr]
-def ppExprLegacy (env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options) (e : Expr) : IO Format :=
-*/
-extern "C" object * lean_pp_expr(object * env, object * mctx, object * lctx, object * opts, object * e, object * w);
-
-/*
-@[export lean_format_pretty]
-def pretty (f : Format) (w : Nat := defWidth) (indent : Nat := 0) (column := 0) : String :=
-*/
-extern "C" object * lean_format_pretty(object * f, object * w, object * i, object * c);
-
-std::string pp_expr(elab_environment const & env, options const & opts, local_ctx const & lctx, expr const & e) {
-    options o = opts;
-    // o = o.update(name{"pp", "proofs"}, true); --
-    object_ref fmt = get_io_result<object_ref>(lean_pp_expr(env.to_obj_arg(), lean_mk_metavar_ctx(lean_box(0)), lctx.to_obj_arg(), o.to_obj_arg(),
-                                                            e.to_obj_arg(), io_mk_world()));
-    string_ref str(lean_format_pretty(fmt.to_obj_arg(), lean_unsigned_to_nat(80), lean_unsigned_to_nat(0), lean_unsigned_to_nat(0)));
-    return str.to_std_string();
-}
-
-std::string pp_expr(elab_environment const & env, options const & opts, expr const & e) {
-    local_ctx lctx;
-    return pp_expr(env, opts, lctx, e);
-}
-
-std::string trace_pp_expr(expr const & e) {
-    return pp_expr(*g_env, *g_opts, e);
-}
 }

src/kernel/trace.h

@@ -51,8 +51,6 @@ if (lean_is_trace_enabled(CName)) {             \
     tout() << tclass(CName); CODE               \
 }}
 
-std::string trace_pp_expr(expr const & e);
-
 void initialize_trace();
 void finalize_trace();
 }