LSP crash

Stream: lean4

[James Sully]

is the vscode extension repo the correct place to report a language server crash?

[James Sully]

I have

def northernTrees : Array String :=
  #["sloe", "birch", "elm", "oak"]

#eval northernTrees[6]

Which works fine (reports a type error), but when I change the index to 5, it crashes

[Scott Morrison]

Curiously either an index of 4 or 5 causes this behaviour. It's not the VSCode extension's fault, though. When you run this file on the command line is fails silently (i.e. doesn't print a PANIC or index out of bounds error).

[Scott Morrison]

Could you open an issue on the lean4 repository?

[Damiano Testa]

I think that what you observed is not expected. However, if you use !, then you get what I would consider the expected behaviour:

#eval northernTrees[6]!

works, panicking starting from 4.

[James Sully]

Curiously either an index of 4 or 5 causes this behaviour

Yeah, I noticed that. I was trying to play around with arrays of different lengths to figure out the rules, but I couldn't get it to happen consistently even with the same combinations of array length and index.

[James Sully]

Could you open an issue on the lean4 repository?

Done!