Lean comment syntax

Stream: lean4

[Tesla Zhang]

Is there any rational behind the multiline comment syntax /- - -/? I found it cool, but is there any particular reason to use this? Is there a problem with /* - */ and (* - *) and {- - -}?

[Mario Carneiro]

the answer to this kind of language design question is almost always "we lifted it from this other language"

[Mario Carneiro]

that said I can't think of any other language that uses /- -/, including the languages from which lean draws the most inspiration (haskell, rust, adga, coq)

[Mario Carneiro]

astoundingly, the character sequence /- cannot even be found on https://rosettacode.org/wiki/Comments

[James Gallicchio]

/me has war flashbacks from parsing /* for a subset-of-C compiler

[Sebastian Ullrich]

/- kind of looks like a compromise between Haskell's {- and the more common /*. But I don't really know.

[Henrik Böving]

The ultimate comment keyword.

[Kyle Miller]

I'm reminded of something I read in a document on the history of Haskell:

Comments provoked much discussion among the committee, and Wadler later formulated a law to describe how effort was allotted to various topics: semantics is discussed half as much as syntax, syntax is discussed half as much as lexical syntax, and lexical syntax is discussed half as much as the syntax of comments.

From this point of view, I like how unique /- ... -/ is as a sort of statement of how the specific choice doesn't really matter :smile:

[Jeremy Avigad]

IIRC, the earliest versions of Lean had --, and Leo implemented /- ... -/ for block comments during the summer of 2014 when Soonho Kong and I were at Microsoft. My vague (and possibly manufactured) memory is that it was a short conversation, just trying to find something that was easy to type and would not cause conflicts.

[Jeremy Avigad]

Given that Lean was written in C++, Leo and Soonho would have had /* ... */ and // in mind, and given that Leo was already using --, /- ... -/ would have been a natural choice.