crash/loop `main` with #guard_msgs

Stream: new members

[Adrien Champion]

In my 3-day lean course (first time teaching it this week, having an amazing time) I rely heavily on #guard_msgs and it seems in 4.9.0 (true for 4.8.0 also) I can use it to get things that don't compile in the binary:

inductive Fls

/-- error: failed to synthesize
  Inhabited Fls
use `set_option diagnostics true` to get diagnostic information
-/
#guard_msgs in
def illogicPanic : Fls :=
  panic! "just trust me"

def main : IO Unit := do
  println! "running"

❯ lake exe guardmsgs
INTERNAL PANIC: executed 'sorry'

[Adrien Champion]

This caused a crash, but I can also cause main to loop forever:

inductive Fls

/-- error:
fail to show termination for
  illogicRec
with errors
structural recursion cannot be used

well-founded recursion cannot be used, 'illogicRec' does not take any (non-fixed) arguments
-/
#guard_msgs in
def illogicRec : Fls :=
  illogicRec

def main : IO Unit := do
  println! "running"

❯ time lake exe guardmsgs
^C
________________________________________________________
Executed in    6.67 secs      fish           external
   usr time  111.11 millis    0.12 millis  110.99 millis
   sys time   56.48 millis    1.44 millis   55.03 millis

[Adrien Champion]

Should I go ahead and open an issue?

[Adrien Champion]

Separately, and I don't think this is related to 4.9.0, but I find it strange that error-producing definitions are added to the environment as long as you #guard_msgs the errors. For example, I would expect this not to compile (unlike my examples above which do and should compile, just not impact runtime):

inductive Fls

/-- error:
fail to show termination for
  illogicRec
with errors
structural recursion cannot be used

well-founded recursion cannot be used, 'illogicRec' does not take any (non-fixed) arguments
-/
#guard_msgs in
def illogicRec : Fls :=
  illogicRec

def main : IO Unit := do
  let _ := illogicRec
  println! "probably not reaching that"

but it does compile and (unsuprisingly) loops forever when lean exe-d

[Adrien Champion]

Obviously you can seemingly prove False

/-- error:
fail to show termination for
  illogicRec
with errors
structural recursion cannot be used

well-founded recursion cannot be used, 'illogicRec' does not take any (non-fixed) arguments
-/
#guard_msgs in
def illogicRec : False :=
  illogicRec

theorem explode : ∀ {p : Prop}, p := by
  cases illogicRec

[Bryan Gin-ge Chen]

Fortunately #print axioms explode shows that sorryAx is used.

[Adrien Champion]

Yeah, the bug I’m reporting is thankfully not a soundness bug!

[Mario Carneiro]

The nontermination issue is the same as lean4#1965: illogicRec is extracted as a closed term and evaluated at initialization time