Open gebner opened 3 years ago
Thanks! You're going to find quite a few issues, there still are some very basic things wrong with the parser -- including ones that mean it takes ridiculous amounts of time to generate at the minute... My best idea so far was just trying to get to the point where I parse advent-of-lean4
or now mathlib4
without errors, which I'm still not there yet on.
But please do file as many of these as you find!
I did not expect a complete grammar---the lean.nvim readme was pretty clear that this is experimental.
Errors are fine as well; the grammar in the vscode extension also has lots of corner cases that are incorrect. I don't mind if a keyword is not highlighted. It's only an issue if an occurrence of some unsupported syntax causes the rest of the file to be highlighted incorrectly (as in this issue and #4).
I looked at this quickly, it's a bit annoying at the minute -- this is being misparsed as
open <identifier>
<another identifier>
which is why the formatting is off, and to fix that I think is because I have precedence for application totally wrong, but it will take a bit of refactoring to fix.
The other ones I haven't looked at yet but may be easier.
This is indeed super ambiguous, the following is a valid three-line long open statement:
namespace something end something -- we need to define the namespace first
open Lean
something -- still part of the open statement :raised_eyebrow:
Yeah :/