Lean 4.30+ Theorem Value Access Breaking Change
Problem
When loading a Lean 4 environment via importModules and iterating over constants,
ConstantInfo.value? returns none for ALL theorems, even though the proof terms
are present in the .olean.private files and loaded into memory.
Context / Trigger Conditions
- Building a Lean 4 code analyzer, dependency extractor, or proof graph tool
- Using
importModules to load an environment (e.g., Mathlib)
ci.value? returns none for .thmInfo constants- 0 proof dependency edges in output despite theorems existing
- Lean toolchain version is 4.30.0-rc1 or later
Root Cause
Breaking change between Lean 4.29.1 and 4.30.0-rc2 in ConstantInfo.value?:
-- Lean 4.29.1 (old behavior):
| .thmInfo {value, ..} => some value
-- Lean 4.30.0-rc2 (new behavior):
| .thmInfo {value, ..} => if allowOpaque then some value else none
In 4.30+, theorems are treated the same as opaqueInfo — their values are hidden
unless allowOpaque := true is explicitly passed. The default allowOpaque = false
causes value? to return none for all theorems.
The proof terms ARE loaded into memory (.olean.private files contain them, and
importModules loads at OLeanLevel.private by default). The data is there — the
accessor just hides it.
Solution
Option A: Pass allowOpaque := true (simplest fix)
if let some val := ci.value? (allowOpaque := true) then
-- val is the proof term
Option B: Pattern match directly (most reliable)
let valInfo := match ci with
| .defnInfo v => some (v.value, "VALUE_USES")
| .thmInfo v => some (v.value, "PROOF_USES")
| _ => none
if let some (val, edgeType) := valInfo then
let deps := val.getUsedConstantsAsSet
-- process deps
Option B is preferred for tools that need to distinguish definition bodies from
proof terms, since allowOpaque := true conflates theorems with opaque declarations.
Verification
-- This should print true for theorems in Lean 4.30+:
let some ci := env.find? `SomeTheorem | ...
match ci with
| .thmInfo v =>
eprintln s!"value? default: {ci.value?.isSome}" -- false
eprintln s!"value? opaque: {(ci.value? (allowOpaque := true)).isSome}" -- true
eprintln s!"direct access: {v.value.getUsedConstants.size}" -- >0
| _ => ...
Related Facts
.olean files have THREE levels: .olean (public), .olean.server (IDE), .olean.private (full proofs)importModules defaults to OLeanLevel.private — proofs are loadedExpr.foldConsts signature: (e : Expr) (init : α) (f : Name → α → α) : α — Name is first arg, accumulator secondExpr.getUsedConstantsAsSet returns NameSet (= Std.TreeSet Name), NOT NameHashSet (= HashSet Name)NameSet doesn't have .fold — use for dep in nameSet do instead- Mathlib scale: 354K declarations, 11.3M edges (including 4.4M PROOF_USES)
Notes
- This change aligns with proof irrelevance: for type checking, proof content doesn't
matter. Tools that DO need proofs (checkers, analyzers, graph builders) must opt in.
- The
value! function also changed — it panics for theorems unless allowOpaque := true.
ConstantInfo.getUsedConstantsAsSet (on ConstantInfo, not Expr) also uses value?
internally, so it will miss proof dependencies too.