perf: do not cause compiler.small to export IR bodies unless the Expr body is already being exported (#10002)

src/Lean/Compiler/LCNF/Visibility.lean

@@ -30,10 +30,15 @@ where
     | .const declName .. => s.insert declName
     | _ => s
 
--- TODO: refine? balance run time vs export size
-private def isBodyRelevant (decl : Decl) : CompilerM Bool := do
-  let opts := (← getOptions)
-  decl.isTemplateLike <||> decl.value.isCodeAndM (pure <| ·.sizeLe (compiler.small.get opts))
+private def shouldExportBody (decl : Decl) : CompilerM Bool := do
+  -- Export body if template-like...
+  decl.isTemplateLike <||>
+  -- ...or it is below the (local) opportunistic inlining threshold and its `Expr` is exported
+  -- anyway, unlikely leading to more rebuilds
+  decl.value.isCodeAndM fun code => do
+    return (
+      ((← getEnv).setExporting true |>.findAsync? decl.name |>.any (·.kind == .defn)) &&
+      code.sizeLe (compiler.small.get (← getOptions)))
 
 /--
 Marks the given declaration as to be exported and recursively infers the correct visibility of its
@@ -41,7 +46,7 @@ body and referenced declarations based on that.
 -/
 partial def markDeclPublicRec (phase : Phase) (decl : Decl) : CompilerM Unit := do
   modifyEnv (setDeclPublic · decl.name)
-  if (← isBodyRelevant decl) && !isDeclTransparent (← getEnv) phase decl.name then
+  if (← shouldExportBody decl) && !isDeclTransparent (← getEnv) phase decl.name then
     trace[Compiler.inferVisibility] m!"Marking {decl.name} as transparent because it is opaque and its body looks relevant"
     modifyEnv (setDeclTransparent · phase decl.name)
     decl.value.forCodeM fun code =>

src/lake/tests/module/test.sh

@@ -8,15 +8,11 @@ source ../common.sh
 # ---
 
 mkdir Test/Generated
-# `set_option compiler.small 0` ensures that the public olean is not
-# dependent on the bodies of definitions due to automatic inlining
 cat > Test/Generated/Module.lean <<EOF
 -- File autogenerated by test.sh
 
 module
 
-set_option compiler.small 0
-
 -- insert here
 
 /-- docstring A -/

stage0/src/stdlib_flags.h

@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// Deary CI, please update stage 0
+
 namespace lean {
 options get_default_options() {
     options opts;

tests/pkg/rebuild/test.sh

@@ -11,8 +11,6 @@ cat <<EOF > Rebuild/Basic.lean
 
 module
 
-set_option compiler.small 0
-
 public def hello := "world"
 
 public def testSpec (xs : List Nat) : List Nat := xs.map (fun x => x + 1)