From ce1213a020853663dbdc5c33b012e0581d6eacc9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 5 Jan 2014 10:32:47 -0800
Subject: [PATCH] feat(frontends/lean): use '(* ... *)' instead of '(** ...
 **)' for script code blocks

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 examples/lean/tactic1.lean         |  4 ++--
 examples/lean/tactic_in_lua.lean   |  6 +++---
 src/frontends/lean/scanner.cpp     | 26 ++++----------------------
 tests/lean/apply_tac1.lean         |  4 ++--
 tests/lean/apply_tac2.lean         |  2 +-
 tests/lean/disj1.lean              | 10 +++++-----
 tests/lean/disjcases.lean          |  2 +-
 tests/lean/find.lean               |  2 +-
 tests/lean/interactive/elab6.lean  |  4 ++--
 tests/lean/interactive/t1.lean     | 10 +++++-----
 tests/lean/interactive/t10.lean    |  4 ++--
 tests/lean/interactive/t11.lean    |  4 ++--
 tests/lean/interactive/t12.lean    |  4 ++--
 tests/lean/interactive/t13.lean    |  4 ++--
 tests/lean/interactive/t2.lean     |  6 +++---
 tests/lean/interactive/t3.lean     |  6 +++---
 tests/lean/interactive/t5.lean     |  2 +-
 tests/lean/interactive/t6.lean     |  6 +++---
 tests/lean/interactive/t7.lean     |  4 ++--
 tests/lean/interactive/t8.lean     |  2 +-
 tests/lean/interactive/t9.lean     |  6 +++---
 tests/lean/loop1.lean              |  6 +++---
 tests/lean/loop1.lean.expected.out |  2 +-
 tests/lean/loop2.lean              |  6 +++---
 tests/lean/lua1.lean               |  4 ++--
 tests/lean/lua10.lean              |  6 ++----
 tests/lean/lua11.lean              |  4 ++--
 tests/lean/lua12.lean              |  4 ++--
 tests/lean/lua13.lean              |  4 ++--
 tests/lean/lua14.lean              |  4 ++--
 tests/lean/lua15.lean              |  4 ++--
 tests/lean/lua16.lean              |  4 ++--
 tests/lean/lua17.lean              |  4 ++--
 tests/lean/lua18.lean              |  4 ++--
 tests/lean/lua2.lean               |  5 ++---
 tests/lean/lua3.lean               |  4 ++--
 tests/lean/lua4.lean               |  4 ++--
 tests/lean/lua5.lean               |  4 ++--
 tests/lean/lua6.lean               | 12 ++++++------
 tests/lean/lua7.lean               |  4 ++--
 tests/lean/lua8.lean               |  4 ++--
 tests/lean/lua9.lean               |  4 ++--
 tests/lean/mod1.lean               |  4 ++--
 tests/lean/nested.lean             |  8 ++++----
 tests/lean/norm_tac.lean           |  2 +-
 tests/lean/pr1.lean                |  2 +-
 tests/lean/slow/tactic1.lean       |  4 ++--
 tests/lean/subst2.lean             |  2 +-
 tests/lean/subst3.lean             |  2 +-
 tests/lean/tactic1.lean            |  4 ++--
 tests/lean/tactic10.lean           |  6 +++---
 tests/lean/tactic11.lean           |  2 +-
 tests/lean/tactic12.lean           |  2 +-
 tests/lean/tactic13.lean           |  6 +++---
 tests/lean/tactic14.lean           |  4 ++--
 tests/lean/tactic2.lean            |  8 ++++----
 tests/lean/tactic3.lean            |  4 ++--
 tests/lean/tactic4.lean            |  4 ++--
 tests/lean/tactic5.lean            |  4 ++--
 tests/lean/tactic6.lean            | 16 ++++++++--------
 tests/lean/tactic8.lean            |  2 +-
 tests/lean/tactic9.lean            |  2 +-
 62 files changed, 141 insertions(+), 162 deletions(-)

diff --git a/examples/lean/tactic1.lean b/examples/lean/tactic1.lean
index 7a2c02b76..4597b5735 100644
--- a/examples/lean/tactic1.lean
+++ b/examples/lean/tactic1.lean
@@ -1,7 +1,7 @@
 -- This example demonstrates how to specify a proof skeleton that contains
 -- "holes" that must be filled using user-defined tactics.
 
-(**
+(*
 -- Import useful macros for creating tactics
 import("tactic.lua")
 
@@ -10,7 +10,7 @@ auto = Repeat(OrElse(assumption_tac(), conj_tac(), conj_hyp_tac()))
 
 conj_hyp = conj_hyp_tac()
 conj     = conj_tac()
-**)
+*)
 
 -- The (by [tactic]) expression is essentially creating a "hole" and associating a "hint" to it.
 -- The "hint" is a tactic that should be used to fill the "hole".
diff --git a/examples/lean/tactic_in_lua.lean b/examples/lean/tactic_in_lua.lean
index c185fd22c..94d0fff92 100644
--- a/examples/lean/tactic_in_lua.lean
+++ b/examples/lean/tactic_in_lua.lean
@@ -1,4 +1,4 @@
-(**
+(*
  -- This example demonstrates how to create a new tactic using Lua.
  -- The basic idea is to reimplement the tactic conj_tactic in Lua.
 
@@ -62,10 +62,10 @@
  end
  conj_in_lua = tactic(conj_fn) -- Create a new tactic object using the Lua function conj_fn
  -- Now, the tactic conj_in_lua can be used when proving theorems in Lean.
-**)
+*)
 
 Theorem T (a b : Bool) : a => b => a /\ b := _.
-   (** Then(Repeat(OrElse(imp_tac(), conj_in_lua)), assumption_tac()) **)
+   (* Then(Repeat(OrElse(imp_tac(), conj_in_lua)), assumption_tac()) *)
    done
 
 -- Show proof created using our script
diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp
index 81bef0df1..22b14048e 100644
--- a/src/frontends/lean/scanner.cpp
+++ b/src/frontends/lean/scanner.cpp
@@ -380,23 +380,11 @@ scanner::token scanner::read_script_block() {
         next();
         if (c1 == '*') {
             char c2 = curr();
+            next();
             if (c2 == EOF)
                 throw_exception("unexpected end of script");
-            next();
-            if (c2 == '*') {
-                char c3 = curr();
-                if (c3 == EOF)
-                    throw_exception("unexpected end of script");
-                next();
-                if (c3 == ')') {
-                    return token::ScriptBlock;
-                } else {
-                    if (c3 == '\n')
-                        new_line();
-                    m_buffer += c1;
-                    m_buffer += c2;
-                    m_buffer += c3;
-                }
+            if (c2 == ')') {
+                return token::ScriptBlock;
             } else {
                 if (c2 == '\n')
                     new_line();
@@ -441,13 +429,7 @@ scanner::token scanner::scan() {
             next();
             if (curr() == '*') {
                 next();
-                if (curr() == '*')  {
-                    next();
-                    return read_script_block();
-                } else {
-                    throw_exception("old comment style");
-                    break;
-                }
+                return read_script_block();
             } else {
                 return token::LeftParen;
             }
diff --git a/tests/lean/apply_tac1.lean b/tests/lean/apply_tac1.lean
index f577e1a11..ffddf5796 100644
--- a/tests/lean/apply_tac1.lean
+++ b/tests/lean/apply_tac1.lean
@@ -11,9 +11,9 @@ Theorem T1 (a : Int) : (P a a) => (f a a).
       done.
 Variable b : Int
 Axiom Ax2 (x : Int) : (f x b)
-(**
+(*
 simple_tac = Repeat(OrElse(imp_tac(), assumption_tac(), apply_tac("Ax2"), apply_tac("Ax1")))
-**)
+*)
 Theorem T2 (a : Int) : (P a a) => (f a a).
      simple_tac.
      done.
diff --git a/tests/lean/apply_tac2.lean b/tests/lean/apply_tac2.lean
index 1d4beb116..7e3c36321 100644
--- a/tests/lean/apply_tac2.lean
+++ b/tests/lean/apply_tac2.lean
@@ -1,4 +1,4 @@
-(** import("tactic.lua") **)
+(* import("tactic.lua") *)
 Check @Discharge
 Theorem T (a b : Bool) : a => b => b => a.
    apply Discharge.
diff --git a/tests/lean/disj1.lean b/tests/lean/disj1.lean
index 1f1592e80..38269b38a 100644
--- a/tests/lean/disj1.lean
+++ b/tests/lean/disj1.lean
@@ -2,17 +2,17 @@ Import tactic
 
 Theorem T1 (a b : Bool) : a \/ b => b \/ a.
     apply Discharge.
-    (** disj_hyp_tac() **)
-    (** disj_tac() **)
+    (* disj_hyp_tac() *)
+    (* disj_tac() *)
     back
     exact.
-    (** disj_tac() **)
+    (* disj_tac() *)
     exact.
     done.
 
-(**
+(*
 simple_tac = Repeat(OrElse(imp_tac(), assumption_tac(), disj_hyp_tac(), disj_tac())) .. now_tac()
-**)
+*)
 
 Theorem T2 (a b : Bool) : a \/ b => b \/ a.
     simple_tac.
diff --git a/tests/lean/disjcases.lean b/tests/lean/disjcases.lean
index ece48f251..fb205065f 100644
--- a/tests/lean/disjcases.lean
+++ b/tests/lean/disjcases.lean
@@ -1,4 +1,4 @@
-(** import("tactic.lua") **)
+(* import("tactic.lua") *)
 Variables a b c : Bool
 Axiom H : a \/ b
 Theorem T (a b : Bool) : a \/ b => b \/ a.
diff --git a/tests/lean/find.lean b/tests/lean/find.lean
index 24e04611b..76f13e7cf 100644
--- a/tests/lean/find.lean
+++ b/tests/lean/find.lean
@@ -1,4 +1,4 @@
-(** import("find.lua") **)
+(* import("find.lua") *)
 Find "^.ongr"
 Find "foo"
 Find "(ab"
\ No newline at end of file
diff --git a/tests/lean/interactive/elab6.lean b/tests/lean/interactive/elab6.lean
index 339fc7e5f..ba67ad981 100644
--- a/tests/lean/interactive/elab6.lean
+++ b/tests/lean/interactive/elab6.lean
@@ -1,9 +1,9 @@
-(**
+(*
 -- The elaborator does not expand definitions marked as 'opaque'.
 -- To be able to prove the following theorem, we have to unmark the
 -- 'forall'
 local env = get_environment()
 env:set_opaque("forall", false)
-**)
+*)
 Theorem ForallIntro2 (A : (Type U)) (P : A -> Bool) (H : Pi x, P x) : forall x, P x :=
         Abst (fun x, EqTIntro (H x))
diff --git a/tests/lean/interactive/t1.lean b/tests/lean/interactive/t1.lean
index 006c81e41..acfce3f3c 100644
--- a/tests/lean/interactive/t1.lean
+++ b/tests/lean/interactive/t1.lean
@@ -1,12 +1,12 @@
 Theorem T2 (a b : Bool) : a => b => a /\ b.
 done.
 done.
-(** imp_tac() **).
+(* imp_tac() *).
 imp_tac2.
 foo.
-(** imp_tac() **).
-(** imp_tac() **).
-(** conj_tac() **).
+(* imp_tac() *).
+(* imp_tac() *).
+(* conj_tac() *).
 back.
-(** assumption_tac() **).
+(* assumption_tac() *).
 done.
diff --git a/tests/lean/interactive/t10.lean b/tests/lean/interactive/t10.lean
index 5903e27aa..4d0c578cd 100644
--- a/tests/lean/interactive/t10.lean
+++ b/tests/lean/interactive/t10.lean
@@ -1,6 +1,6 @@
-(**
+(*
 simple_tac = Repeat(OrElse(conj_hyp_tac(), conj_tac(), assumption_tac()))
-**)
+*)
 
 Theorem T2 (A B : Bool) : A /\ B => B /\ A :=
      Discharge (fun H : A /\ B,
diff --git a/tests/lean/interactive/t11.lean b/tests/lean/interactive/t11.lean
index bac07a73e..7a19b0014 100644
--- a/tests/lean/interactive/t11.lean
+++ b/tests/lean/interactive/t11.lean
@@ -1,6 +1,6 @@
-(**
+(*
 auto = Repeat(OrElse(conj_hyp_tac(), conj_tac(), assumption_tac()))
-**)
+*)
 
 Theorem T2 (A B : Bool) : A /\ B -> B /\ A :=
      fun assumption : A /\ B,
diff --git a/tests/lean/interactive/t12.lean b/tests/lean/interactive/t12.lean
index b3540b3e8..3c07928e4 100644
--- a/tests/lean/interactive/t12.lean
+++ b/tests/lean/interactive/t12.lean
@@ -1,8 +1,8 @@
-(**
+(*
 import("tactic.lua")
 -- Define a simple tactic using Lua
 auto = Repeat(OrElse(assumption_tac(), conj_tac(), conj_hyp_tac()))
-**)
+*)
 
 Theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
      fun assumption : A /\ B,
diff --git a/tests/lean/interactive/t13.lean b/tests/lean/interactive/t13.lean
index 367715bf4..96f3a7bbb 100644
--- a/tests/lean/interactive/t13.lean
+++ b/tests/lean/interactive/t13.lean
@@ -1,7 +1,7 @@
-(**
+(*
 -- Define a simple tactic using Lua
 auto = Repeat(OrElse(assumption_tac(), conj_tac(), conj_hyp_tac()))
-**)
+*)
 
 Theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
      fun assumption : A /\ B,
diff --git a/tests/lean/interactive/t2.lean b/tests/lean/interactive/t2.lean
index 6af329132..6f9b751d9 100644
--- a/tests/lean/interactive/t2.lean
+++ b/tests/lean/interactive/t2.lean
@@ -1,8 +1,8 @@
 Theorem T2 (a b : Bool) : a => b => a /\ b.
-(** imp_tac() **)
-(** imp_tac2() **)
+(* imp_tac() *)
+(* imp_tac2() *)
 foo.
-(** imp_tac() **)
+(* imp_tac() *)
 abort.
 
 Variables a b : Bool.
diff --git a/tests/lean/interactive/t3.lean b/tests/lean/interactive/t3.lean
index 7cec59e2b..ec9edaf65 100644
--- a/tests/lean/interactive/t3.lean
+++ b/tests/lean/interactive/t3.lean
@@ -1,8 +1,8 @@
-(** import("tactic.lua") **)
+(* import("tactic.lua") *)
 
 Theorem T2 (a b : Bool) : b => a \/ b.
-(** imp_tac() **).
-(** disj_tac() **).
+(* imp_tac() *).
+(* disj_tac() *).
 back.
 back.
 exact.
diff --git a/tests/lean/interactive/t5.lean b/tests/lean/interactive/t5.lean
index bbf9c24e3..961ac4778 100644
--- a/tests/lean/interactive/t5.lean
+++ b/tests/lean/interactive/t5.lean
@@ -1,4 +1,4 @@
-(** import("tactic.lua") **)
+(* import("tactic.lua") *)
 Axiom magic (a : Bool) : a.
 
 Theorem T (a : Bool) : a.
diff --git a/tests/lean/interactive/t6.lean b/tests/lean/interactive/t6.lean
index c90acf051..5d4100e9e 100644
--- a/tests/lean/interactive/t6.lean
+++ b/tests/lean/interactive/t6.lean
@@ -1,7 +1,7 @@
-(** import("tactic.lua") **)
+(* import("tactic.lua") *)
 Theorem T1 (a b : Bool) : a => b => a /\ b.
-    (** imp_tac() **).
-    (** imp_tac() **).
+    (* imp_tac() *).
+    (* imp_tac() *).
     apply Conj.
     exact.
     done.
diff --git a/tests/lean/interactive/t7.lean b/tests/lean/interactive/t7.lean
index f82882be4..24f138fd2 100644
--- a/tests/lean/interactive/t7.lean
+++ b/tests/lean/interactive/t7.lean
@@ -1,11 +1,11 @@
 Import Int.
-(** import("tactic.lua") **)
+(* import("tactic.lua") *)
 Variable q : Int -> Int -> Bool.
 Variable p : Int -> Bool.
 Axiom Ax (a b : Int) (H : q a b) : p b.
 Variable a : Int.
 Theorem T (x : Int) : (q a x) => (p x).
-    (** imp_tac() **).
+    (* imp_tac() *).
     apply (Ax a).
     exact.
     done.
diff --git a/tests/lean/interactive/t8.lean b/tests/lean/interactive/t8.lean
index 0d27fce77..c5213063a 100644
--- a/tests/lean/interactive/t8.lean
+++ b/tests/lean/interactive/t8.lean
@@ -1,4 +1,4 @@
-(** import("tactic.lua") **)
+(* import("tactic.lua") *)
 SetOption tactic::proof_state::goal_names true.
 Theorem T (a : Bool) : a => a /\ a.
    apply Discharge.
diff --git a/tests/lean/interactive/t9.lean b/tests/lean/interactive/t9.lean
index 73bc3b6bd..8cf93cc86 100644
--- a/tests/lean/interactive/t9.lean
+++ b/tests/lean/interactive/t9.lean
@@ -1,4 +1,4 @@
-(** import("tactic.lua") **)
+(* import("tactic.lua") *)
 Theorem T1 (A B : Bool) : A /\ B => B /\ A :=
      Discharge (fun H : A /\ B,
                    let main : B /\ A :=
@@ -16,9 +16,9 @@ Theorem T1 (A B : Bool) : A /\ B => B /\ A :=
   exact.
   done.
 
-(**
+(*
 simple_tac = Repeat(OrElse(conj_hyp_tac(), conj_tac(), assumption_tac()))
-**)
+*)
 
 Theorem T2 (A B : Bool) : A /\ B => B /\ A :=
      Discharge (fun H : A /\ B,
diff --git a/tests/lean/loop1.lean b/tests/lean/loop1.lean
index 6a2138d30..c70e77d64 100644
--- a/tests/lean/loop1.lean
+++ b/tests/lean/loop1.lean
@@ -1,11 +1,11 @@
-(**
+(*
  -- This example ask uses the parses to process a Lean string that
  -- contains a nested script block. The nexted script block will
  -- invoke the leanlua_state recursively. It also demonstrates that we
  -- need to use std::recursive_mutex instead of std::mutex at
  -- leanlua_state. Otherwise, it will deadlock trying to get a lock on
  -- the mutex.
- code = "(*" .. "*" .. "print('hello')" .. "*" .. "*)"
+ code = "(" .. "*" .. "print('hello')" .. "*" .. ")"
  print("executing: " .. code)
  parse_lean_cmds(code)
-**)
+*)
diff --git a/tests/lean/loop1.lean.expected.out b/tests/lean/loop1.lean.expected.out
index 5d9b8dd76..c575b1275 100644
--- a/tests/lean/loop1.lean.expected.out
+++ b/tests/lean/loop1.lean.expected.out
@@ -1,4 +1,4 @@
   Set: pp::colors
   Set: pp::unicode
-executing: (**print('hello')**)
+executing: (*print('hello')*)
 hello
diff --git a/tests/lean/loop2.lean b/tests/lean/loop2.lean
index aef38681a..96b40ac51 100644
--- a/tests/lean/loop2.lean
+++ b/tests/lean/loop2.lean
@@ -1,8 +1,8 @@
 Import Int.
 
-(**
+(*
  function add_paren(code)
-    return "(" .. "** " .. code .. " **" .. ")"
+    return "(" .. "* " .. code .. " *" .. ")"
  end
  parse_lean_cmds(add_paren([[
      local env = get_environment()
@@ -10,4 +10,4 @@ Import Int.
      print(env:find_object("x"))
   ]]))
  print("done")
-**)
+*)
diff --git a/tests/lean/lua1.lean b/tests/lean/lua1.lean
index 32d83b6de..78196067a 100644
--- a/tests/lean/lua1.lean
+++ b/tests/lean/lua1.lean
@@ -1,8 +1,8 @@
 Import Int.
 Variable x : Int
 
-(**
+(*
 print("hello world from Lua")
-**)
+*)
 
 Variable y : Int
diff --git a/tests/lean/lua10.lean b/tests/lean/lua10.lean
index 03bf5909d..ce433d55f 100644
--- a/tests/lean/lua10.lean
+++ b/tests/lean/lua10.lean
@@ -1,8 +1,7 @@
-
 Variables x1 x2 x3 : Bool
 Definition F : Bool := x1 /\ (x2 \/ x3)
 
-(**
+(*
  local env    = get_environment()
  local F      = env:find_object("F"):get_value()
  print(F)
@@ -15,5 +14,4 @@ Definition F : Bool := x1 /\ (x2 \/ x3)
 
  print(expr_size(F))
 
-**)
-
+*)
diff --git a/tests/lean/lua11.lean b/tests/lean/lua11.lean
index cced009e4..c59532d4d 100644
--- a/tests/lean/lua11.lean
+++ b/tests/lean/lua11.lean
@@ -1,5 +1,5 @@
 Import Int.
-(**
+(*
 
  local env = get_environment()
  local o1  = env:find_object(name("Int", "add"))
@@ -49,4 +49,4 @@ Import Int.
  assert(env:find_object("Refl"):is_axiom())
  assert(env:find_object(name("Int", "sub")):is_definition())
  assert(env:find_object("x"):is_var_decl())
-**)
+*)
diff --git a/tests/lean/lua12.lean b/tests/lean/lua12.lean
index 32cafd3ab..b47b5b4b9 100644
--- a/tests/lean/lua12.lean
+++ b/tests/lean/lua12.lean
@@ -1,7 +1,7 @@
 Import Int.
 Variables x y z : Int
 
-(**
+(*
  import("util.lua")
  local env  = get_environment()
  local plus = Const{"Int", "add"}
@@ -9,6 +9,6 @@ Variables x y z : Int
  local def  = plus(plus(x, y), iVal(1000))
  print(def, ":", env:type_check(def))
  env:add_definition("sum", def)
-**)
+*)
 
 Eval sum + 3
diff --git a/tests/lean/lua13.lean b/tests/lean/lua13.lean
index e292088d3..3b0c7c541 100644
--- a/tests/lean/lua13.lean
+++ b/tests/lean/lua13.lean
@@ -2,7 +2,7 @@ Import Int.
 Variables x y z : Int
 Variable f : Int -> Int -> Int
 
-(**
+(*
  local t = parse_lean("fun w, f w (f y 0)")
  print(t)
  assert(t:closed())
@@ -11,4 +11,4 @@ Variable f : Int -> Int -> Int
  assert(not b:closed())
  local env = get_environment()
  assert(env:find_object("Int"):get_name() == name("Int"))
-**)
+*)
diff --git a/tests/lean/lua14.lean b/tests/lean/lua14.lean
index bd78831d2..02f44a759 100644
--- a/tests/lean/lua14.lean
+++ b/tests/lean/lua14.lean
@@ -2,7 +2,7 @@ Import Int.
 Variables x y z : Int
 Variable f : Int -> Int -> Int
 
-(**
+(*
  local t = parse_lean("fun w, f w (f y 0)")
  print(t)
  assert(t:closed())
@@ -17,6 +17,6 @@ Variable f : Int -> Int -> Int
     Variable g : Int -> Int
  ]])
 
-**)
+*)
 
 Check g (f x 10)
diff --git a/tests/lean/lua15.lean b/tests/lean/lua15.lean
index cca862bc0..940d6daa1 100644
--- a/tests/lean/lua15.lean
+++ b/tests/lean/lua15.lean
@@ -2,7 +2,7 @@ Import Int.
 Variables i j : Int
 Variable p : Bool
 
-(**
+(*
  local env = get_environment()
  ok, ex = pcall(
     function()
@@ -12,4 +12,4 @@ Variable p : Bool
  assert(is_exception(ex))
  print(ex:what())
  ex:rethrow()
-**)
+*)
diff --git a/tests/lean/lua16.lean b/tests/lean/lua16.lean
index 0c73c9593..bca712a20 100644
--- a/tests/lean/lua16.lean
+++ b/tests/lean/lua16.lean
@@ -1,8 +1,8 @@
 Import Int.
 Variables a b : Int
 
-(**
+(*
   local ios = io_state()
   ios:print(parse_lean("a + b"))
   print(parse_lean("a + b"))
-**)
\ No newline at end of file
+*)
\ No newline at end of file
diff --git a/tests/lean/lua17.lean b/tests/lean/lua17.lean
index ffb03e5bc..c5c0348f8 100644
--- a/tests/lean/lua17.lean
+++ b/tests/lean/lua17.lean
@@ -1,7 +1,7 @@
 Import Int.
 Variables a b : Int
 Show Options
-(**
+(*
   local ios = io_state()
 
   print(get_options())
@@ -9,6 +9,6 @@ Show Options
   ios:print(parse_lean("a + b"))
   print(parse_lean("fun x, a + x"))
   print(get_options())
-**)
+*)
 Show Options
 Show Environment 2
\ No newline at end of file
diff --git a/tests/lean/lua18.lean b/tests/lean/lua18.lean
index eb817b1df..675a868dc 100644
--- a/tests/lean/lua18.lean
+++ b/tests/lean/lua18.lean
@@ -1,5 +1,5 @@
 Import Int.
-(**
+(*
 macro("MyMacro", { macro_arg.Expr, macro_arg.Comma, macro_arg.Expr },
      function (env, e1, e2)
         return Const({"Int", "add"})(e1, e2)
@@ -16,7 +16,7 @@ macro("Sum", { macro_arg.Exprs },
          end
          return r
       end)
-**)
+*)
 
 Show (MyMacro 10, 20) + 20
 Show (Sum)
diff --git a/tests/lean/lua2.lean b/tests/lean/lua2.lean
index faae048f8..7bd2c49be 100644
--- a/tests/lean/lua2.lean
+++ b/tests/lean/lua2.lean
@@ -1,6 +1,6 @@
 Variable x : Bool
 
-(**
+(*
  a = {}
  print("hello world")
  print ("ok")
@@ -9,7 +9,6 @@ Variable x : Bool
     y = 20
  }
  rint ("ok")
-**)
+*)
 
 Variable y : Bool
-
diff --git a/tests/lean/lua3.lean b/tests/lean/lua3.lean
index c0081937f..52c8a28ae 100644
--- a/tests/lean/lua3.lean
+++ b/tests/lean/lua3.lean
@@ -1,6 +1,6 @@
 Import Int.
 Variable x : Int
 
-(**
+(*
 dofile("script.lua")
-**)
\ No newline at end of file
+*)
\ No newline at end of file
diff --git a/tests/lean/lua4.lean b/tests/lean/lua4.lean
index c007ea733..460f64b16 100644
--- a/tests/lean/lua4.lean
+++ b/tests/lean/lua4.lean
@@ -1,7 +1,7 @@
 Import Int.
 Variable x : Int
 
-(**
+(*
 -- Add a variable to the environment using Lua
 -- The type of the new variable is equal to the type
 -- of x
@@ -9,6 +9,6 @@ local env = get_environment()
 typeofx = env:type_check(Const("x"))
 print("type of x is " .. tostring(typeofx))
 env:add_var("y", typeofx)
-**)
+*)
 
 Check x + y
diff --git a/tests/lean/lua5.lean b/tests/lean/lua5.lean
index f3522d1bf..fa8a9183c 100644
--- a/tests/lean/lua5.lean
+++ b/tests/lean/lua5.lean
@@ -1,7 +1,7 @@
 Import Int.
 Variable x : Int
 
-(**
+(*
 local N   = 100
 local env = get_environment()
 -- Create N variables with the same type of x
@@ -9,7 +9,7 @@ typeofx = env:type_check(Const("x"))
 for i = 1, N do
     env:add_var("y_" .. i, typeofx)
 end
-**)
+*)
 
 Show Environment 101
 Check x + y_1 + y_2
\ No newline at end of file
diff --git a/tests/lean/lua6.lean b/tests/lean/lua6.lean
index 7c2101405..862102086 100644
--- a/tests/lean/lua6.lean
+++ b/tests/lean/lua6.lean
@@ -1,20 +1,20 @@
 Import Int.
 Variable x : Int
 SetOption pp::notation false
-(**
+(*
 print(get_options())
-**)
+*)
 Check x + 2
-(**
+(*
 o = get_options()
 o = o:update(name('lean', 'pp', 'notation'), true)
 set_options(o)
 print(get_options())
-**)
+*)
 Check x + 2
-(**
+(*
 set_option(name('lean', 'pp', 'notation'), false)
 print(get_options())
-**)
+*)
 Variable y : Int
 Check x + y
diff --git a/tests/lean/lua7.lean b/tests/lean/lua7.lean
index c2fbf7ee0..964ecabdb 100644
--- a/tests/lean/lua7.lean
+++ b/tests/lean/lua7.lean
@@ -1,6 +1,6 @@
-(**
+(*
 x = Const("x")
 y = Const("y")
 N = Const("N")
 print(fun({{x, N}, {y, N}}, x))
-**)
\ No newline at end of file
+*)
\ No newline at end of file
diff --git a/tests/lean/lua8.lean b/tests/lean/lua8.lean
index d4c62e1fc..e804dee0c 100644
--- a/tests/lean/lua8.lean
+++ b/tests/lean/lua8.lean
@@ -1,7 +1,7 @@
 Import Int.
 Variable x : Int
 
-(**
+(*
 local env = get_environment()
 ty_x = env:type_check(Const("x"))
 c = context()
@@ -12,4 +12,4 @@ o = env:find_object("x")
 print(o)
 o = env:find_object("y")
 print(o)
-**)
\ No newline at end of file
+*)
\ No newline at end of file
diff --git a/tests/lean/lua9.lean b/tests/lean/lua9.lean
index f49a6506b..e800ad12d 100644
--- a/tests/lean/lua9.lean
+++ b/tests/lean/lua9.lean
@@ -1,7 +1,7 @@
 Import Int.
 Variable x : Bool
 
-(**
+(*
  import("util.lua")
  local env    = get_environment()
  local Int    = Const("Int")
@@ -31,7 +31,7 @@ Variable x : Bool
  print(s)
  print(env:type_check(s))
  env:add_definition("sum1", s)
-**)
+*)
 
 Show Environment 1
 Eval sum1
diff --git a/tests/lean/mod1.lean b/tests/lean/mod1.lean
index 4d9ef7ea6..f493c63d6 100644
--- a/tests/lean/mod1.lean
+++ b/tests/lean/mod1.lean
@@ -1,11 +1,11 @@
 Import cast
 Import cast
-(**
+(*
    local env = environment() -- create new environment
    parse_lean_cmds([[
       Import cast
       Import cast
       Check @cast
    ]], env)
-**)
+*)
 Check @cast
\ No newline at end of file
diff --git a/tests/lean/nested.lean b/tests/lean/nested.lean
index 580621243..ff3c5f9b5 100644
--- a/tests/lean/nested.lean
+++ b/tests/lean/nested.lean
@@ -1,4 +1,4 @@
-(**
+(*
 cmd_macro("Simple",
           { macro_arg.String },
           function (env, str)
@@ -9,12 +9,12 @@ cmd_macro("Simple",
 parse_lean_cmds([[
    Simple "foo"
 ]])
-**)
+*)
 
 Simple "testing"
 
-(**
+(*
 parse_lean_cmds([[
    Simple "bla"
 ]])
-**)
+*)
diff --git a/tests/lean/norm_tac.lean b/tests/lean/norm_tac.lean
index b8a233bdd..7d27b2d04 100644
--- a/tests/lean/norm_tac.lean
+++ b/tests/lean/norm_tac.lean
@@ -10,4 +10,4 @@ Definition D := read V1 1 (by trivial)
 Show Environment 1
 Variable b : Bool
 Definition a := b
-Theorem T : b => a := (by (** imp_tac() .. normalize_tac() .. assumption_tac() **))
+Theorem T : b => a := (by (* imp_tac() .. normalize_tac() .. assumption_tac() *))
diff --git a/tests/lean/pr1.lean b/tests/lean/pr1.lean
index 7699472e6..3cb6f8ffa 100644
--- a/tests/lean/pr1.lean
+++ b/tests/lean/pr1.lean
@@ -1,4 +1,4 @@
-(** import("tactic.lua") **)
+(* import("tactic.lua") *)
 Theorem T (C A B : Bool) : C -> A -> B -> A.
    exact.
    done.
diff --git a/tests/lean/slow/tactic1.lean b/tests/lean/slow/tactic1.lean
index cc9e52368..1c61a87db 100644
--- a/tests/lean/slow/tactic1.lean
+++ b/tests/lean/slow/tactic1.lean
@@ -2,7 +2,7 @@ Import Int.
 Definition double {A : Type} (f : A -> A) : A -> A := fun x, f (f x).
 Definition big {A : Type} (f : A -> A) : A -> A := (double (double (double (double (double (double (double f))))))).
 
-(**
+(*
 
  -- Tactic for trying to prove goal using Reflexivity, Congruence and available assumptions
 local congr_tac = Repeat(OrElse(apply_tac("Refl"), apply_tac("Congr"), assumption_tac()))
@@ -18,7 +18,7 @@ eager_tac = Then(-- unfold homogeneous equality
 lazy_tac = OrElse(Then(Try(unfold_tac("eq")), congr_tac, now_tac()),
                   eager_tac)
 
-**)
+*)
 
 Theorem T1 (a b : Int) (f : Int -> Int) (H : a = b) : (big f a) = (big f b).
         eager_tac.
diff --git a/tests/lean/subst2.lean b/tests/lean/subst2.lean
index c688d42f9..32d6b0efd 100644
--- a/tests/lean/subst2.lean
+++ b/tests/lean/subst2.lean
@@ -1,4 +1,4 @@
-(** import("tactic.lua") **)
+(* import("tactic.lua") *)
 Theorem T (A : Type) (p : A -> Bool) (f : A -> A -> A) : forall x y z, p (f x x) => x = y => x = z => p (f y z).
    apply ForallIntro.
    beta.
diff --git a/tests/lean/subst3.lean b/tests/lean/subst3.lean
index 0745cb99a..682694278 100644
--- a/tests/lean/subst3.lean
+++ b/tests/lean/subst3.lean
@@ -1,4 +1,4 @@
-(** import("macros.lua") **)
+(* import("macros.lua") *)
 
 Theorem T (A : Type) (p : A -> Bool) (f : A -> A -> A) : forall x y z, p (f x x) => x = y => x = z => p (f y z) :=
    For x y z, Assume (H1 : p (f x x)) (H2 : x = y) (H3 : x = z),
diff --git a/tests/lean/tactic1.lean b/tests/lean/tactic1.lean
index e6fc74e16..df496ea0d 100644
--- a/tests/lean/tactic1.lean
+++ b/tests/lean/tactic1.lean
@@ -1,11 +1,11 @@
 Variables p q r : Bool
 
-(**
+(*
  local env = get_environment()
  local conjecture = parse_lean('p => q => p && q')
  local tac = Repeat(conj_tac() ^ imp_tac() ^ assumption_tac())
  local proof = tac:solve(env, context(), conjecture)
  env:add_theorem("T1", conjecture, proof)
-**)
+*)
 
 Show Environment 1.
diff --git a/tests/lean/tactic10.lean b/tests/lean/tactic10.lean
index 546d1ef9b..2b9ac1e34 100644
--- a/tests/lean/tactic10.lean
+++ b/tests/lean/tactic10.lean
@@ -1,4 +1,4 @@
-(** import("tactic.lua") **)
+(* import("tactic.lua") *)
 Definition f(a : Bool) : Bool := not a.
 Definition g(a b : Bool) : Bool := a \/ b.
 
@@ -11,9 +11,9 @@ Theorem T1 (a b : Bool) : (g a b) => (f b) => a := _.
      absurd
      done.
 
-(**
+(*
 simple_tac   = Repeat(unfold_tac()) .. Repeat(OrElse(imp_tac(), conj_hyp_tac(), assumption_tac(), absurd_tac(), conj_hyp_tac(), disj_hyp_tac()))
-**)
+*)
 
 Definition h(a b : Bool) : Bool := g a b.
 
diff --git a/tests/lean/tactic11.lean b/tests/lean/tactic11.lean
index 5bd937c1d..87a3996f5 100644
--- a/tests/lean/tactic11.lean
+++ b/tests/lean/tactic11.lean
@@ -1,4 +1,4 @@
-(** import("tactic.lua") **)
+(* import("tactic.lua") *)
 Theorem T (a b : Bool) : ((fun x, x /\ b) a) => ((fun x, x) a) := _ .
    beta.
    apply Discharge.
diff --git a/tests/lean/tactic12.lean b/tests/lean/tactic12.lean
index fc1193e06..172b67fd4 100644
--- a/tests/lean/tactic12.lean
+++ b/tests/lean/tactic12.lean
@@ -1,4 +1,4 @@
-(** import("tactic.lua") **)
+(* import("tactic.lua") *)
 Theorem T (a b : Bool) : ((fun x, x /\ b) a) => ((fun x, x) a).
    beta.
    apply Discharge.
diff --git a/tests/lean/tactic13.lean b/tests/lean/tactic13.lean
index 2e58d3736..57b048f2d 100644
--- a/tests/lean/tactic13.lean
+++ b/tests/lean/tactic13.lean
@@ -1,15 +1,15 @@
 Import Int.
-(** import("tactic.lua") **)
+(* import("tactic.lua") *)
 Variable f : Int -> Int -> Int
 
-(**
+(*
 refl_tac           = apply_tac("Refl")
 congr_tac          = apply_tac("Congr")
 symm_tac           = apply_tac("Symm")
 trans_tac          = apply_tac("Trans")
 unfold_homo_eq_tac = unfold_tac("eq")
 auto = unfold_homo_eq_tac .. Repeat(OrElse(refl_tac, congr_tac, assumption_tac(), Then(symm_tac, assumption_tac(), now_tac())))
-**)
+*)
 
 Theorem T1 (a b c : Int) (H1 : a = b) (H2 : a = c) : (f (f a a) b) = (f (f b c) a).
    auto.
diff --git a/tests/lean/tactic14.lean b/tests/lean/tactic14.lean
index ac5df00ba..3dc86521c 100644
--- a/tests/lean/tactic14.lean
+++ b/tests/lean/tactic14.lean
@@ -1,10 +1,10 @@
 Import Int.
-(**
+(*
 
 -- Tactic for trying to prove goal using Reflexivity, Congruence and available assumptions
 congr_tac = Try(unfold_tac("eq")) .. Repeat(OrElse(apply_tac("Refl"), apply_tac("Congr"), assumption_tac()))
 
-**)
+*)
 
 Theorem T1 (a b : Int) (f : Int -> Int) : a = b -> (f (f a)) = (f (f b)) :=
    fun assumption : a = b,
diff --git a/tests/lean/tactic2.lean b/tests/lean/tactic2.lean
index 42bc9900f..605cc94ef 100644
--- a/tests/lean/tactic2.lean
+++ b/tests/lean/tactic2.lean
@@ -1,4 +1,4 @@
-(** import("tactic.lua") **)
+(* import("tactic.lua") *)
 Variables p q r : Bool
 
 Theorem T1 : p => q => p /\ q :=
@@ -13,9 +13,9 @@ Theorem T1 : p => q => p /\ q :=
     exact -- solve second metavar
     done
 
-(**
+(*
 simple_tac = Repeat(imp_tac() ^ conj_tac() ^ assumption_tac())
-**)
+*)
 
 Theorem T2 : p => q => p /\ q /\ p := _.
     simple_tac
@@ -24,7 +24,7 @@ Theorem T2 : p => q => p /\ q /\ p := _.
 Show Environment 1
 
 Theorem T3 : p => p /\ q => r => q /\ r /\ p := _.
-    (** Repeat(OrElse(imp_tac(), conj_tac(), conj_hyp_tac(), assumption_tac())) **)
+    (* Repeat(OrElse(imp_tac(), conj_tac(), conj_hyp_tac(), assumption_tac())) *)
     done
 
 -- Display proof term generated by previous tac
diff --git a/tests/lean/tactic3.lean b/tests/lean/tactic3.lean
index e60202029..09728c16d 100644
--- a/tests/lean/tactic3.lean
+++ b/tests/lean/tactic3.lean
@@ -1,8 +1,8 @@
-(** import("tactic.lua") **)
+(* import("tactic.lua") *)
 Variables p q r : Bool
 
 Theorem T1 : p => p /\ q => r => q /\ r /\ p := _.
-    (** Repeat(OrElse(imp_tac(), conj_tac(), conj_hyp_tac(), assumption_tac())) **)
+    (* Repeat(OrElse(imp_tac(), conj_tac(), conj_hyp_tac(), assumption_tac())) *)
     done
 
 -- Display proof term generated by previous tactic
diff --git a/tests/lean/tactic4.lean b/tests/lean/tactic4.lean
index 6181fcfb1..018034fb6 100644
--- a/tests/lean/tactic4.lean
+++ b/tests/lean/tactic4.lean
@@ -1,6 +1,6 @@
-(**
+(*
 simple_tac = Repeat(OrElse(imp_tac(), conj_tac())) .. assumption_tac()
-**)
+*)
 
 Theorem T4 (a b : Bool) : a => b => a /\ b := _.
         simple_tac
diff --git a/tests/lean/tactic5.lean b/tests/lean/tactic5.lean
index 0141839a3..5f8d8886d 100644
--- a/tests/lean/tactic5.lean
+++ b/tests/lean/tactic5.lean
@@ -1,6 +1,6 @@
-(**
+(*
 simple_tac = Repeat(OrElse(imp_tac(), conj_tac())) .. assumption_tac()
-**)
+*)
 
 Theorem T4 (a b : Bool) : a => b => a /\ b /\ a := _.
         simple_tac
diff --git a/tests/lean/tactic6.lean b/tests/lean/tactic6.lean
index 355f586c4..1a2ce641f 100644
--- a/tests/lean/tactic6.lean
+++ b/tests/lean/tactic6.lean
@@ -1,10 +1,10 @@
-(** import("tactic.lua") **)
+(* import("tactic.lua") *)
 Theorem T (a b c : Bool): a => b /\ c => c /\ a /\ b := _.
    apply Discharge
    apply Discharge
    conj_hyp
    apply Conj
-   (** Focus(Then(show_tac(), conj_tac(), show_tac(), assumption_tac()), 2) **)
+   (* Focus(Then(show_tac(), conj_tac(), show_tac(), assumption_tac()), 2) *)
    exact
    done
 
@@ -13,10 +13,10 @@ Theorem T2 (a b c : Bool): a => b /\ c => c /\ a /\ b := _.
    apply Discharge
    conj_hyp
    apply Conj
-   (** show_tac() **)
-   (** Focus(Then(show_tac(), conj_tac(), Focus(assumption_tac(), 1)), 2) **)
-   (** show_tac() **)
-   (** Focus(assumption_tac(), 1) **)
-   (** show_tac() **)
-   (** Focus(assumption_tac(), 1) **)
+   (* show_tac() *)
+   (* Focus(Then(show_tac(), conj_tac(), Focus(assumption_tac(), 1)), 2) *)
+   (* show_tac() *)
+   (* Focus(assumption_tac(), 1) *)
+   (* show_tac() *)
+   (* Focus(assumption_tac(), 1) *)
    done
\ No newline at end of file
diff --git a/tests/lean/tactic8.lean b/tests/lean/tactic8.lean
index 784c1671d..d4379d4fc 100644
--- a/tests/lean/tactic8.lean
+++ b/tests/lean/tactic8.lean
@@ -1,4 +1,4 @@
-(** import("tactic.lua") **)
+(* import("tactic.lua") *)
 Theorem T (a b : Bool) : a \/ b => (not b) => a := _.
      apply Discharge
      apply Discharge
diff --git a/tests/lean/tactic9.lean b/tests/lean/tactic9.lean
index fd59f1aab..abb0ffedf 100644
--- a/tests/lean/tactic9.lean
+++ b/tests/lean/tactic9.lean
@@ -1,4 +1,4 @@
-(** import("tactic.lua") **)
+(* import("tactic.lua") *)
 Definition f(a : Bool) : Bool := not a.
 
 Theorem T (a b : Bool) : a \/ b => (f b) => a := _.