Panics in syntax accessors

Stream: lean4 dev

[Gabriel Ebner]

fix: panic when Syntax.missing

I got a panic error message today in VS Code because of this function.
It is weird because, as far as I can tell, this function is only used by
the register_simp_attr macro, and this macro was not being used in
the files I was editing.
I think the fix is resonable for a Syntax.missing case.

@Leonardo de Moura Thanks for spotting this issue, I completely forgot that .missing is a valid syntax for every TSyntax k.

Unfortunately, the same issue is present in a lot of other functions. Just one example:

macro "same" &"issue" n:num : term =>
  open Lean in pure (quote n.getNat : Term)

#check same issue -- PANIC

Personally I'm not a fan of panic! at all, since it completely defies the principle of "well-typed programs don't crash". Particularly with Syntax, we often get temporarily wrong syntax trees during editing, and the most common ways to access syntax (pattern matching, indexing) fail safely. So my preference would be to remove the panic cases for these syntax accessors entirely, and return a default value instead (0, empty string, etc.). Any thoughts?

[Leonardo de Moura]

Yes, panic!s behavior is a recurrent issue.

Personally I'm not a fan of panic! at all, since it completely defies the principle of "well-typed programs don't crash".

Note that the program only crashes if we set the environment variable LEAN_ABORT_ON_PANIC.

So my preference would be to remove the panic cases for these syntax accessors entirely, and return a default value instead (0, empty string, etc.). Any thoughts?

I am fine with this solution, but in the past others complained about silently returning the default value in similar situations.

[Gabriel Ebner]

but in the past others complained about silently returning the default value in similar situations.

I think this is more of an issue with List.head! [], where [] is both a perfectly common value for List Nat, and a value which should be handled in a separate case. With Syntax.NumLit, the only common value is ⟨.atom ..⟩; the ⟨.missing⟩ value should not be treated differently since it only comes from parsing errors.

Note that some Syntax functions are already non-panicking. For example, Syntax.getIdent or TSyntax.getIdent return the anonymous name if the argument is not an identifier. stx[i] returns .missing if the argument is not a node, etc.

[Gabriel Ebner]

Note that the program only crashes if we set the environment variable LEAN_ABORT_ON_PANIC.

Okay, I was stretching the term "crash" here a bit. For the user, it doesn't matter too much if the program terminates from an abort, from a segfault, or prints a pages-long scary warning message. All of these are issues that need to be fixed.

[Leonardo de Moura]

Note that some Syntax functions are already non-panicking. For example, Syntax.getIdent or TSyntax.getIdent return the anonymous name if the argument is not an identifier. stx[i] returns .missing if the argument is not a node, etc.

I am fine with not panicking in Syntax functions.