thought i'd make a fun quiz on how the comment parser behaves - you should try and figure out whether the position directly after said token is valid Lean code, a comment, or an error - good luck :)
ps the syntax highlighter won't always help you!
--
Answer
simple - an inline comment. directly after would be a comment, or normal code after a newline.
/- -/
Answer
again, a simple multiline comment; it is closed, so after it would be normal code.
/-- -/
Answer
a doc comment - technically this is an error, as doc comments require to be just before a declaration (you can see the full list if you copy-paste this into an editor
/- /- -/
Answer
you're still in a comment! (technically you error as it's unterminated). Lean is the only language I know that supports nested multiline comments.
/- /- -/ -/
Answer
yes, this is indeed a valid nested comment! after would be normal code.
-- /-
-/
Answer
the inline comment stops the multiline from starting, so you terminate a comment that doesn't exist -- error.
/-/-/
Answer
this is normal code?? but you opened a comment twice?
/-/--/-/
Answer
this is an error! huh?!
/--/
Answer
this is still a comment / error as an unterminated multiline comment - this explains what happens in the above two. the first three characters are parsed as the docstring marker. however, the way this parsing is done doesn't backtrack - so for the case of /-/-/, the second / is actually eaten, and so the comment parser effectively sees /-|-/ (where the bar implies they're two separate tokens) and so this would be a valid comment.
/- /--/ -/
Answer
this is normal code. the inner parser for comments within comments does not eat the third character as above, because it's of course implemented separately ;)
curious what scores people get!
some further comments
There's also some special handling for /-!, module docstrings, but I don't think you can do anything that fun with them that's not covered by the existing /-- handler.
I think these last few examples lead to very odd syntax formatting in editors - not sure this "eating" behaviour has been written into these
Lean is the only language I know that supports nested multiline comments.
Rust & Haskell & Kotlin & Typst also support it.
I think most relatively-new languages support nesting, though interestingly Zig has no multiline comments at all.
hmm, that's interesting - I have been learning Rust lately for fun and not realised this! i wonder if this is due to the advent of LSP-based "comment out" features, that make it nice to not have such issues. in that case, I guess this could be a considered a bug report - "comment out" on "/-/-/" would give you a syntax error. although this is probably an unsolvable problem in general - see https://www.reddit.com/r/rust/comments/dshfiy/nested_comments_are_a_lie/. AFAIR Lean's (complicated!) string parser does not run within the comment parser.