From 85341d02ac340eb4bd7bc7d1577740f6bf9a2b51 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 30 Jan 2026 17:07:25 +0100 Subject: [PATCH] feat: immediate `noncomputable` check (#12028) This PR gives a simpler semantics to `noncomputable`, improving predictability as well as preparing codegen to be moved into a separate build step without breaking immediate generation of error messages. Specifically, `noncomputable` is now needed whenever an axiom or another `noncomputable` def is used by a def except for the following special cases: * uses inside proofs, types, type formers, and constructor arguments corresponding to (fixed) inductive parameters are ignored * uses of functions marked `@[extern]/@[implemented_by]/@[csimp]` are ignored * for applications of a function marked `@[macro_inline]`, noncomputability of the inlining is instead inspected # Breaking change After this change, more `noncomputable` annotations than before may be required in exchange for improved future stability. --- src/Lean/Compiler/IR/ToIR.lean | 3 +- src/Lean/Compiler/LCNF/ToLCNF.lean | 39 ++++++++++++- src/Lean/Compiler/LCNF/ToMono.lean | 78 +++++++++---------------- src/Lean/Compiler/LCNF/Visibility.lean | 4 +- tests/lean/run/10213.lean | 2 +- tests/lean/run/9806.lean | 3 +- tests/lean/run/noncomputableUnused.lean | 4 +- tests/lean/run/pow_exploit.lean | 4 +- tests/lean/run/unsafeInit.lean | 2 +- tests/lean/run/usesOfNoncomputable.lean | 2 +- 10 files changed, 76 insertions(+), 65 deletions(-) diff --git a/src/Lean/Compiler/IR/ToIR.lean b/src/Lean/Compiler/IR/ToIR.lean index 15dce36813..2dfb142c4e 100644 --- a/src/Lean/Compiler/IR/ToIR.lean +++ b/src/Lean/Compiler/IR/ToIR.lean @@ -250,7 +250,8 @@ partial def lowerLet (decl : LCNF.LetDecl .pure) (k : LCNF.Code .pure) : M FnBod | some (.defnInfo ..) | some (.opaqueInfo ..) => mkFap name irArgs | some (.axiomInfo ..) | .some (.quotInfo ..) | .some (.inductInfo ..) | .some (.thmInfo ..) => - throwNamedError lean.dependsOnNoncomputable f!"`{name}` not supported by code generator; consider marking definition as `noncomputable`" + -- Should have been caught by `ToLCNF` + throwError f!"ToIR: unexpected use of noncomputable declaration `{name}`; please report this issue" | some (.recInfo ..) => throwError f!"code generator does not support recursor `{name}` yet, consider using 'match ... with' and/or structural recursion" | none => panic! "reference to unbound name" diff --git a/src/Lean/Compiler/LCNF/ToLCNF.lean b/src/Lean/Compiler/LCNF/ToLCNF.lean index 22b13d275f..f94ae06f1e 100644 --- a/src/Lean/Compiler/LCNF/ToLCNF.lean +++ b/src/Lean/Compiler/LCNF/ToLCNF.lean @@ -12,6 +12,8 @@ public import Lean.Compiler.LCNF.Bind public import Lean.Compiler.NeverExtractAttr import Lean.Meta.CasesInfo import Lean.Meta.WHNF +import Lean.Compiler.NoncomputableAttr +import Lean.AddDecl public section namespace Lean.Compiler.LCNF namespace ToLCNF @@ -194,6 +196,13 @@ where else return c +structure Context where + /-- + Whether uses of `noncomputable` defs should be ignored; used in contexts that will be erased + eventually. + -/ + ignoreNoncomputable : Bool := false + structure State where /-- Local context containing the original Lean types (not LCNF ones). -/ lctx : LocalContext := {} @@ -219,7 +228,7 @@ structure State where -/ toAny : FVarIdSet := {} -abbrev M := StateRefT State CompilerM +abbrev M := ReaderT Context <| StateRefT State CompilerM @[inline] def liftMetaM (x : MetaM α) : M α := do x.run' { lctx := (← get).lctx } @@ -253,7 +262,7 @@ def toCode (result : Arg .pure) : M (Code .pure) := do seqToCode (← get).seq (.return fvarId) def run (x : M α) : CompilerM α := - x |>.run' {} + x.run {} |>.run' {} /-- Return true iff `type` is `Sort _` or `As → Sort _`. @@ -391,6 +400,16 @@ def etaExpandN (e : Expr) (n : Nat) : M Expr := do Meta.forallBoundedTelescope (← Meta.inferType e) n fun xs _ => Meta.mkLambdaFVars xs (mkAppN e xs) +private def checkComputable (ref : Name) : M Unit := do + if (← read).ignoreNoncomputable then + return + if ref matches ``Quot.mk | ``Quot.lift || isExtern (← getEnv) ref || (getImplementedBy? (← getEnv) ref).isSome then + return + if isNoncomputable (← getEnv) ref then + throwNamedError lean.dependsOnNoncomputable m!"failed to compile definition, consider marking it as 'noncomputable' because it depends on '{.ofConstName ref}', which is 'noncomputable'" + else if getOriginalConstKind? (← getEnv) ref matches some .axiom | some .quot | some .induct | some .thm then + throwNamedError lean.dependsOnNoncomputable f!"`{ref}` not supported by code generator; consider marking definition as `noncomputable`" + /-- Eta reduce implicits. We use this function to eliminate introduced by the implicit lambda feature, where it generates terms such as `fun {α} => ReaderT.pure` @@ -606,7 +625,20 @@ where visitCtor (arity : Nat) (e : Expr) : M (Arg .pure) := etaIfUnderApplied e arity do - visitAppDefaultConst e.getAppFn e.getAppArgs + let f := e.getAppFn + let args := e.getAppArgs + let env ← getEnv + let .const declName us := CSimp.replaceConstants env f | unreachable! + let ctorInfo? ← isCtor? declName + let args ← args.mapIdxM fun idx arg => + -- We can rely on `toMono` erasing ctor params eventually; we do not do so here so that type + -- inference on the value is preserved. + withReader (fun ctx => + { ignoreNoncomputable := ctx.ignoreNoncomputable || ctorInfo?.any (idx < ·.numParams) }) do + visitAppArg arg + if hasNeverExtractAttribute env declName then + modify fun s => {s with shouldCache := false } + letValueToArg <| .const declName us args visitQuotLift (e : Expr) : M (Arg .pure) := do let arity := 6 @@ -723,6 +755,7 @@ where visitApp (e : Expr) : M (Arg .pure) := do if let .const declName us := CSimp.replaceConstants (← getEnv) e.getAppFn then + checkComputable declName if declName == ``Quot.lift then visitQuotLift e else if declName == ``Quot.mk then diff --git a/src/Lean/Compiler/LCNF/ToMono.lean b/src/Lean/Compiler/LCNF/ToMono.lean index 9f74b1f436..f1e7d20f2b 100644 --- a/src/Lean/Compiler/LCNF/ToMono.lean +++ b/src/Lean/Compiler/LCNF/ToMono.lean @@ -16,7 +16,6 @@ namespace Lean.Compiler.LCNF structure ToMonoM.State where typeParams : FVarIdHashSet := {} - noncomputableVars : Std.HashMap FVarId Name := {} abbrev ToMonoM := StateRefT ToMonoM.State CompilerM @@ -25,34 +24,17 @@ def Param.toMono (param : Param .pure) : ToMonoM (Param .pure) := do modify fun s => { s with typeParams := s.typeParams.insert param.fvarId } param.update (← toMonoType param.type) -def throwNoncomputableError {α : Type} (declName : Name) : ToMonoM α := - throwNamedError lean.dependsOnNoncomputable m!"failed to compile definition, consider marking it as 'noncomputable' because it depends on '{.ofConstName declName}', which is 'noncomputable'" - -def checkFVarUse (fvarId : FVarId) : ToMonoM Unit := do - if let some declName := (← get).noncomputableVars.get? fvarId then - throwNoncomputableError declName - -def checkFVarUseDeferred (resultFVar fvarId : FVarId) : ToMonoM Unit := do - if let some declName := (← get).noncomputableVars.get? fvarId then - modify fun s => { s with noncomputableVars := s.noncomputableVars.insert resultFVar declName } - @[inline] -def argToMonoBase (check : FVarId → ToMonoM Unit) (arg : Arg .pure) : ToMonoM (Arg .pure) := do +def argToMono (arg : Arg .pure) : ToMonoM (Arg .pure) := do match arg with | .erased | .type .. => return .erased | .fvar fvarId => if (← get).typeParams.contains fvarId then return .erased else - check fvarId return arg -def argToMono (arg : Arg .pure) : ToMonoM (Arg .pure) := argToMonoBase checkFVarUse arg - -def argToMonoDeferredCheck (resultFVar : FVarId) (arg : Arg .pure) : ToMonoM (Arg .pure) := - argToMonoBase (checkFVarUseDeferred resultFVar) arg - -def argsToMonoWithFnType (resultFVar : FVarId) (args : Array (Arg .pure)) (type : Expr) +def argsToMonoWithFnType (args : Array (Arg .pure)) (type : Expr) : ToMonoM (Array (Arg .pure)) := do let mut remainingType : Option Expr := some type let mut result := Array.emptyWithCapacity args.size @@ -62,14 +44,14 @@ def argsToMonoWithFnType (resultFVar : FVarId) (args : Array (Arg .pure)) (type if d.isErased then pure .erased else - argToMonoDeferredCheck resultFVar arg + argToMono arg else remainingType := none - argToMonoDeferredCheck resultFVar arg + argToMono arg result := result.push monoArg return result -def argsToMonoRedArg (resultFVar : FVarId) (args : Array (Arg .pure)) (params : Array (Param .pure)) +def argsToMonoRedArg (args : Array (Arg .pure)) (params : Array (Param .pure)) (redArgs : Array (Arg .pure)) : ToMonoM (Array (Arg .pure)) := do let mut result := #[] let mut argIdx := 0 @@ -78,23 +60,23 @@ def argsToMonoRedArg (resultFVar : FVarId) (args : Array (Arg .pure)) (params : | .fvar fvarId => while params[argIdx]!.fvarId != fvarId do argIdx := argIdx + 1 - let arg ← argToMonoDeferredCheck resultFVar args[argIdx]! + let arg ← argToMono args[argIdx]! argIdx := argIdx + 1 result := result.push arg | .erased | .type _ => pure () for arg in args[params.size...*] do - let arg ← argToMonoDeferredCheck resultFVar arg + let arg ← argToMono arg result := result.push arg return result -def ctorAppToMono (resultFVar : FVarId) (ctorInfo : ConstructorVal) (args : Array (Arg .pure)) +def ctorAppToMono (ctorInfo : ConstructorVal) (args : Array (Arg .pure)) : ToMonoM (LetValue .pure) := do let argsNewParams : Array (Arg .pure) := .replicate ctorInfo.numParams .erased - let argsNewFields ← args[ctorInfo.numParams...*].toArray.mapM (argToMonoDeferredCheck resultFVar) + let argsNewFields ← args[ctorInfo.numParams...*].toArray.mapM argToMono let argsNew := argsNewParams ++ argsNewFields return .const ctorInfo.name [] argsNew -partial def LetValue.toMono (e : LetValue .pure) (resultFVar : FVarId) : ToMonoM (LetValue .pure) := do +partial def LetValue.toMono (e : LetValue .pure) : ToMonoM (LetValue .pure) := do match e with | .erased | .lit .. => return e | .const declName _ args => @@ -125,48 +107,43 @@ partial def LetValue.toMono (e : LetValue .pure) (resultFVar : FVarId) : ToMonoM unreachable! else if let some (.ctorInfo ctorInfo) := (← getEnv).find? declName then if let some info ← hasTrivialStructure? ctorInfo.induct then - args[ctorInfo.numParams + info.fieldIdx]!.toLetValue.toMono resultFVar + args[ctorInfo.numParams + info.fieldIdx]!.toLetValue.toMono else - ctorAppToMono resultFVar ctorInfo args + ctorAppToMono ctorInfo args else let env ← getEnv - if isNoncomputable env declName && !(isExtern env declName) then - modify fun s => { s with noncomputableVars := s.noncomputableVars.insert resultFVar declName } if let some monoDecl ← getMonoDecl? declName then if args.size >= monoDecl.params.size then if let .code (.let { fvarId := resultFVar, value := .const callName _ callArgs, .. } (.return retFVar)) := monoDecl.value then let redArgDeclName := declName ++ `_redArg if callName == redArgDeclName && retFVar == resultFVar then - let args ← argsToMonoRedArg resultFVar args monoDecl.params callArgs + let args ← argsToMonoRedArg args monoDecl.params callArgs return .const redArgDeclName [] args - let args ← argsToMonoWithFnType resultFVar args monoDecl.type + let args ← argsToMonoWithFnType args monoDecl.type return .const declName [] args else - let args ← args.mapM (argToMonoDeferredCheck resultFVar) + let args ← args.mapM argToMono return .const declName [] args | .fvar fvarId args => if (← get).typeParams.contains fvarId then return .erased else - checkFVarUseDeferred resultFVar fvarId - return .fvar fvarId (← args.mapM (argToMonoDeferredCheck resultFVar)) - | .proj structName fieldIdx baseFVar => - if (← get).typeParams.contains baseFVar then + return .fvar fvarId (← args.mapM argToMono) + | .proj structName fieldIdx fvarId => + if (← get).typeParams.contains fvarId then return .erased - else - checkFVarUseDeferred resultFVar baseFVar - if let some info ← hasTrivialStructure? structName then - if info.fieldIdx == fieldIdx then - return .fvar baseFVar #[] - else - return .erased + else if let some info ← hasTrivialStructure? structName then + if info.fieldIdx == fieldIdx then + return .fvar fvarId #[] else - return e + return .erased + else + return e def LetDecl.toMono (decl : LetDecl .pure) : ToMonoM (LetDecl .pure) := do let type ← toMonoType decl.type - let value ← decl.value.toMono decl.fvarId + let value ← decl.value.toMono decl.update type value def mkFieldParamsForComputedFields (ctorType : Expr) (numParams : Nat) (numNewFields : Nat) @@ -370,11 +347,8 @@ partial def Code.toMono (code : Code .pure) : ToMonoM (Code .pure) := do | .fun decl k | .jp decl k => return code.updateFun! (← decl.toMono) (← k.toMono) | .unreach type => return .unreach (← toMonoType type) | .jmp fvarId args => return code.updateJmp! fvarId (← args.mapM argToMono) - | .return fvarId => - checkFVarUse fvarId - return code + | .return .. => return code | .cases c => - checkFVarUse c.discr if h : c.typeName == ``Decidable then decToMono c h else if h : c.typeName == ``Nat then diff --git a/src/Lean/Compiler/LCNF/Visibility.lean b/src/Lean/Compiler/LCNF/Visibility.lean index f354fd2f65..7d99c905b8 100644 --- a/src/Lean/Compiler/LCNF/Visibility.lean +++ b/src/Lean/Compiler/LCNF/Visibility.lean @@ -9,6 +9,8 @@ prelude public import Lean.Compiler.ImplementedByAttr import Lean.ExtraModUses import Lean.Compiler.Options +import Lean.Compiler.NoncomputableAttr +import Lean.AddDecl public section @@ -139,7 +141,7 @@ where go (origDecl decl : Decl .pure) : StateT NameSet CompilerM Unit := do for ref in collectUsedDecls code do if (← get).contains ref then continue - modify (·.insert decl.name) + modify (·.insert ref) if let some localDecl := baseExt.getState (← getEnv) |>.find? ref then -- check transitively through local decls if isPrivateName localDecl.name && (← localDecl.isTemplateLike) then diff --git a/tests/lean/run/10213.lean b/tests/lean/run/10213.lean index f743d443b8..f741000365 100644 --- a/tests/lean/run/10213.lean +++ b/tests/lean/run/10213.lean @@ -12,7 +12,7 @@ error: invalid 'csimp' theorem, only constant replacement theorems (e.g., `@f = theorem bad_csimp : @funnyChoice.{0} = @id.{0} := rfl /-- -error: Tactic `native_decide` failed. Error: failed to compile definition, compiler IR check failed at `_example._nativeDecide_1._closed_0`. Error: depends on declaration 'funnyChoice', which has no executable code; consider marking definition as 'noncomputable' +error: Tactic `native_decide` failed. Error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'funnyChoice', which is 'noncomputable' -/ #guard_msgs in example : False := by diff --git a/tests/lean/run/9806.lean b/tests/lean/run/9806.lean index 310bce36ae..5480ef10e0 100644 --- a/tests/lean/run/9806.lean +++ b/tests/lean/run/9806.lean @@ -2,4 +2,5 @@ def foo : Squash (Unit → Bool) := .mk fun _ => false def bar : Squash Bool := foo.lift fun f => .mk !f () -#eval IO.println bar.lcInv +set_option trace.Compiler.result true in +#eval unsafeCast (β := Bool) bar diff --git a/tests/lean/run/noncomputableUnused.lean b/tests/lean/run/noncomputableUnused.lean index 6d5011a0b9..9ea06a2d78 100644 --- a/tests/lean/run/noncomputableUnused.lean +++ b/tests/lean/run/noncomputableUnused.lean @@ -1,7 +1,7 @@ -@[noinline] +@[macro_inline] noncomputable def noncomp (a : Nat) : Nat := a -@[noinline] +@[macro_inline] def f (_ b : Nat) : Nat := b def g (b : Nat) := f (noncomp 0) b diff --git a/tests/lean/run/pow_exploit.lean b/tests/lean/run/pow_exploit.lean index de5d38c261..0e49125dc1 100644 --- a/tests/lean/run/pow_exploit.lean +++ b/tests/lean/run/pow_exploit.lean @@ -5,13 +5,13 @@ This was once an exploit of a bug in the Lean kernel relying on the Lean kernel falsely interpreting an expression as a Nat literal. -/ -def g.{u} : PUnit.{u} → Nat := fun _ => open Classical in if Type = Type then 0 else 0 +noncomputable def g.{u} : PUnit.{u} → Nat := fun _ => open Classical in if Type = Type then 0 else 0 -- Just writing `Nat.pow (Nat.pow 10 8) 502` would also work; `Nat.pow (Nat.pow 10 8) 503` wouldn't def T : Nat → Prop := fun x => if x = 0 then False else True -- The kernel reduces this to a number between 10^8032 and 10^8048 -def POW! := Nat.pow (g.{0} ⟨⟩) 1 +noncomputable def POW! := Nat.pow (g.{0} ⟨⟩) 1 elab "#inject_bad_proof" : command => do let decl : Lean.Declaration := .defnDecl { diff --git a/tests/lean/run/unsafeInit.lean b/tests/lean/run/unsafeInit.lean index 56e8afa975..eded02813c 100644 --- a/tests/lean/run/unsafeInit.lean +++ b/tests/lean/run/unsafeInit.lean @@ -1 +1 @@ -unsafe initialize no : Nat ← pure lcUnreachable +unsafe initialize no : Nat ← pure (unsafeCast (0 : Nat)) diff --git a/tests/lean/run/usesOfNoncomputable.lean b/tests/lean/run/usesOfNoncomputable.lean index e75cdb0530..97d46d39b9 100644 --- a/tests/lean/run/usesOfNoncomputable.lean +++ b/tests/lean/run/usesOfNoncomputable.lean @@ -46,7 +46,7 @@ universe u def Erased (α : Sort u) : Sort max 1 u := { s : α → Prop // ∃ a, (a = ·) = s } -def Erased.mk {α} (a : α) : Erased α := +@[macro_inline] def Erased.mk {α} (a : α) : Erased α := ⟨fun b => a = b, a, rfl⟩ noncomputable def Erased.out {α} : Erased α → α