No diagnostic about use of `sorry`

Stream: lean4

[Eric Wieser]

The following code lets me prove False without warning about the use of sorry:

theorem not_at_all_apologetic {α : Prop} : α := by
  sorry
where
  foo : True := by
    rw [garbage]

example : False := not_at_all_apologetic

[Damiano Testa]

It's almost as though lean is telling you that there is so much junk in what you wrote, that it is pretending it is not even lean syntax.

[Joachim Breitner]

Maybe the code that handles such possible mutual groups does not go through

def addDecl (decl : Declaration) : CoreM Unit := do
  profileitM Exception "type checking" (← getOptions) do
    withTraceNode `Kernel (fun _ => return m!"typechecking declaration") do
      if !(← MonadLog.hasErrors) && decl.hasSorry then
        logWarning "declaration uses 'sorry'"
      match (← getEnv).addDecl (← getOptions) decl (← read).cancelTk? with
      | .ok    env => setEnv env
      | .error ex  => throwKernelException ex

or the decl.hasSorry somehow fails, or the MonadLog has errors, but they are not shown for some reason. Sounds like it's worth reporting as a lean4 bug.