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

@@ -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

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

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
 

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'

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

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