From d3491f7300c931f9d7a5e9884a7a9bf6fa0e43f0 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 28 May 2026 10:50:40 +0000 Subject: [PATCH 1/4] feat(Environment): add `Environment.hasExposedBody` MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The idiom env.setExporting true |>.find? n |>.any (·.hasValue) answers a real, self-contained question — does `env` export a body for `n` to downstream modules? — and was duplicated inline in at least eight places under five different local names (`exposed`, `exported`, `isExposed`, `bodyExposed`, plus inline uses). It also appears in Mathlib (`Mathlib/Tactic/Simps/Basic.lean`, `Mathlib/Tactic/Translate/Core.lean`). Pull it out as a small `Environment.hasExposedBody` helper with a docstring clarifying the corner cases (axioms, declarations not in the environment, the non-module case). Update all eight inline callers under `src/Lean/` to use it. Two of the callers (`Lean/Meta/Eqns.lean`, `Lean/Meta/MethodSpecs.lean`) wrap the check with `!env.header.isModule || …` so that the non-module case is treated as exposed; they keep that guard explicitly, calling `env.hasExposedBody n` for the inner check. This is a pure refactor; no behaviour change is intended. --- src/Lean/Elab/Deriving/Basic.lean | 2 +- .../PreDefinition/PartialFixpoint/Eqns.lean | 2 +- .../Elab/PreDefinition/Structural/Eqns.lean | 2 +- src/Lean/Elab/PreDefinition/WF/Eqns.lean | 2 +- src/Lean/Environment.lean | 17 +++++++++++++++++ src/Lean/Meta/Constructions/SparseCasesOn.lean | 2 +- src/Lean/Meta/Eqns.lean | 2 +- src/Lean/Meta/MethodSpecs.lean | 2 +- 8 files changed, 24 insertions(+), 7 deletions(-) diff --git a/src/Lean/Elab/Deriving/Basic.lean b/src/Lean/Elab/Deriving/Basic.lean index 060dce7e4fcf..1bc13dbf5ec0 100644 --- a/src/Lean/Elab/Deriving/Basic.lean +++ b/src/Lean/Elab/Deriving/Basic.lean @@ -181,7 +181,7 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) (isNoncomputable let decl ← whnfCore decl let .const declName _ := decl.getAppFn | throwError "Failed to delta derive instance, expecting a term of the form `C ...` where `C` is a constant, given{indentExpr decl}" - let exposed := (← getEnv).setExporting true |>.find? declName |>.any (·.hasValue) + let exposed := (← getEnv).hasExposedBody declName -- When the definition body is private, the deriving handler will need access to the private scope, -- and the instance body will automatically be private as well. withExporting (isExporting := exposed) do diff --git a/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean b/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean index 8c48e0bd63a6..e01bfbfb38c6 100644 --- a/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean @@ -29,7 +29,7 @@ public builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension (exportEntriesFn := fun env s => let all := s.toArray -- Do not export for non-exposed defs at exported/server levels - let exported := s.filter (fun n _ => (env.setExporting true).find? n |>.any (·.hasValue)) |>.toArray + let exported := s.filter (fun n _ => env.hasExposedBody n) |>.toArray { exported, server := exported, «private» := all }) public def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) diff --git a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean index f5f2ebb9d1a7..bbb0c35cb5e6 100644 --- a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean @@ -151,7 +151,7 @@ public builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension (exportEntriesFn := fun env s => let all := s.toArray -- Do not export for non-exposed defs at exported/server levels - let exported := s.filter (fun n _ => (env.setExporting true).find? n |>.any (·.hasValue)) |>.toArray + let exported := s.filter (fun n _ => env.hasExposedBody n) |>.toArray { exported, server := exported, «private» := all }) public def registerEqnsInfo (preDef : PreDefinition) (declNames : Array Name) (recArgPos : Nat) diff --git a/src/Lean/Elab/PreDefinition/WF/Eqns.lean b/src/Lean/Elab/PreDefinition/WF/Eqns.lean index 25a967bc33bd..69a38f359706 100644 --- a/src/Lean/Elab/PreDefinition/WF/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/WF/Eqns.lean @@ -27,7 +27,7 @@ public builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension (exportEntriesFn := fun env s => let all := s.toArray -- Do not export for non-exposed defs at exported/server levels - let exported := s.filter (fun n _ => (env.setExporting true).find? n |>.any (·.hasValue)) |>.toArray + let exported := s.filter (fun n _ => env.hasExposedBody n) |>.toArray { exported, server := exported, «private» := all }) public def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedParamPerms : FixedParamPerms) diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index bc11918643d5..2d03a2f5c0be 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -656,6 +656,23 @@ def setExporting (env : Environment) (isExporting : Bool) : Environment := else { env with isExporting } +/-- Returns `true` iff `env` exports a value for `n` to downstream modules. + +This is the case iff `n` is a definition (or `instance`, `theorem`, etc.) marked +`@[expose]`, an `abbrev`, or otherwise a declaration whose body is visible across module +boundaries. + +Returns `false` for axioms, opaques, declarations not present in the environment, and +declarations whose body is sealed (i.e. lacking `@[expose]` under the module system). + +Note: when the current module is not using the module system (i.e. `env.header.isModule` +is `false`), there is no sealing mechanism, so any declaration that has a value is +"exposed" in that sense. Callers that wish to treat the non-module case uniformly as +exposed (e.g. when deciding name privacy) should write +`!env.header.isModule || env.hasExposedBody n`. -/ +def hasExposedBody (env : Environment) (n : Name) : Bool := + env.setExporting true |>.find? n |>.any (·.hasValue) + /-- Consistently updates synchronous and (private) asynchronous parts of the environment without blocking. -/ private def modifyCheckedAsync (env : Environment) (f : Kernel.Environment → Kernel.Environment) : Environment := { env with checked := env.checked.map (sync := true) f, base.private := f env.base.private } diff --git a/src/Lean/Meta/Constructions/SparseCasesOn.lean b/src/Lean/Meta/Constructions/SparseCasesOn.lean index 22464fe27517..f184572b0c27 100644 --- a/src/Lean/Meta/Constructions/SparseCasesOn.lean +++ b/src/Lean/Meta/Constructions/SparseCasesOn.lean @@ -38,7 +38,7 @@ builtin_initialize sparseCasesOnInfoExt : MapDeclarationExtension SparseCasesOnI mkMapDeclarationExtension (exportEntriesFn := fun env s => let all := s.toArray -- Do not export for non-exposed defs at exported/server levels - let exported := s.filter (fun n _ => (env.setExporting true).find? n |>.any (·.hasValue)) |>.toArray + let exported := s.filter (fun n _ => env.hasExposedBody n) |>.toArray { exported, server := exported, «private» := all }) /-- diff --git a/src/Lean/Meta/Eqns.lean b/src/Lean/Meta/Eqns.lean index 91d528caae1e..efadd858dfd4 100644 --- a/src/Lean/Meta/Eqns.lean +++ b/src/Lean/Meta/Eqns.lean @@ -78,7 +78,7 @@ def declFromEqLikeName (env : Environment) (name : Name) : Option (Name × Strin return none def mkEqLikeNameFor (env : Environment) (declName : Name) (suffix : String) : Name := - let isExposed := !env.header.isModule || ((env.setExporting true).find? declName).elim false (·.hasValue) + let isExposed := !env.header.isModule || env.hasExposedBody declName let name := .str declName suffix let name := if isExposed then name else mkPrivateName env name name diff --git a/src/Lean/Meta/MethodSpecs.lean b/src/Lean/Meta/MethodSpecs.lean index fcbb9ef03181..9abb0830f6ce 100644 --- a/src/Lean/Meta/MethodSpecs.lean +++ b/src/Lean/Meta/MethodSpecs.lean @@ -65,7 +65,7 @@ def getMethodSpecsInfo (instName : Name) : MetaM MethodSpecsInfo := do unless xs == ys do throwError "function `{f}` does not take its arguments in the same order as the instance" let implName := f.constName! - let isExposed := !(← getEnv).header.isModule || (((← getEnv).setExporting true).find? implName).elim false (·.hasValue) + let isExposed := !(← getEnv).header.isModule || (← getEnv).hasExposedBody implName unless isExposed do privateSpecs := true -- Construct the replacement theorems From 02abfa66a1c95ead104a0245bad6e83d08fdf617 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 28 May 2026 11:05:13 +0000 Subject: [PATCH 2/4] fixup: rewrite hasExposedBody docstring, dedup getEnv, add test MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Per review: - Rewrite the `hasExposedBody` docstring. The previous wording said `n` could be a "definition (or `instance`, `theorem`, etc.)" — but `ConstantInfo.hasValue` with the default `allowOpaque := false` returns `true` only for `defnInfo`, so the function returns `false` for theorems and opaques. State that plainly, and re-frame the non-module note: the suggested `!env.header.isModule || env.hasExposedBody n` pattern is a *policy* (bypass the body-exposed check outside modules) rather than a fact about `n`'s body. - In `Lean/Meta/MethodSpecs.lean`, bind `env` once rather than calling `(← getEnv)` twice in the same line. - Add a small test in `tests/elab/hasExposedBody.lean` covering exposed `def`, sealed `def`, theorem, opaque, axiom, inductive, and a missing name. --- src/Lean/Environment.lean | 27 +++++++++++++-------------- src/Lean/Meta/MethodSpecs.lean | 3 ++- tests/elab/hasExposedBody.lean | 28 ++++++++++++++++++++++++++++ 3 files changed, 43 insertions(+), 15 deletions(-) create mode 100644 tests/elab/hasExposedBody.lean diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 2d03a2f5c0be..81a4b9686c62 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -656,20 +656,19 @@ def setExporting (env : Environment) (isExporting : Bool) : Environment := else { env with isExporting } -/-- Returns `true` iff `env` exports a value for `n` to downstream modules. - -This is the case iff `n` is a definition (or `instance`, `theorem`, etc.) marked -`@[expose]`, an `abbrev`, or otherwise a declaration whose body is visible across module -boundaries. - -Returns `false` for axioms, opaques, declarations not present in the environment, and -declarations whose body is sealed (i.e. lacking `@[expose]` under the module system). - -Note: when the current module is not using the module system (i.e. `env.header.isModule` -is `false`), there is no sealing mechanism, so any declaration that has a value is -"exposed" in that sense. Callers that wish to treat the non-module case uniformly as -exposed (e.g. when deciding name privacy) should write -`!env.header.isModule || env.hasExposedBody n`. -/ +/-- Returns `true` iff `n` resolves, in `env`'s exported view, to a `def` with a value. + +Concretely this checks whether downstream modules can see a reducible body for `n` +(an exposed definition or an `abbrev`). Returns `false` for theorems and opaque +declarations (this uses `hasValue` with `allowOpaque := false`), axioms, inductives, +constructors, recursors, declarations not in the environment, and `def`s whose body +is sealed by the module system. + +Outside the module system, `setExporting true` is a no-op, so this collapses to +"does `n` resolve to a `def` in the current environment?". Callers that instead +want to *bypass* the body-exposed check entirely outside modules (e.g. for name- +privacy decisions, where there is no sealing boundary anyway) should write that +policy explicitly: `!env.header.isModule || env.hasExposedBody n`. -/ def hasExposedBody (env : Environment) (n : Name) : Bool := env.setExporting true |>.find? n |>.any (·.hasValue) diff --git a/src/Lean/Meta/MethodSpecs.lean b/src/Lean/Meta/MethodSpecs.lean index 9abb0830f6ce..cc829c27427b 100644 --- a/src/Lean/Meta/MethodSpecs.lean +++ b/src/Lean/Meta/MethodSpecs.lean @@ -65,7 +65,8 @@ def getMethodSpecsInfo (instName : Name) : MetaM MethodSpecsInfo := do unless xs == ys do throwError "function `{f}` does not take its arguments in the same order as the instance" let implName := f.constName! - let isExposed := !(← getEnv).header.isModule || (← getEnv).hasExposedBody implName + let env ← getEnv + let isExposed := !env.header.isModule || env.hasExposedBody implName unless isExposed do privateSpecs := true -- Construct the replacement theorems diff --git a/tests/elab/hasExposedBody.lean b/tests/elab/hasExposedBody.lean new file mode 100644 index 000000000000..d1d7483f59df --- /dev/null +++ b/tests/elab/hasExposedBody.lean @@ -0,0 +1,28 @@ +module +import Lean.Elab.Command + +/-! +# Tests for `Lean.Environment.hasExposedBody` + +Confirms the function returns `true` only for `def`s whose body is exposed across +module boundaries, and `false` for theorems, opaques, axioms, inductives, +declarations not in the environment, and `def`s whose body is sealed by the +module system. +-/ + +@[expose] def exposedDef : Nat := 0 +def sealedDef : Nat := 1 +theorem aTheorem : 0 = 0 := rfl +opaque anOpaque : Nat := 2 +axiom anAxiom : Nat +inductive AnInductive where | mk + +run_cmd do + let env ← Lean.getEnv + guard <| env.hasExposedBody ``exposedDef + guard <| !env.hasExposedBody ``sealedDef + guard <| !env.hasExposedBody ``aTheorem + guard <| !env.hasExposedBody ``anOpaque + guard <| !env.hasExposedBody ``anAxiom + guard <| !env.hasExposedBody ``AnInductive + guard <| !env.hasExposedBody `nonexistent.name From d5bab2be65ceb3029b55010134b834d898cd3841 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 28 May 2026 11:25:39 +0000 Subject: [PATCH 3/4] fix: move hasExposedBody to after Environment.find? The helper was placed right after setExporting (line ~660), but Environment.find? isn't defined until line ~855 in the same file. Move the helper to right after find? so it's visible at the use site. --- src/Lean/Environment.lean | 32 ++++++++++++++++---------------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 81a4b9686c62..fa45cdb5406a 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -656,22 +656,6 @@ def setExporting (env : Environment) (isExporting : Bool) : Environment := else { env with isExporting } -/-- Returns `true` iff `n` resolves, in `env`'s exported view, to a `def` with a value. - -Concretely this checks whether downstream modules can see a reducible body for `n` -(an exposed definition or an `abbrev`). Returns `false` for theorems and opaque -declarations (this uses `hasValue` with `allowOpaque := false`), axioms, inductives, -constructors, recursors, declarations not in the environment, and `def`s whose body -is sealed by the module system. - -Outside the module system, `setExporting true` is a no-op, so this collapses to -"does `n` resolve to a `def` in the current environment?". Callers that instead -want to *bypass* the body-exposed check entirely outside modules (e.g. for name- -privacy decisions, where there is no sealing boundary anyway) should write that -policy explicitly: `!env.header.isModule || env.hasExposedBody n`. -/ -def hasExposedBody (env : Environment) (n : Name) : Bool := - env.setExporting true |>.find? n |>.any (·.hasValue) - /-- Consistently updates synchronous and (private) asynchronous parts of the environment without blocking. -/ private def modifyCheckedAsync (env : Environment) (f : Kernel.Environment → Kernel.Environment) : Environment := { env with checked := env.checked.map (sync := true) f, base.private := f env.base.private } @@ -857,6 +841,22 @@ def find? (env : Environment) (n : Name) (skipRealize := false) : Option Constan return c env.findAsyncCore? n (skipRealize := skipRealize) |>.map (·.toConstantInfo) +/-- Returns `true` iff `n` resolves, in `env`'s exported view, to a `def` with a value. + +Concretely this checks whether downstream modules can see a reducible body for `n` +(an exposed definition or an `abbrev`). Returns `false` for theorems and opaque +declarations (this uses `hasValue` with `allowOpaque := false`), axioms, inductives, +constructors, recursors, declarations not in the environment, and `def`s whose body +is sealed by the module system. + +Outside the module system, `setExporting true` is a no-op, so this collapses to +"does `n` resolve to a `def` in the current environment?". Callers that instead +want to *bypass* the body-exposed check entirely outside modules (e.g. for name- +privacy decisions, where there is no sealing boundary anyway) should write that +policy explicitly: `!env.header.isModule || env.hasExposedBody n`. -/ +def hasExposedBody (env : Environment) (n : Name) : Bool := + env.setExporting true |>.find? n |>.any (·.hasValue) + /-- Allows `realizeConst` calls for the given declaration in all derived environment branches. Realizations will run using the given environment and options to ensure deterministic results. Note From ffe74086fb17b45581b6f89209a6e41f14e1c4fa Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 28 May 2026 17:35:36 +0000 Subject: [PATCH 4/4] fix: avoid `guard` in hasExposedBody test `guard` needs an `Alternative` instance, which `CommandElabM` lacks, so the test failed to elaborate. Use `unless`/`if` + `throwError` instead, which need no `Alternative`. --- tests/elab/hasExposedBody.lean | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/tests/elab/hasExposedBody.lean b/tests/elab/hasExposedBody.lean index d1d7483f59df..9732abb4dc6c 100644 --- a/tests/elab/hasExposedBody.lean +++ b/tests/elab/hasExposedBody.lean @@ -19,10 +19,8 @@ inductive AnInductive where | mk run_cmd do let env ← Lean.getEnv - guard <| env.hasExposedBody ``exposedDef - guard <| !env.hasExposedBody ``sealedDef - guard <| !env.hasExposedBody ``aTheorem - guard <| !env.hasExposedBody ``anOpaque - guard <| !env.hasExposedBody ``anAxiom - guard <| !env.hasExposedBody ``AnInductive - guard <| !env.hasExposedBody `nonexistent.name + unless env.hasExposedBody ``exposedDef do + throwError "`exposedDef` should have an exposed body" + for n in [``sealedDef, ``aTheorem, ``anOpaque, ``anAxiom, ``AnInductive, `nonexistent.name] do + if env.hasExposedBody n then + throwError "`{n}` should not have an exposed body"