Bug: 'unterminated comment' error when you have `/-` in a docstring

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Having /- appear in a docstring or block comment seems to be interpreted as starting a nested comment, triggering an unterminated comment error. This error confusingly is only shown at the very end of the file, even if the faulty comment is much higher up.

Furthermore, syntax highlighting in VSCode does show the comment as being properly terminated, making the error very confusing to track down.

/-- `x +/- y` -/
def test : String := "foo"

-- We get `unterminated comment` at the *end* of the file, even if we introduce other definitions after `test`

Context

Zulip post

Steps to Reproduce

1. Write a docstring that has /- in it
2. Be confused about the 'unterminated comment' error

Expected behavior: [Clear and concise description of what you expect to happen]
Having /- inside a docstring or block comment should not have any special meaning.
At the very least, the 'unterminated comment' error should be located at the faulty comment.

Actual behavior: [Clear and concise description of what actually happens]
Having /- inside a docstring or block comment seems to start a nested comment, that is expected to be terminated by a matching -/. This causes an unterminated comment error at the very end of the file

Versions

live.lean-lang.org version 4.12.0-nightly-2024-08-12

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with the minimal Lean reproducer in the issue and compare how docstrings and block comments are parsed when they contain /-. Check both the reported error location and the expected behavior that the sequence should have no special meaning inside a comment; done means the reproducer no longer reports an unterminated comment at end of file.