From 44c8b0df8559728b2a1bea5e2f52f63def5dfaa0 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 29 Jun 2025 12:31:17 -0700 Subject: [PATCH] feat: `warn.sorry` option (#8662) This PR adds a `warn.sorry` option (default true) that logs the "declaration uses 'sorry'" warning when declarations contain `sorryAx`. When false, the warning is not logged. Closes #8611 (assuming that one would set `warn.sorry` as an extra flag when building). Other change: Uses `warn.sorry` when creating auxiliary declarations in `structure` elaborator, to suppress irrelevant 'sorry' warnings. We could include the sorries themselves in the message if they are labeled, letting users "go to definition" to see where the sorries are coming from. In an earlier version, added additional information to the warning when it is a synthetic sorry, since these can be caused by elaboration bugs and they can also be caused by elaboration failures in previous declarations. This idea needs some more work, so it's not included. --- src/Lean/AddDecl.lean | 12 +++++-- src/Lean/Elab/Structure.lean | 20 ++++++----- src/Lean/Util/Sorry.lean | 3 ++ .../autoImplicitForbidden.lean.expected.out | 1 - tests/lean/run/345.lean | 2 -- tests/lean/run/warnSorry.lean | 36 +++++++++++++++++++ 6 files changed, 60 insertions(+), 14 deletions(-) create mode 100644 tests/lean/run/warnSorry.lean diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean index 0c2bd1620f..d8567fbb8d 100644 --- a/src/Lean/AddDecl.lean +++ b/src/Lean/AddDecl.lean @@ -70,6 +70,13 @@ private def looksLikeRelevantTheoremProofType (type : Expr) : Bool := else type.isAppOfArity ``WellFounded 2 +/-- If `warn.sorry` is set to true, then, so long as the message log does not already have any errors, +declarations with `sorryAx` generate the "declaration uses 'sorry'" warning. -/ +register_builtin_option warn.sorry : Bool := { + defValue := true + descr := "warn about uses of `sorry` in declarations added to the environment" +} + def addDecl (decl : Declaration) : CoreM Unit := do -- register namespaces for newly added constants; this used to be done by the kernel itself -- but that is incompatible with moving it to a separate task @@ -135,8 +142,9 @@ where doAdd := do profileitM Exception "type checking" (← getOptions) do withTraceNode `Kernel (fun _ => return m!"typechecking declarations {decl.getTopLevelNames}") do - if !(← MonadLog.hasErrors) && decl.hasSorry then - logWarning <| .tagged `hasSorry m!"declaration uses 'sorry'" + if warn.sorry.get (← getOptions) then + if !(← MonadLog.hasErrors) && decl.hasSorry then + logWarning <| .tagged `hasSorry m!"declaration uses 'sorry'" try let env ← (← getEnv).addDeclAux (← getOptions) decl (← read).cancelTk? |> ofExceptKernelException diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index b49314d878..8c0c0e7521 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -1155,12 +1155,11 @@ private partial def mkFlatCtor (levelParams : List Name) (params : Array Expr) ( let ctor := getStructureCtor env structName let val ← mkFlatCtorExpr levelParams params ctor replaceIndFVars withLCtx {} {} do trace[Elab.structure] "created flat constructor:{indentExpr val}" - unless val.hasSyntheticSorry do - -- Note: flatCtorName will be private if the constructor is private - let flatCtorName := mkFlatCtorOfStructCtorName ctor.name - let valType ← replaceIndFVars (← instantiateMVars (← inferType val)) - let valType := valType.inferImplicit params.size true - addDecl <| Declaration.defnDecl (← mkDefinitionValInferrringUnsafe flatCtorName levelParams valType val .abbrev) + -- Note: flatCtorName will be private if the constructor is private + let flatCtorName := mkFlatCtorOfStructCtorName ctor.name + let valType ← replaceIndFVars (← instantiateMVars (← inferType val)) + let valType := valType.inferImplicit params.size true + addDecl <| Declaration.defnDecl (← mkDefinitionValInferrringUnsafe flatCtorName levelParams valType val .abbrev) private partial def checkResultingUniversesForFields (fieldInfos : Array StructFieldInfo) (u : Level) : TermElabM Unit := do for info in fieldInfos do @@ -1442,13 +1441,16 @@ def elabStructureCommand : InductiveElabDescr where finalizeTermElab := withLCtx lctx localInsts do checkDefaults fieldInfos prefinalize := fun levelParams params replaceIndFVars => do withLCtx lctx localInsts do - addProjections params r fieldInfos + withOptions (warn.sorry.set · false) do + addProjections params r fieldInfos registerStructure view.declName fieldInfos runStructElabM (init := state) do - mkFlatCtor levelParams params view.declName replaceIndFVars + withOptions (warn.sorry.set · false) do + mkFlatCtor levelParams params view.declName replaceIndFVars addDefaults levelParams params replaceIndFVars let parentInfos ← withLCtx lctx localInsts <| runStructElabM (init := state) do - mkRemainingProjections levelParams params view + withOptions (warn.sorry.set · false) do + mkRemainingProjections levelParams params view setStructureParents view.declName parentInfos withSaveInfoContext do -- save new env for field in view.fields do diff --git a/src/Lean/Util/Sorry.lean b/src/Lean/Util/Sorry.lean index b97e91c8fb..d7c68de456 100644 --- a/src/Lean/Util/Sorry.lean +++ b/src/Lean/Util/Sorry.lean @@ -33,6 +33,9 @@ def Expr.hasNonSyntheticSorry (e : Expr) : Bool := def Declaration.hasSorry (d : Declaration) : Bool := Id.run do d.foldExprM (fun r e => r || e.hasSorry) false +def Declaration.hasSyntheticSorry (d : Declaration) : Bool := Id.run do + d.foldExprM (fun r e => r || e.hasSyntheticSorry) false + def Declaration.hasNonSyntheticSorry (d : Declaration) : Bool := Id.run do d.foldExprM (fun r e => r || e.hasNonSyntheticSorry) false diff --git a/tests/lean/autoImplicitForbidden.lean.expected.out b/tests/lean/autoImplicitForbidden.lean.expected.out index 0d92b70454..dc28113019 100644 --- a/tests/lean/autoImplicitForbidden.lean.expected.out +++ b/tests/lean/autoImplicitForbidden.lean.expected.out @@ -1,7 +1,6 @@ autoImplicitForbidden.lean:1:8-1:9: error: unknown identifier 'f' autoImplicitForbidden.lean:6:10-6:11: error: unknown identifier 'h' autoImplicitForbidden.lean:13:24-13:27: error: unknown identifier 'Bla' -autoImplicitForbidden.lean:14:2-14:5: warning: declaration uses 'sorry' autoImplicitForbidden.lean:16:21-16:24: error: unknown identifier 'Foo' autoImplicitForbidden.lean:20:18-20:21: error: unknown identifier 'Ex2' autoImplicitForbidden.lean:28:14-28:20: error: unknown identifier 'foobar' diff --git a/tests/lean/run/345.lean b/tests/lean/run/345.lean index ea558d3aa7..a9bab2c6ef 100644 --- a/tests/lean/run/345.lean +++ b/tests/lean/run/345.lean @@ -20,8 +20,6 @@ numerals are polymorphic in Lean, but the numeral `1` cannot be used in a contex due to the absence of the instance above Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command. ---- -warning: declaration uses 'sorry' -/ #guard_msgs in structure Foo where diff --git a/tests/lean/run/warnSorry.lean b/tests/lean/run/warnSorry.lean new file mode 100644 index 0000000000..bbd9225293 --- /dev/null +++ b/tests/lean/run/warnSorry.lean @@ -0,0 +1,36 @@ +import Lean +/-! +# `warn.sorry` tests + +When `warn.sorry` is false, don't log the "declaration uses 'sorry'" warning. +-/ + +/-- warning: declaration uses 'sorry' -/ +#guard_msgs in +example : True := sorry + +#guard_msgs in +set_option warn.sorry false in +example : True := sorry + +/-! +Synthetic sorries should come with associated errors. +We want to get an error if there is a synthetic sorry with no associated error. +However: sometimes there are synthetic sorries in terms that come from other other terms +that have already been warned about. There is no way to tell if a given synthetic sorry had +been reported on previously. We want to be able to turn off the warning in this case too. +If we can tell whether sorries have already been warned about, +we could direct the user to inform us about elaboration bugs (synthetic sorries with no errors in the message log). + +So, for now we report them just like a user `sorry`. +-/ + +elab "synth_sorry" : term <= expectedType => Lean.Meta.mkSorry expectedType true + +/-- warning: declaration uses 'sorry' -/ +#guard_msgs in +example : True := synth_sorry + +#guard_msgs in +set_option warn.sorry false in +example : True := synth_sorry