feat(frontends/lean): change multicomment to /- ... -/

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

library/standard/hott/path.lean

@@ -466,14 +466,14 @@ induction_on p idp
 -- Transporting in particular fibrations
 -- -------------------------------------
 
-(-- From the Coq HoTT library:
+/-
+From the Coq HoTT library:
 
 One frequently needs lemmas showing that transport in a certain dependent type is equal to some
 more explicitly defined operation, defined according to the structure of that dependent type.
 For most dependent types, we prove these lemmas in the appropriate file in the types/
 subdirectory.  Here we consider only the most basic cases.
-
---)
+-/
 
 -- Transporting in a constant fibration.
 definition transport_const {A B : Type} {x1 x2 : A} (p : x1 ≈ x2) (y : B) :
@@ -640,7 +640,7 @@ definition apD02_pp {A} (B : A → Type) (f : Π x:A, B x) {x y : A}
 induction_on r1 (take r2, induction_on r2 (induction_on p1 idp)) r2
 
 
-(-- From the Coq version:
+/- From the Coq version:
 
 -- ** Tactics, hints, and aliases
 
@@ -691,4 +691,4 @@ Hint Rewrite
 Ltac hott_simpl :=
   autorewrite with paths in * |- * ; auto with path_hints.
 
---)
+-/

src/frontends/lean/scanner.cpp

@@ -228,8 +228,8 @@ bool scanner::consume(char const * str, char const * error_msg) {
     }
 }
 
-static char const * g_begin_comment_block = "(--";
-static char const * g_end_comment_block = "--)";
+static char const * g_begin_comment_block = "/-";
+static char const * g_end_comment_block = "-/";
 
 void scanner::read_comment_block() {
     static char const * end_error_msg = "unexpected end of comment block";
@@ -422,7 +422,7 @@ auto scanner::read_key_cmd_id() -> token_kind {
 
 static name g_begin_script_tk("(*");
 static name g_begin_comment_tk("--");
-static name g_begin_comment_block_tk("(--");
+static name g_begin_comment_block_tk("/-");
 
 auto scanner::scan(environment const & env) -> token_kind {
     m_tokens = &get_token_table(env);

src/frontends/lean/token_table.cpp

@@ -70,7 +70,7 @@ token_table init_token_table() {
          {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
          {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec}, {"Type'", g_max_prec},
          {"|", 0}, {"!", 0}, {"with", 0}, {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0},
-         {"(*", 0}, {"(--", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec}, {"including", 0}, {"sorry", g_max_prec},
+         {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec}, {"including", 0}, {"sorry", g_max_prec},
          {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}};
 
     char const * commands[] = {"theorem", "axiom", "variable", "definition", "coercion",

src/tests/frontends/lean/scanner.cpp

@@ -143,8 +143,8 @@ static void tst2() {
     env = add_token(env, "+", 0);
     check("x+y", {tk::Identifier, tk::Keyword, tk::Identifier}, env);
     check("-- testing", {});
-    check("(-- testing --)", {});
-    check("(-- (-- testing\n --) --)", {});
+    check("/- testing -/", {});
+    check("/- /- testing\n -/ -/", {});
     check(" 2.31  ", {tk::Decimal});
     check("2.31", {tk::Decimal});
     check(" 333 22", {tk::Numeral, tk::Numeral});

tests/lean/slow/path_groupoids.lean

@@ -460,14 +460,14 @@ induction_on p idp
 -- Transporting in particular fibrations
 -- -------------------------------------
 
-(-- From the Coq HoTT library:
+/-
+From the Coq HoTT library:
 
 One frequently needs lemmas showing that transport in a certain dependent type is equal to some
 more explicitly defined operation, defined according to the structure of that dependent type.
 For most dependent types, we prove these lemmas in the appropriate file in the types/
 subdirectory.  Here we consider only the most basic cases.
-
---)
+-/
 
 -- Transporting in a constant fibration.
 definition transport_const {A B : Type} {x1 x2 : A} (p : x1 ≈ x2) (y : B) :