Open PatrickMassot opened 2 years ago
At least here, whatever is involved here seems to depend both on the sequence of characters you type as well as how fast you type them.
Recording:
https://github.com/leanprover/lean4/assets/329822/00a18ce3-0c7c-4388-b5e8-dd9124147793
Prerequisites
Description
I get an unexpected error "unexpected end of input" when creating a comment at the end of a file. It goes away only if Lean is forced to recompile the file.
Steps to Reproduce
#check Nat
/- comment -/
Expected behavior: [What you expect to happen] Getting a comment.
Actual behavior: [What actually happens] Get an error "unexpected end of input"
Reproduces how often: [What percentage of the time does it reproduce?] Always
Versions
You can get this information from copy and pasting the output of
lean --version
, please include the OS and what version of the OS you're running.Lean (version 4.0.0-nightly-2022-07-18, commit 5083d47e4d3c, Release)
on Linux