diff --git a/src/Lean/Compiler/LCNF/Visibility.lean b/src/Lean/Compiler/LCNF/Visibility.lean index f3723f6942..e30e24a603 100644 --- a/src/Lean/Compiler/LCNF/Visibility.lean +++ b/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 => diff --git a/src/lake/tests/module/test.sh b/src/lake/tests/module/test.sh index 84cd1a17ad..85da9c75de 100755 --- a/src/lake/tests/module/test.sh +++ b/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 < 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)