fix

src/Lean/Compiler/IR/EmitC.lean

@@ -22,7 +22,7 @@ import Lean.Runtime
 public section
 
 namespace Lean.IR.EmitC
-open Lean.Compiler.LCNF (isBoxedName isSimpleGroundDecl getSimpleGroundExpr
+open Lean.Compiler.LCNF (isBoxedName isSimpleGroundDecl isLocalSimpleGroundDecl getSimpleGroundExpr
   getSimpleGroundExprWithResolvedRefs uint64ToByteArrayLE SimpleGroundExpr SimpleGroundArg
   addSimpleGroundDecl)
 
@@ -139,13 +139,13 @@ structure GroundState where
 
 abbrev GroundM := StateT GroundState M
 
-partial def emitGroundDecl (decl : Decl) (cppBaseName : String) : M Unit := do
-  let some ground := getSimpleGroundExpr (← getEnv) decl.name | unreachable!
-  discard <| compileGround ground |>.run {}
+private partial def emitGroundDecl (e : SimpleGroundExpr) (declName : Name)
+    (cppBaseName : String) : M Unit := do
+  discard <| compileGround e |>.run {}
 where
   compileGround (e : SimpleGroundExpr) : GroundM Unit := do
     let valueName ← compileGroundToValue e
-    let declPrefix := if isClosedTermName (← getEnv) decl.name then "static" else "LEAN_EXPORT"
+    let declPrefix := if isClosedTermName (← getEnv) declName then "static" else "LEAN_EXPORT"
     emitLn <| s!"{declPrefix} const lean_object* {cppBaseName} = (const lean_object*)&{valueName};"
 
   compileGroundToValue (e : SimpleGroundExpr) : GroundM String := do
@@ -283,8 +283,8 @@ def emitFnDeclAux (decl : Decl) (cppBaseName : String) (isExternal : Bool) : M U
   let ps := decl.params
   let env ← getEnv
 
-  if isSimpleGroundDecl env decl.name then
-    emitGroundDecl decl cppBaseName
+  if let some groundExpr := getSimpleGroundExpr env decl.name then
+    emitGroundDecl groundExpr decl.name cppBaseName
   else if isClosedTermName env decl.name then
     emitFnClosedDecl decl cppBaseName
   else
@@ -619,7 +619,7 @@ def emitExternCall (f : FunId) (ps : Array Param) (extData : ExternAttrData) (ys
 
 def emitLeanFunReference (t : IRType) (f : FunId) : M Unit := do
   let env ← getEnv
-  if isSimpleGroundDecl env f then
+  if isLocalSimpleGroundDecl env f then
     emit s!"((lean_object*)({← toCName f}))"
   else if isClosedTermName env f then
     emitClosedTermRead t f
@@ -855,7 +855,7 @@ def emitDeclAux (d : Decl) : M Unit := do
   let env ← getEnv
   let (_, jpMap) := mkVarJPMaps d
   withReader (fun ctx => { ctx with jpMap := jpMap }) do
-  unless hasInitAttr env d.name || isSimpleGroundDecl env d.name do
+  unless hasInitAttr env d.name || isLocalSimpleGroundDecl env d.name do
     match d with
     | .fdecl (f := f) (xs := xs) (type := t) (body := b) .. =>
       let baseName ← toCName f;

src/Lean/Compiler/LCNF/SimpleGroundExpr.lean

@@ -95,13 +95,22 @@ builtin_initialize simpleGroundDeclExt : EnvExtension SimpleGroundExtState ←
         { s with constNames := s.constNames.insert n g, revNames := n :: s.revNames }
     )
 
+/--
+Tracks which declarations are simple ground expressions across modules.
+The non-persistent `simpleGroundDeclExt` stores the actual `SimpleGroundExpr` values within a module,
+while this extension persists just the tag across module boundaries.
+-/
+builtin_initialize simpleGroundTagExt : TagDeclarationExtension ←
+  mkTagDeclarationExtension (asyncMode := .sync)
+
 /--
 Record `declName` as mapping to the simple ground expr `expr`.
 -/
 public def addSimpleGroundDecl (env : Environment) (declName : Name) (expr : SimpleGroundExpr) :
     Environment :=
-  simpleGroundDeclExt.modifyState env fun s =>
+  let env := simpleGroundDeclExt.modifyState env fun s =>
     { s with constNames := s.constNames.insert declName expr, revNames := declName :: s.revNames }
+  simpleGroundTagExt.tag env declName
 
 /--
 Attempt to fetch a `SimpleGroundExpr` associated with `declName` if it exists.
@@ -124,10 +133,16 @@ public def getSimpleGroundExprWithResolvedRefs (env : Environment) (declName : N
   return none
 
 /--
-Check if `declName` is recorded as being a `SimpleGroundExpr`.
+Check if `declName` is recorded as being a `SimpleGroundExpr` in any module.
 -/
 public def isSimpleGroundDecl (env : Environment) (declName : Name) : Bool :=
-  (simpleGroundDeclExt.getState env).constNames.contains declName
+  simpleGroundTagExt.isTagged env declName
+
+/--
+Check if `declName` is recorded as being a `SimpleGroundExpr` in this module.
+-/
+public def isLocalSimpleGroundDecl (env : Environment) (declName : Name) : Bool :=
+  (getSimpleGroundExpr env declName).isSome
 
 public def uint64ToByteArrayLE (n : UInt64) : Array UInt8 :=
   #[
@@ -191,7 +206,7 @@ where
   compileNonFinalLet (decl : LetDecl .impure) (k : Code .impure) : DetectM SimpleGroundExpr := do
     match decl.value with
     | .fap c #[] =>
-      guard <| isSimpleGroundDecl (← getEnv) c
+      guard <| isLocalSimpleGroundDecl (← getEnv) c
       record decl.fvarId (.arg (.reference c))
       go k
     | .lit v =>
@@ -350,7 +365,7 @@ where
       let .arg elemArg := (← get).groundMap[elemId]! | failure
       return .array (elemArg :: elems).toArray.reverse
     | .fap c #[] =>
-      guard <| isSimpleGroundDecl (← getEnv) c
+      guard <| isLocalSimpleGroundDecl (← getEnv) c
       return .reference c
     | .box _ fvarId =>
       match (← get).groundMap[fvarId]! with

stage0/src/stdlib_flags.h

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