diff --git a/doc/lean/expr.md b/doc/lean/expr.md
index ad0621666b..eb0e3e731b 100644
--- a/doc/lean/expr.md
+++ b/doc/lean/expr.md
@@ -89,16 +89,16 @@ infix 50 = : eq
 ```
 
 The curly braces indicate that the first argument of `eq` is implicit. The symbol `=` is just a syntax sugar for `eq`.
-In the following example, we use the `setoption` command to force Lean to display implicit arguments and
+In the following example, we use the `set::option` command to force Lean to display implicit arguments and
 disable notation when pretty printing expressions.
 
 ```lean
-setoption pp::implicit true
-setoption pp::notation false
+set::option pp::implicit true
+set::option pp::notation false
 check 1 = 2
 
 -- restore default configuration
-setoption pp::implicit false
-setoption pp::notation true
+set::option pp::implicit false
+set::option pp::notation true
 check 1 = 2
 ```
diff --git a/examples/lean/even.lean b/examples/lean/even.lean
index 2496d8258e..c1127afdc1 100644
--- a/examples/lean/even.lean
+++ b/examples/lean/even.lean
@@ -63,7 +63,7 @@ print environment 2.
 
 -- By default, Lean does not display implicit arguments.
 -- The following command will force it to display them.
-setoption pp::implicit true.
+set::option pp::implicit true.
 
 print environment 2.
 
diff --git a/examples/lean/ex1.lean b/examples/lean/ex1.lean
index d600ae7599..8d4182bbb4 100644
--- a/examples/lean/ex1.lean
+++ b/examples/lean/ex1.lean
@@ -30,6 +30,6 @@ theorem T2 : (h a (h a b)) = (h a (h c e)) :=
 print environment 2
 
 -- print implicit arguments
-setoption lean::pp::implicit true
-setoption pp::width 150
+set::option lean::pp::implicit true
+set::option pp::width 150
 print environment 2
diff --git a/examples/lean/ex2.lean b/examples/lean/ex2.lean
index c813ea2cdb..cabb952256 100644
--- a/examples/lean/ex2.lean
+++ b/examples/lean/ex2.lean
@@ -6,7 +6,7 @@ theorem simple (p q r : Bool) : (p ⇒ q) ∧ (q ⇒ r) ⇒ p ⇒ r
             P_qr := and::elimr H_pq_qr
         in P_qr ◂ (P_pq ◂ H_p)
 
-setoption pp::implicit true.
+set::option pp::implicit true.
 print environment 1.
 
 theorem simple2 (a b c : Bool) : (a ⇒ b ⇒ c) ⇒ (a ⇒ b) ⇒ a ⇒ c
diff --git a/src/builtin/Int.lean b/src/builtin/Int.lean
index fe7bcc9c6a..b5575081cb 100644
--- a/src/builtin/Int.lean
+++ b/src/builtin/Int.lean
@@ -46,14 +46,14 @@ infix 50 | : divides
 definition abs (a : Int) : Int := if (0 ≤ a) a (- a)
 notation 55 | _ | : abs
 
-setopaque sub true
-setopaque neg true
-setopaque mod true
-setopaque divides true
-setopaque abs true
-setopaque ge true
-setopaque lt true
-setopaque gt true
+set::opaque sub true
+set::opaque neg true
+set::opaque mod true
+set::opaque divides true
+set::opaque abs true
+set::opaque ge true
+set::opaque lt true
+set::opaque gt true
 end
 
 namespace Nat
@@ -63,6 +63,6 @@ infixl 65 - : sub
 definition neg (a : Nat) : Int := - (nat_to_int a)
 notation 75 - _ : neg
 
-setopaque sub true
-setopaque neg true
+set::opaque sub true
+set::opaque neg true
 end
\ No newline at end of file
diff --git a/src/builtin/Nat.lean b/src/builtin/Nat.lean
index 38d4f9c867..872b4ecf43 100644
--- a/src/builtin/Nat.lean
+++ b/src/builtin/Nat.lean
@@ -243,8 +243,8 @@ theorem le::antisym {a b : Nat} (H1 : a ≤ b) (H2 : b ≤ a) : a = b
           ...  =  a  + w1 : { symm L2 }
           ...  =  b       : Hw1
 
-setopaque ge true
-setopaque lt true
-setopaque gt true
-setopaque id true
+set::opaque ge true
+set::opaque lt true
+set::opaque gt true
+set::opaque id true
 end
\ No newline at end of file
diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean
index 5c44301dc9..1c24edd68c 100644
--- a/src/builtin/kernel.lean
+++ b/src/builtin/kernel.lean
@@ -240,11 +240,11 @@ theorem exists::intro {A : TypeU} {P : A → Bool} (a : A) (H : P a) : Exists A
 -- them as opaque Opaque definitions improve performance, and
 -- effectiveness of Lean's elaborator
 
-setopaque implies true
-setopaque not     true
-setopaque or      true
-setopaque and     true
-setopaque forall  true
+set::opaque implies true
+set::opaque not     true
+set::opaque or      true
+set::opaque and     true
+set::opaque forall  true
 
 theorem or::comm (a b : Bool) : (a ∨ b) == (b ∨ a)
 := iff::intro (assume H, or::elim H (λ H1, or::intror b H1) (λ H2, or::introl H2 a))
@@ -393,4 +393,4 @@ theorem exists::unfold {A : TypeU} (P : A → Bool) (a : A) : (∃ x : A, P x) =
 := iff::intro (assume H : (∃ x : A, P x), exists::unfold1 a H)
               (assume H : (P a ∨ (∃ x : A, x ≠ a ∧ P x)), exists::unfold2 a H)
 
-setopaque exists true
+set::opaque exists true
diff --git a/src/frontends/lean/parser_cmds.cpp b/src/frontends/lean/parser_cmds.cpp
index d6ad01622d..90fa18c350 100644
--- a/src/frontends/lean/parser_cmds.cpp
+++ b/src/frontends/lean/parser_cmds.cpp
@@ -37,8 +37,8 @@ static name g_infix_kwd("infix");
 static name g_infixl_kwd("infixl");
 static name g_infixr_kwd("infixr");
 static name g_notation_kwd("notation");
-static name g_set_option_kwd("setoption");
-static name g_set_opaque_kwd("setopaque");
+static name g_set_option_kwd("set", "option");
+static name g_set_opaque_kwd("set", "opaque");
 static name g_options_kwd("options");
 static name g_env_kwd("environment");
 static name g_import_kwd("import");
@@ -596,28 +596,29 @@ void parser_imp::parse_help() {
         }
     } else {
         regular(m_io_state) << "Available commands:" << endl
-                            << "  alias [id] : [expr]    define an alias for the given expression" << endl
-                            << "  axiom [id] : [type]    assert/postulate a new axiom" << endl
-                            << "  check [expr]           type check the given expression" << endl
+                            << "  alias [id] : [expr]      define an alias for the given expression" << endl
+                            << "  axiom [id] : [type]      assert/postulate a new axiom" << endl
+                            << "  check [expr]             type check the given expression" << endl
                             << "  definition [id] : [type] := [expr]   define a new element" << endl
-                            << "  end                    end the current scope/namespace" << endl
-                            << "  eval [expr]            evaluate the given expression" << endl
-                            << "  exit                   exit" << endl
-                            << "  help                   display this message" << endl
-                            << "  help options           display available options" << endl
-                            << "  help notation          describe commands for defining infix, mixfix, postfix operators" << endl
-                            << "  import [string]        load the given file" << endl
-                            << "  pop::scope             discard the current scope" << endl
-                            << "  print [expr]           pretty print the given expression" << endl
-                            << "  print Options          print current the set of assigned options" << endl
-                            << "  print [string]         print the given string" << endl
-                            << "  print Environment      print objects in the environment, if [Num] provided, then show only the last [Num] objects" << endl
-                            << "  print Environment [num] show the last num objects in the environment" << endl
-                            << "  scope                  create a scope" << endl
-                            << "  setoption [id] [value] set option [id] with value [value]" << endl
-                            << "  theorem [id] : [type] := [expr]      define a new theorem" << endl
-                            << "  variable [id] : [type] declare/postulate an element of the given type" << endl
-                            << "  universe [id] [level]  declare a new universe variable that is >= the given level" << endl;
+                            << "  end                      end the current scope/namespace" << endl
+                            << "  eval [expr]              evaluate the given expression" << endl
+                            << "  exit                     exit" << endl
+                            << "  help                     display this message" << endl
+                            << "  help options             display available options" << endl
+                            << "  help notation            describe commands for defining infix, mixfix, postfix operators" << endl
+                            << "  import [string]          load the given file" << endl
+                            << "  pop::scope               discard the current scope" << endl
+                            << "  print [expr]             pretty print the given expression" << endl
+                            << "  print Options            print current the set of assigned options" << endl
+                            << "  print [string]           print the given string" << endl
+                            << "  print Environment        print objects in the environment, if [Num] provided, then show only the last [Num] objects" << endl
+                            << "  print Environment [num]  show the last num objects in the environment" << endl
+                            << "  scope                    create a scope" << endl
+                            << "  set::option [id] [value] set option [id] with value [value]" << endl
+                            << "  set::opaque [id] [bool]  set the given definition as opaque/transparent" << endl
+                            << "  theorem [id] : [type] := [expr]    define a new theorem" << endl
+                            << "  variable [id] : [type]   declare/postulate an element of the given type" << endl
+                            << "  universe [id] [level]    declare a new universe variable that is >= the given level" << endl;
 #if !defined(LEAN_WINDOWS)
         regular(m_io_state) << "Type Ctrl-D to exit" << endl;
 #endif
diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index ae6e26694b..a8b9f8c7d6 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -33,7 +33,7 @@ class set_opaque_command : public neutral_object_cell {
 public:
     set_opaque_command(name const & n, bool opaque):m_obj_name(n), m_opaque(opaque) {}
     virtual ~set_opaque_command() {}
-    virtual char const * keyword() const { return "setopaque"; }
+    virtual char const * keyword() const { return "set::opaque"; }
     virtual void write(serializer & s) const { s << "Opa" << m_obj_name << m_opaque; }
     name const & get_obj_name() const { return m_obj_name; }
     bool get_flag() const { return m_opaque; }
diff --git a/src/tests/frontends/lean/parser.cpp b/src/tests/frontends/lean/parser.cpp
index b628fe7ee1..75071c9450 100644
--- a/src/tests/frontends/lean/parser.cpp
+++ b/src/tests/frontends/lean/parser.cpp
@@ -94,11 +94,11 @@ static void tst3() {
     parse_error(env, ios, "check U");
     parse(env, ios, "variable h : Real -> Real -> Real. notation 10 [ _ ; _ ] : h. check [ 10.3 ; 20.1 ].");
     parse_error(env, ios, "variable h : Real -> Real -> Real. notation 10 [ _ ; _ ] : h. check [ 10.3 | 20.1 ].");
-    parse_error(env, ios, "setoption pp::indent true");
-    parse(env, ios, "setoption pp::indent 10");
-    parse_error(env, ios, "setoption pp::colors foo");
-    parse_error(env, ios, "setoption pp::colors \"foo\"");
-    parse(env, ios, "setoption pp::colors true");
+    parse_error(env, ios, "set::option pp::indent true");
+    parse(env, ios, "set::option pp::indent 10");
+    parse_error(env, ios, "set::option pp::colors foo");
+    parse_error(env, ios, "set::option pp::colors \"foo\"");
+    parse(env, ios, "set::option pp::colors true");
     parse_error(env, ios, "notation 10 : Int::add");
     parse_error(env, ios, "notation 10 _ : Int::add");
     parse(env, ios, "notation 10 _ ++ _ : Int::add. eval 10 ++ 20.");
diff --git a/tests/lean/abst.lean b/tests/lean/abst.lean
index 7712c8b52e..f6ef3b1891 100644
--- a/tests/lean/abst.lean
+++ b/tests/lean/abst.lean
@@ -2,5 +2,5 @@ import Int.
 axiom PlusComm(a b : Int) : a + b == b + a.
 variable a : Int.
 check (abst (fun x : Int, (PlusComm a x))).
-setoption pp::implicit true.
+set::option pp::implicit true.
 check (abst (fun x : Int, (PlusComm a x))).
diff --git a/tests/lean/alias2.lean b/tests/lean/alias2.lean
index 008602499d..d625f6f6cd 100644
--- a/tests/lean/alias2.lean
+++ b/tests/lean/alias2.lean
@@ -3,14 +3,14 @@ scope
   alias ℕℕ : Natural.
   variable x : Natural.
   print environment 1.
-  setoption pp::unicode false.
+  set::option pp::unicode false.
   print environment 1.
-  setoption pp::unicode true.
+  set::option pp::unicode true.
   print environment 1.
   alias NN : Natural.
   print environment 2.
   alias ℕℕℕ : Natural.
   print environment 3.
-  setoption pp::unicode false.
+  set::option pp::unicode false.
   print environment 3.
 pop::scope
\ No newline at end of file
diff --git a/tests/lean/arith1.lean b/tests/lean/arith1.lean
index c9b844932e..fbb92abceb 100644
--- a/tests/lean/arith1.lean
+++ b/tests/lean/arith1.lean
@@ -10,9 +10,9 @@ variable n : Nat
 variable m : Nat
 print n + m
 print n + x + m
-setoption lean::pp::coercion true
+set::option lean::pp::coercion true
 print n + x + m + 10
 print x + n + m + 10
 print n + m + 10 + x
-setoption lean::pp::notation false
+set::option lean::pp::notation false
 print n + m + 10 + x
diff --git a/tests/lean/arith2.lean b/tests/lean/arith2.lean
index d2adaa403c..668e812d81 100644
--- a/tests/lean/arith2.lean
+++ b/tests/lean/arith2.lean
@@ -7,7 +7,7 @@ variable x : Real
 variable i : Int
 variable n : Nat
 print x + i + 1 + n
-setoption lean::pp::coercion true
+set::option lean::pp::coercion true
 print x + i + 1 + n
 print x * i + x
 print x - i + x - x >= 0
diff --git a/tests/lean/arith3.lean b/tests/lean/arith3.lean
index 898bc60f62..3721ab4996 100644
--- a/tests/lean/arith3.lean
+++ b/tests/lean/arith3.lean
@@ -4,7 +4,7 @@ eval 8 div 4
 eval 7 div 3
 eval 7 mod 3
 print -8 mod 3
-setoption lean::pp::notation false
+set::option lean::pp::notation false
 print -8 mod 3
 eval -8 mod 3
 eval (-8 div 3)*3 + (-8 mod 3)
\ No newline at end of file
diff --git a/tests/lean/arith6.lean b/tests/lean/arith6.lean
index 5f5ced6e81..0b09644a64 100644
--- a/tests/lean/arith6.lean
+++ b/tests/lean/arith6.lean
@@ -1,5 +1,5 @@
 import Int.
-setoption pp::unicode false
+set::option pp::unicode false
 print 3 | 6
 eval 3 | 6
 eval 3 | 7
@@ -9,5 +9,5 @@ variable x : Int
 eval x | 3
 eval 3 | x
 eval 6 | 3
-setoption pp::notation false
+set::option pp::notation false
 print 3 | x
\ No newline at end of file
diff --git a/tests/lean/arith7.lean b/tests/lean/arith7.lean
index e1f7493163..bc3c370952 100644
--- a/tests/lean/arith7.lean
+++ b/tests/lean/arith7.lean
@@ -11,6 +11,6 @@ eval |x + 1| > 0
 variable y : Int
 eval |x + y|
 print |x + y| > x
-setoption pp::notation false
+set::option pp::notation false
 print |x + y| > x
 print |x + y| + |y + x| > x
\ No newline at end of file
diff --git a/tests/lean/bad10.lean b/tests/lean/bad10.lean
index 3861cee142..0a8028457e 100644
--- a/tests/lean/bad10.lean
+++ b/tests/lean/bad10.lean
@@ -1,5 +1,5 @@
-setoption pp::implicit true.
-setoption pp::colors   false.
+set::option pp::implicit true.
+set::option pp::colors   false.
 variable N : Type.
 
 definition T (a : N) (f : _ -> _) (H : f a == a) : f (f _) == f _ :=
diff --git a/tests/lean/bad2.lean b/tests/lean/bad2.lean
index 754f798f4f..e3f0c580b3 100644
--- a/tests/lean/bad2.lean
+++ b/tests/lean/bad2.lean
@@ -8,6 +8,6 @@ definition n3 : list Int := cons 10 nil
 definition n4 : list Int := nil
 definition n5 : _ := cons 10 nil
 
-setoption pp::coercion true
-setoption pp::implicit true
+set::option pp::coercion true
+set::option pp::implicit true
 print environment 1.
\ No newline at end of file
diff --git a/tests/lean/bad9.lean b/tests/lean/bad9.lean
index 9c25a26e88..e60bd69cdd 100644
--- a/tests/lean/bad9.lean
+++ b/tests/lean/bad9.lean
@@ -1,5 +1,5 @@
-setoption pp::implicit true.
-setoption pp::colors   false.
+set::option pp::implicit true.
+set::option pp::colors   false.
 variable N : Type.
 
 check
diff --git a/tests/lean/cast2.lean b/tests/lean/cast2.lean
index 3eefa3d495..80d8b60ad7 100644
--- a/tests/lean/cast2.lean
+++ b/tests/lean/cast2.lean
@@ -7,6 +7,6 @@ axiom H : (A -> B) = (A' -> B')
 variable a : A
 check dominj H
 theorem BeqB' : B = B' := raninj H a
-setoption pp::implicit true
+set::option pp::implicit true
 print dominj H
 print raninj H a
diff --git a/tests/lean/cast4.lean b/tests/lean/cast4.lean
index ce6035a786..c92bedf887 100644
--- a/tests/lean/cast4.lean
+++ b/tests/lean/cast4.lean
@@ -1,5 +1,5 @@
 import cast
-setoption pp::colors false
+set::option pp::colors false
 
 check fun (A A': TypeM)
           (B   : A -> TypeM)
diff --git a/tests/lean/coercion2.lean b/tests/lean/coercion2.lean
index 44e2443d6f..0af2afa342 100644
--- a/tests/lean/coercion2.lean
+++ b/tests/lean/coercion2.lean
@@ -8,25 +8,25 @@ print g a a
 variable b : R
 print g a b
 print g b a
-setoption lean::pp::coercion true
+set::option lean::pp::coercion true
 print g a a
 print g a b
 print g b a
-setoption lean::pp::coercion false
+set::option lean::pp::coercion false
 variable S : Type
 variable s : S
 variable r : S
 variable h : S -> S -> S
 infixl 10 ++ : g
 infixl 10 ++ : h
-setoption lean::pp::notation false
+set::option lean::pp::notation false
 print a ++ b ++ a
 print r ++ s ++ r
 check a ++ b ++ a
 check r ++ s ++ r
-setoption lean::pp::coercion true
+set::option lean::pp::coercion true
 print a ++ b ++ a
 print r ++ s ++ r
-setoption lean::pp::notation true
+set::option lean::pp::notation true
 print a ++ b ++ a
 print r ++ s ++ r
diff --git a/tests/lean/config.lean b/tests/lean/config.lean
index 9386ad12fd..f5980302c4 100644
--- a/tests/lean/config.lean
+++ b/tests/lean/config.lean
@@ -1,3 +1,3 @@
--- setoption default configuration for tests
-setoption pp::colors  false
-setoption pp::unicode true
+-- set::option default configuration for tests
+set::option pp::colors  false
+set::option pp::unicode true
diff --git a/tests/lean/elab4.lean b/tests/lean/elab4.lean
index 4af3e58b09..ae6fabcc78 100644
--- a/tests/lean/elab4.lean
+++ b/tests/lean/elab4.lean
@@ -8,5 +8,5 @@ variable R {A A' : Type} {B : A -> Type} {B' : A' -> Type} (H : (Pi x : A, B x)
 theorem R2 : Pi (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : A1), B1 = B2 :=
     fun A1 A2 B1 B2 H a, R H a
 
-setoption pp::implicit true
+set::option pp::implicit true
 print environment 7.
diff --git a/tests/lean/elab5.lean b/tests/lean/elab5.lean
index 1af323df9f..0768e3d408 100644
--- a/tests/lean/elab5.lean
+++ b/tests/lean/elab5.lean
@@ -8,5 +8,5 @@ variable R {A A' : Type} {B : A -> Type} {B' : A' -> Type} (H : (Pi x : A, B x)
 theorem R2 : Pi (A1 A2 B1 B2 : Type), ((A1 -> B1) = (A2 -> B2)) -> A1 -> (B1 = B2) :=
     fun A1 A2 B1 B2 H a, R H a
 
-setoption pp::implicit true
+set::option pp::implicit true
 print environment 7.
diff --git a/tests/lean/elab7.lean b/tests/lean/elab7.lean
index b68550b085..7a4281881d 100644
--- a/tests/lean/elab7.lean
+++ b/tests/lean/elab7.lean
@@ -17,5 +17,5 @@ theorem T2 : (fun (x1 : A) (x2 : B), F1 x1 x2) = F2 := abst (fun a, (abst (fun b
 theorem T3 : F1 = (fun (x1 : A) (x2 : B), F2 x1 x2) := abst (fun a, (abst (fun b, H a b)))
 theorem T4 : (fun (x1 : A) (x2 : B), F1 x1 x2) = (fun (x1 : A) (x2 : B), F2 x1 x2) := abst (fun a, (abst (fun b, H a b)))
 print environment 4
-setoption pp::implicit true
+set::option pp::implicit true
 print environment 4
\ No newline at end of file
diff --git a/tests/lean/eq1.lean b/tests/lean/eq1.lean
index cd740150af..4f543346ef 100644
--- a/tests/lean/eq1.lean
+++ b/tests/lean/eq1.lean
@@ -1,5 +1,5 @@
 import Int.
 variable i : Int
 check i = 0
-setoption pp::coercion true
+set::option pp::coercion true
 check i = 0
diff --git a/tests/lean/eq2.lean b/tests/lean/eq2.lean
index 87527eff2a..cc1671051e 100644
--- a/tests/lean/eq2.lean
+++ b/tests/lean/eq2.lean
@@ -4,5 +4,5 @@ variable nil  {A : Type} : List A
 variable cons {A : Type} (head : A) (tail : List A) : List A
 variable l : List Int.
 check l = nil.
-setoption pp::implicit true
+set::option pp::implicit true
 check l = nil.
diff --git a/tests/lean/eq3.lean b/tests/lean/eq3.lean
index 925df762f2..9cdb0e399f 100644
--- a/tests/lean/eq3.lean
+++ b/tests/lean/eq3.lean
@@ -6,5 +6,5 @@ variable v3 : Vector (0 + n)
 axiom H1 : v1 == v2
 axiom H2 : v2 == v3
 check htrans H1 H2
-setoption pp::implicit true
+set::option pp::implicit true
 check htrans H1 H2
diff --git a/tests/lean/ex2.lean b/tests/lean/ex2.lean
index c6c71c8ada..87662216eb 100644
--- a/tests/lean/ex2.lean
+++ b/tests/lean/ex2.lean
@@ -1,8 +1,8 @@
 -- comment
 print true
-setoption lean::pp::notation false
+set::option lean::pp::notation false
 print true && false
-setoption pp::unicode false
+set::option pp::unicode false
 print true && false
 variable a : Bool
 variable a : Bool
@@ -12,7 +12,7 @@ variable A : Type
 check a && A
 print environment 1
 print options
-setoption lean::p::notation true
-setoption lean::pp::notation 10
-setoption lean::pp::notation true
+set::option lean::p::notation true
+set::option lean::pp::notation 10
+set::option lean::pp::notation true
 print a && b
diff --git a/tests/lean/ex2.lean.expected.out b/tests/lean/ex2.lean.expected.out
index 6725809189..0aaf996b19 100644
--- a/tests/lean/ex2.lean.expected.out
+++ b/tests/lean/ex2.lean.expected.out
@@ -19,7 +19,7 @@ Arguments types:
     A : Type
 variable A : Type
 (lean::pp::notation := false, pp::unicode := false, pp::colors := false)
-Error (line: 15, pos: 10) unknown option 'lean::p::notation', type 'Help Options.' for list of available options
-Error (line: 16, pos: 29) invalid option value, given option is not an integer
+Error (line: 15, pos: 12) unknown option 'lean::p::notation', type 'Help Options.' for list of available options
+Error (line: 16, pos: 31) invalid option value, given option is not an integer
   Set: lean::pp::notation
 a /\ b
diff --git a/tests/lean/ex3.lean b/tests/lean/ex3.lean
index 3670ddb924..726240b8a5 100644
--- a/tests/lean/ex3.lean
+++ b/tests/lean/ex3.lean
@@ -5,5 +5,5 @@ variable a : T
 check myeq _ true a
 variable myeq2 {A:Type} (a b : A) : Bool
 infix 50 === : myeq2
-setoption lean::pp::implicit true
+set::option lean::pp::implicit true
 check true === a
\ No newline at end of file
diff --git a/tests/lean/exists3.lean b/tests/lean/exists3.lean
index d9c2f324d6..77c98c6457 100644
--- a/tests/lean/exists3.lean
+++ b/tests/lean/exists3.lean
@@ -1,7 +1,7 @@
 import Int.
 variable P : Int -> Int -> Bool
 
-setopaque exists false.
+set::opaque exists false.
 
 theorem T1 (R1 : not (exists x y, P x y)) : forall x y, not (P x y) :=
          forall::intro (fun a,
diff --git a/tests/lean/exists7.lean b/tests/lean/exists7.lean
index d901ef092f..9de3711cb9 100644
--- a/tests/lean/exists7.lean
+++ b/tests/lean/exists7.lean
@@ -1,11 +1,11 @@
-setoption pp::colors false
+set::option pp::colors false
 variable N : Type
 variables a b c : N
 variables P : N -> N -> N -> Bool
 
-setopaque forall  false.
-setopaque exists  false.
-setopaque not     false.
+set::opaque forall  false.
+set::opaque exists  false.
+set::opaque not     false.
 
 theorem T1 (f : N -> N) (H : P (f a) b (f (f c))) : exists x y z, P x y z := exists::intro _ (exists::intro _ (exists::intro _ H))
 
diff --git a/tests/lean/implicit1.lean b/tests/lean/implicit1.lean
index 4ae6c4b186..a105760461 100644
--- a/tests/lean/implicit1.lean
+++ b/tests/lean/implicit1.lean
@@ -6,7 +6,7 @@ print forall a b, f a b > 0
 variable g : Int -> Real -> Int
 print forall a b, g a b > 0
 print forall a b, g a (f a b) > 0
-setoption pp::coercion true
+set::option pp::coercion true
 print forall a b, g a (f a b) > 0
 print fun a, a + 1
 print fun a b, a + b
diff --git a/tests/lean/implicit2.lean b/tests/lean/implicit2.lean
index 2cc06e19d9..0f071888bd 100644
--- a/tests/lean/implicit2.lean
+++ b/tests/lean/implicit2.lean
@@ -8,6 +8,6 @@ check g 10 20 true
 check let r : Real -> Real -> Real := g 10 20
       in r
 check g 10
-setoption pp::implicit true
+set::option pp::implicit true
 check let r : Real -> Real -> Real := g 10 20
       in r
diff --git a/tests/lean/implicit3.lean b/tests/lean/implicit3.lean
index 636b8caee6..b6e79879bd 100644
--- a/tests/lean/implicit3.lean
+++ b/tests/lean/implicit3.lean
@@ -5,7 +5,7 @@ variable f : Int -> Int -> Int
 variable g : Int -> Int -> Int -> Int
 notation 10 _ ++ _ : f
 notation 10 _ ++ _ : g
-setoption pp::implicit true
-setoption pp::notation false
+set::option pp::implicit true
+set::option pp::notation false
 print (10 ++ 20)
 print (10 ++ 20) 10
diff --git a/tests/lean/implicit6.lean b/tests/lean/implicit6.lean
index 6f760811e1..6ebf3bee87 100644
--- a/tests/lean/implicit6.lean
+++ b/tests/lean/implicit6.lean
@@ -4,8 +4,8 @@ infixl 65 + : f
 print true + false
 print 10 + 20
 print 10 + (- 20)
-setoption pp::notation false
-setoption pp::coercion true
+set::option pp::notation false
+set::option pp::coercion true
 print true + false
 print 10 + 20
 print 10 + (- 20)
diff --git a/tests/lean/implicit7.lean b/tests/lean/implicit7.lean
index 7f23fb8057..d38a2a179a 100644
--- a/tests/lean/implicit7.lean
+++ b/tests/lean/implicit7.lean
@@ -4,9 +4,9 @@ notation 100 _ ; _ ; _ : f
 notation 100 _ ; _ ; _ : g
 check 10 ; true ; false
 check 10 ; 10 ; true
-setoption pp::notation false
+set::option pp::notation false
 check 10 ; true ; false
 check 10 ; 10 ; true
-setoption pp::implicit true
+set::option pp::implicit true
 check 10 ; true ; false
 check 10 ; 10 ; true
diff --git a/tests/lean/interactive/config.lean b/tests/lean/interactive/config.lean
index 9386ad12fd..f5980302c4 100644
--- a/tests/lean/interactive/config.lean
+++ b/tests/lean/interactive/config.lean
@@ -1,3 +1,3 @@
--- setoption default configuration for tests
-setoption pp::colors  false
-setoption pp::unicode true
+-- set::option default configuration for tests
+set::option pp::colors  false
+set::option pp::unicode true
diff --git a/tests/lean/interactive/t8.lean b/tests/lean/interactive/t8.lean
index 97bc0c79bd..185a8125f7 100644
--- a/tests/lean/interactive/t8.lean
+++ b/tests/lean/interactive/t8.lean
@@ -1,5 +1,5 @@
 (* import("tactic.lua") *)
-setoption tactic::proof_state::goal_names true.
+set::option tactic::proof_state::goal_names true.
 theorem T (a : Bool) : a => a /\ a.
    apply discharge.
    apply and::intro.
diff --git a/tests/lean/let1.lean b/tests/lean/let1.lean
index 12318bd3c1..8ad56a11d6 100644
--- a/tests/lean/let1.lean
+++ b/tests/lean/let1.lean
@@ -6,5 +6,5 @@ check let a : Nat := 10 in a + 1
 eval let a : Nat := 20 in a + 10
 eval let a := 20 in a + 10
 check let a : Int := 20 in a + 10
-setoption pp::coercion true
+set::option pp::coercion true
 print let a : Int := 20 in a + 10
diff --git a/tests/lean/let3.lean b/tests/lean/let3.lean
index cda1b254bd..5f9c77ae3c 100644
--- a/tests/lean/let3.lean
+++ b/tests/lean/let3.lean
@@ -2,8 +2,8 @@ import Int.
 
 variable magic : Pi (H : Bool), H
 
-setoption pp::notation false
-setoption pp::coercion true
+set::option pp::notation false
+set::option pp::coercion true
 print let a : Int   := 1,
          H : a > 0 := magic (a > 0)
      in H
\ No newline at end of file
diff --git a/tests/lean/let4.lean b/tests/lean/let4.lean
index 74e6729131..8ce9363df9 100644
--- a/tests/lean/let4.lean
+++ b/tests/lean/let4.lean
@@ -41,7 +41,7 @@ let a  := 10,
     v2 : vector Int  a := v1
 in v2
 
-setoption pp::coercion true
+set::option pp::coercion true
 
 print
 let a  := 10,
diff --git a/tests/lean/lua6.lean b/tests/lean/lua6.lean
index 25a9dca8b0..3745198afc 100644
--- a/tests/lean/lua6.lean
+++ b/tests/lean/lua6.lean
@@ -1,6 +1,6 @@
 import Int.
 variable x : Int
-setoption pp::notation false
+set::option pp::notation false
 (*
 print(get_options())
 *)
diff --git a/tests/lean/norm_bug1.lean b/tests/lean/norm_bug1.lean
index 36a183450d..202cb80c2d 100644
--- a/tests/lean/norm_bug1.lean
+++ b/tests/lean/norm_bug1.lean
@@ -1,5 +1,5 @@
 import cast
-setoption pp::colors false
+set::option pp::colors false
 
 check fun (A A': TypeM)
           (a   : A)
diff --git a/tests/lean/norm_tac.lean b/tests/lean/norm_tac.lean
index 5a58582302..219aa95abb 100644
--- a/tests/lean/norm_tac.lean
+++ b/tests/lean/norm_tac.lean
@@ -1,8 +1,8 @@
 import Int
 import tactic
-setoption pp::implicit true
-setoption pp::coercion true
-setoption pp::notation false
+set::option pp::implicit true
+set::option pp::coercion true
+set::option pp::notation false
 variable vector (A : Type) (sz : Nat) : Type
 variable read {A : Type} {sz : Nat} (v : vector A sz) (i : Nat) (H : i < sz) : A
 variable V1 : vector Int 10
diff --git a/tests/lean/overload1.lean b/tests/lean/overload1.lean
index d5842d480f..1374ad19f4 100644
--- a/tests/lean/overload1.lean
+++ b/tests/lean/overload1.lean
@@ -4,7 +4,7 @@ variable g : N -> N -> N
 infixl 10 ++ : f
 infixl 10 ++ : g
 print true ++ false ++ true
-setoption lean::pp::notation false
+set::option lean::pp::notation false
 print true ++ false ++ true
 variable a : N
 variable b : N
diff --git a/tests/lean/overload2.lean b/tests/lean/overload2.lean
index cec84b0b26..d2c699feb8 100644
--- a/tests/lean/overload2.lean
+++ b/tests/lean/overload2.lean
@@ -10,8 +10,8 @@ coercion t2r
 variable f : T -> R -> T
 variable a : T
 variable b : R
-setoption lean::pp::coercion true
-setoption lean::pp::notation false
+set::option lean::pp::coercion true
+set::option lean::pp::notation false
 print f a b
 print f b a
 variable g : R -> T -> R
diff --git a/tests/lean/showenv.l b/tests/lean/showenv.l
index 033b270786..c18bd02aac 100644
--- a/tests/lean/showenv.l
+++ b/tests/lean/showenv.l
@@ -1,3 +1,3 @@
-setoption pp::colors  false
+set::option pp::colors  false
 print "===BEGIN ENVIRONMENT==="
 print environment
diff --git a/tests/lean/slow/config.lean b/tests/lean/slow/config.lean
index 9386ad12fd..f5980302c4 100644
--- a/tests/lean/slow/config.lean
+++ b/tests/lean/slow/config.lean
@@ -1,3 +1,3 @@
--- setoption default configuration for tests
-setoption pp::colors  false
-setoption pp::unicode true
+-- set::option default configuration for tests
+set::option pp::colors  false
+set::option pp::unicode true
diff --git a/tests/lean/slow/deep.lean b/tests/lean/slow/deep.lean
index 78d9b08547..3e03171b36 100644
--- a/tests/lean/slow/deep.lean
+++ b/tests/lean/slow/deep.lean
@@ -3,6 +3,6 @@ definition f1 (f : Int -> Int) (x : Int) : Int := f (f (f (f x)))
 definition f2 (f : Int -> Int) (x : Int) : Int := f1 (f1 (f1 (f1 f))) x
 definition f3 (f : Int -> Int) (x : Int) : Int := f1 (f2 (f2 f)) x
 variable f : Int -> Int.
-setoption pp::width 80.
-setoption lean::pp::max_depth 2000.
+set::option pp::width 80.
+set::option lean::pp::max_depth 2000.
 eval f3 f 0.
\ No newline at end of file
diff --git a/tests/lean/subst.lean b/tests/lean/subst.lean
index a8e9a9cf78..ac2c17e8dc 100644
--- a/tests/lean/subst.lean
+++ b/tests/lean/subst.lean
@@ -4,7 +4,7 @@ variable n : Nat
 axiom H1 : a + a + a = 10
 axiom H2 : a = n
 theorem T : a + n + a = 10 := subst H1 H2
-setoption pp::coercion true
-setoption pp::notation false
-setoption pp::implicit true
+set::option pp::coercion true
+set::option pp::notation false
+set::option pp::implicit true
 print environment 1.
diff --git a/tests/lean/tst2.lean b/tests/lean/tst2.lean
index 49e28724f3..961ec465f7 100644
--- a/tests/lean/tst2.lean
+++ b/tests/lean/tst2.lean
@@ -2,10 +2,10 @@ print options
 variable a : Bool
 variable b : Bool
 print a/\b
-setoption lean::pp::notation false
+set::option lean::pp::notation false
 print options
 print a/\b
 print environment 2
-setoption lean::pp::notation true
+set::option lean::pp::notation true
 print options
 print a/\b
diff --git a/tests/lean/tst3.lean b/tests/lean/tst3.lean
index dadf5f1fa4..b2ee389bec 100644
--- a/tests/lean/tst3.lean
+++ b/tests/lean/tst3.lean
@@ -1,10 +1,10 @@
-setoption lean::parser::verbose false.
+set::option lean::parser::verbose false.
 notation 10 if _ then _ : implies.
 print environment 1.
 print if true then false.
 variable a : Bool.
 print if true then if a then false.
-setoption lean::pp::notation false.
+set::option lean::pp::notation false.
 print if true then if a then false.
 variable A : Type.
 variable f : A -> A -> A -> Bool.
@@ -14,29 +14,29 @@ variable c : A.
 variable d : A.
 variable e : A.
 print c |- d ; e.
-setoption lean::pp::notation true.
+set::option lean::pp::notation true.
 print c |- d ; e.
 variable fact : A -> A.
 notation 20 _ ! : fact.
 print c! !.
-setoption lean::pp::notation false.
+set::option lean::pp::notation false.
 print c! !.
-setoption lean::pp::notation true.
+set::option lean::pp::notation true.
 variable g : A -> A -> A.
 notation 30 [ _ ; _ ] : g
 print [c;d].
 print [c ; [d;e] ].
-setoption lean::pp::notation false.
+set::option lean::pp::notation false.
 print [c ; [d;e] ].
-setoption lean::pp::notation true.
+set::option lean::pp::notation true.
 variable h : A -> A -> A.
 notation 40 _ << _ >> : h.
 print environment 1.
 print d << e >>.
 print [c ; d << e >> ].
-setoption lean::pp::notation false.
+set::option lean::pp::notation false.
 print [c ; d << e >> ].
-setoption lean::pp::notation true.
+set::option lean::pp::notation true.
 variable r : A -> A -> A.
 infixl 30 ++ : r.
 variable s : A -> A -> A.
@@ -46,13 +46,13 @@ variable p1 : Bool.
 variable p2 : Bool.
 variable p3 : Bool.
 print p1 || p2 && p3.
-setoption lean::pp::notation false.
+set::option lean::pp::notation false.
 print c ** d ++ e ** c.
 print p1 || p2 && p3.
-setoption lean::pp::notation true.
+set::option lean::pp::notation true.
 print c = d || d = c.
 print  not p1 || p2.
 print p1 && p3 || p2 && p3.
-setoption lean::pp::notation false.
+set::option lean::pp::notation false.
 print  not p1 || p2.
 print p1 && p3 || p2 && p3.
diff --git a/tests/lean/tst4.lean b/tests/lean/tst4.lean
index 4103643233..17f097cce7 100644
--- a/tests/lean/tst4.lean
+++ b/tests/lean/tst4.lean
@@ -2,7 +2,7 @@ variable f {A : Type} (a b : A) : A
 variable N : Type
 variable n1 : N
 variable n2 : N
-setoption lean::pp::implicit true
+set::option lean::pp::implicit true
 print f n1 n2
 print f (fun x : N -> N, x) (fun y : _, y)
 variable EqNice {A : Type} (lhs rhs : A) : Bool
diff --git a/tests/lean/tst5.lean b/tests/lean/tst5.lean
index b47f87b697..ccdba11e08 100644
--- a/tests/lean/tst5.lean
+++ b/tests/lean/tst5.lean
@@ -3,7 +3,7 @@ variable a : N
 variable b : N
 print a = b
 check a = b
-setoption lean::pp::implicit true
+set::option lean::pp::implicit true
 print a = b
 print (Type 1) = (Type 1)
 print true = false
diff --git a/tests/lean/tst6.lean b/tests/lean/tst6.lean
index fceff6dcfc..2a100f81be 100644
--- a/tests/lean/tst6.lean
+++ b/tests/lean/tst6.lean
@@ -5,11 +5,11 @@ theorem congrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h
    congr (congr (refl h) H1) H2
 
 -- Display the theorem showing implicit arguments
-setoption lean::pp::implicit true
+set::option lean::pp::implicit true
 print environment 2
 
 -- Display the theorem hiding implicit arguments
-setoption lean::pp::implicit false
+set::option lean::pp::implicit false
 print environment 2
 
 theorem Example1 (a b c d : N) (H: (a = b ∧ b = c) ∨ (a = d ∧ d = c)) : (h a b) = (h c b) :=
@@ -20,7 +20,7 @@ theorem Example1 (a b c d : N) (H: (a = b ∧ b = c) ∨ (a = d ∧ d = c)) : (h
                    congrH (trans (and::eliml H1) (and::elimr H1)) (refl b))
 
 -- print proof of the last theorem with all implicit arguments
-setoption lean::pp::implicit true
+set::option lean::pp::implicit true
 print environment 1
 
 -- Using placeholders to hide the type of H1
@@ -31,7 +31,7 @@ theorem Example2 (a b c d : N) (H: (a = b ∧ b = c) ∨ (a = d ∧ d = c)) : (h
               (fun H1 : _,
                    congrH (trans (and::eliml H1) (and::elimr H1)) (refl b))
 
-setoption lean::pp::implicit true
+set::option lean::pp::implicit true
 print environment 1
 
 -- Same example but the first conjuct has unnecessary stuff
@@ -42,7 +42,7 @@ theorem Example3 (a b c d e : N) (H: (a = b ∧ b = e ∧ b = c) ∨ (a = d ∧
               (fun H1 : _,
                    congrH (trans (and::eliml H1) (and::elimr H1)) (refl b))
 
-setoption lean::pp::implicit false
+set::option lean::pp::implicit false
 print environment 1
 
 theorem Example4 (a b c d e : N) (H: (a = b ∧ b = e ∧ b = c) ∨ (a = d ∧ d = c)) : (h a c) = (h c a) :=
@@ -54,5 +54,5 @@ theorem Example4 (a b c d e : N) (H: (a = b ∧ b = e ∧ b = c) ∨ (a = d ∧
                    let AeqC := trans (and::eliml H1) (and::elimr H1)
                    in congrH AeqC (symm AeqC))
 
-setoption lean::pp::implicit false
+set::option lean::pp::implicit false
 print environment 1
diff --git a/tests/lean/type_inf_bug1.lean b/tests/lean/type_inf_bug1.lean
index 399b6f4dd8..8dd251ec7d 100644
--- a/tests/lean/type_inf_bug1.lean
+++ b/tests/lean/type_inf_bug1.lean
@@ -1,5 +1,5 @@
 import cast
-setoption pp::colors false
+set::option pp::colors false
 
 check fun (A A': TypeM)
           (a   : A)
diff --git a/tests/lean/unicode.lean b/tests/lean/unicode.lean
index bcec1d33af..c8287a5935 100644
--- a/tests/lean/unicode.lean
+++ b/tests/lean/unicode.lean
@@ -1,8 +1,8 @@
 print true /\ false
-setoption pp::unicode false
+set::option pp::unicode false
 print true /\ false
-setoption pp::unicode true
-setoption lean::pp::notation false
+set::option pp::unicode true
+set::option lean::pp::notation false
 print true /\ false
-setoption pp::unicode false
+set::option pp::unicode false
 print true /\ false
diff --git a/tests/lua/front.lua b/tests/lua/front.lua
index 157576be58..f230e11d75 100644
--- a/tests/lua/front.lua
+++ b/tests/lua/front.lua
@@ -10,8 +10,8 @@ variables i j : Int
 variables p q : Bool
 notation 100 _ ++ _ : f
 notation 100 _ ++ _ : g
-setoption pp::colors true
-setoption pp::width  300
+set::option pp::colors true
+set::option pp::width  300
 ]], env)
 print(get_options())
 assert(get_options():get{"pp", "colors"})
diff --git a/tests/lua/parser2.lua b/tests/lua/parser2.lua
index fd6389ddd6..3a238ccb2d 100644
--- a/tests/lua/parser2.lua
+++ b/tests/lua/parser2.lua
@@ -4,14 +4,14 @@ parse_lean_cmds([[
    variable N : Type
    variables x y : N
    variable f : N -> N -> N
-   setoption pp::colors false
+   set::option pp::colors false
 ]], env)
 local f, x, y = Consts("f, x, y")
 print(env:type_check(f(x, y)))
 assert(env:type_check(f(x, y)) == Const("N"))
 assert(not get_options():get{"pp", "colors"})
 parse_lean_cmds([[
-   setoption pp::colors true
+   set::option pp::colors true
 ]], env)
 assert(get_options():get{"pp", "colors"})
 local o = get_options()
@@ -19,7 +19,7 @@ o:update({"lean", "pp", "notation"}, false)
 assert(not o:get{"lean", "pp", "notation"})
 o = parse_lean_cmds([[
    check fun x : N, y
-   setoption pp::notation true
+   set::option pp::notation true
    check fun x : N, y
 ]], env, o)
 print(o)