Wrong "unexpected end of input"

[PatrickMassot]

trafficstars

Prerequisites

• [X] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

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

1. In VSCode (not sure if emacs would do the same), create a file containing #check Nat
2. Create a comment at the end of the file by typing /- 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