suppress sorry warnings

Stream: lean4

[Siddharth Bhat]

I'd like to enable lake --wfail, but I'd like to suppress the lean feature that emits a warning when one uses a sorry.

It seems like the code in AddDecl.lean has no option to change this --- I'd be happy to implement this, but I wanted to double-check that I am not missing something!

[Andrés Goens]

I guess a workaround could be to implement your own sorry_no_warnings that just does exactly the same thing but with a different sorryAxNoWarnings?

[Andrés Goens]

(then the test of Declaration.hasSorry will fail :sweat_smile: )

[Andrés Goens]

For example:

@[extern "lean_sorry", never_extract]
axiom sorryAxNoWarning (α : Sort _) (synthetic := false) : α

macro "sorry_no_warn" : tactic => `(tactic| exact @sorryAxNoWarning _ false)

/-
declaration uses 'sorry'
-/
theorem one_plus_one : 1 + 1 = 2 := by sorry
/-
<no warning>
-/
theorem one_plus_one' : 1 + 1 = 2 := by sorry_no_warn

[Andrés Goens]

and if you #guard_msgs a #print axioms of your main theorems (which I happen to know that you do), then this should still not creep into anything unwantedly :)

[Kyle Miller]

Sometimes sorries appear inside tactics too, and if you want to handle those, you could have a command combinator that transforms the sorry warning into sorry info.

import Lean

open Lean Elab Command in
elab "yes_i_am_sorry " cmd:command : command => do
  let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
  try
    elabCommand cmd
    let msgs := (← get).messages
    let mut msgs' : MessageLog := {}
    for msg in msgs.toArray do
      if msg.severity == .warning && (← msg.data.toString) == "declaration uses 'sorry'" then
        msgs' := msgs'.add {msg with severity := .information}
      else
        msgs' := msgs'.add msg
    modify fun st => { st with messages := msgs' }
  finally
    modify fun st => { st with messages := initMsgs ++ st.messages }

/-- warning: declaration uses 'sorry' -/
#guard_msgs in
example : Nat := sorry

/-- info: declaration uses 'sorry' -/
#guard_msgs in
yes_i_am_sorry
example : Nat := sorry

[Kyle Miller]

Maybe there should be an RFC to create an option to adjust the severity level for the "declaration uses 'sorry'" message?

It seems like it would be useful to have it be 'info' for certain projects in conjunction with lake --wfail.