diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean
index c6cc587cf6..b0cf9f11cc 100644
--- a/library/init/lean/elaborator.lean
+++ b/library/init/lean/elaborator.lean
@@ -97,6 +97,7 @@ structure local_state :=
 (ns_stack : list name := [])
 /- The set of active `open` declarations. -/
 (open_decls : list open_spec.view := [])
+(options : options := options.mk)
 
 /-- An `export` command together with the namespace it was declared in. Opening the namespace activates
     the export. -/
@@ -118,7 +119,6 @@ structure elaborator_state :=
 (expander_cfg : expander.expander_config)
 (env : environment := environment.empty)
 (ngen : name_generator)
-(options : options)
 (next_inst_idx : nat := 0)
 
 @[derive monad monad_reader monad_state monad_except]
@@ -358,6 +358,7 @@ do cfg ← read,
      univs := st.local_state.univs.entries.reverse,
      vars := st.local_state.vars.entries.reverse,
      include_vars := st.local_state.include_vars.to_list,
+     options := st.local_state.options,
      ..st},
    match st' with
    | some st' := put {
@@ -365,6 +366,7 @@ do cfg ← read,
        univs := ordered_rbmap.of_list st'.univs,
        vars := ordered_rbmap.of_list st'.vars,
        include_vars := rbtree.of_list st'.include_vars,
+       options := st'.options,
      },
      ..st', ..st}
    | none := pure (),  -- error
@@ -813,6 +815,21 @@ def export.elaborate : elaborator :=
 def init_quot.elaborate : elaborator :=
 λ stx, old_elab_command stx $ expr.mdata (kvmap.set_name {} `command `init_quot) dummy
 
+def set_option.elaborate : elaborator :=
+λ stx, do
+  let v := view «set_option» stx,
+  let opt := v.opt.val,
+  st ← get,
+  let opts := st.local_state.options,
+  -- TODO(Sebastian): check registered options
+  let opts := match v.val with
+  | option_value.view.bool b := opts.set_bool opt (match b with bool_option_value.view.true _ := tt | _ := ff)
+  | option_value.view.string lit := (match lit.value with
+    | some s := opts.set_string opt s
+    | none   := opts)  -- parser already failed
+  | option_value.view.num lit := opts.set_nat opt lit.to_nat,
+  put {st with local_state := {st.local_state with options := opts}}
+
 /-- List of commands: recursively elaborate each command. -/
 def no_kind.elaborate : coelaborator := do
   stx ← current_command,
@@ -886,7 +903,8 @@ def elaborators : rbmap name coelaborator (<) := rbmap.from_list [
   (open.name, open.elaborate),
   (export.name, export.elaborate),
   (check.name, check.elaborate),
-  (init_quot.name, init_quot.elaborate)
+  (init_quot.name, init_quot.elaborate),
+  (set_option.name, set_option.elaborate)
 ] _
 
 -- TODO: optimize
@@ -962,7 +980,7 @@ do
     parser_cfg := cfg.initial_parser_cfg,
     expander_cfg := {transformers := expander.builtin_transformers, ..cfg},
     ngen := ⟨`_ngen.fixme, 0⟩,
-    options := options.mk},
+    local_state := {options := options.mk.set_bool `trace.as_messages tt}},
   p ← except_t.run $ flip state_t.run st $ flip reader_t.run cfg $ rec_t.run
     (commands.elaborate ff max_commands)
     (λ _, modify $ λ st, {st with messages := st.messages.add {filename := "foo", pos := ⟨1,0⟩, text := "elaborator.run: out of fuel"}})
diff --git a/library/init/lean/parser/command.lean b/library/init/lean/parser/command.lean
index 77ca69a279..53f59d495c 100644
--- a/library/init/lean/parser/command.lean
+++ b/library/init/lean/parser/command.lean
@@ -98,12 +98,24 @@ node! «attribute» [
 def init_quot.parser : command_parser :=
 node! «init_quot» ["init_quot"]
 
+@[derive parser.has_tokens parser.has_view]
+def set_option.parser : command_parser :=
+node! «set_option» ["set_option", opt: ident.parser, val: node_choice! option_value {
+  bool: node_choice! bool_option_value {
+    true: symbol_or_ident "true",
+    false: symbol_or_ident "true",
+  },
+  string: string_lit.parser,
+  -- TODO(Sebastian): fractional numbers
+  num: number.parser,
+}]
+
 @[derive has_tokens]
 def builtin_command_parsers : list command_parser := [
   declaration.parser, variable.parser, variables.parser, namespace.parser, end.parser,
   open.parser, section.parser, universe.parser, notation.parser, reserve_notation.parser,
   mixfix.parser, reserve_mixfix.parser, check.parser, attribute.parser,
-  export.parser, include.parser, omit.parser, init_quot.parser]
+  export.parser, include.parser, omit.parser, init_quot.parser, set_option.parser]
 end «command»
 
 def command_parser.run (commands : list command_parser) (p : command_parser)
diff --git a/library/init/lean/parser/token.lean b/library/init/lean/parser/token.lean
index ae8022e653..447a0053ac 100644
--- a/library/init/lean/parser/token.lean
+++ b/library/init/lean/parser/token.lean
@@ -299,7 +299,7 @@ def string_lit.parser : parser :=
 lift $ try $ do {
   it ← left_over,
   stx ← token,
-  some _ ← pure $ try_view string_lit stx | error "" (dlist.singleton "number") it,
+  some _ ← pure $ try_view string_lit stx | error "" (dlist.singleton "string") it,
   pure stx
 } <?> "string"
 
@@ -307,6 +307,12 @@ instance string_lit.parser.tokens : parser.has_tokens (string_lit.parser : parse
 instance string_lit.parser.view : parser.has_view string_lit.view (string_lit.parser : parser) :=
 {..string_lit.has_view}
 
+def string_lit.view.value (lit : string_lit.view) : option string := do
+  atom ← lit.val,
+  except.ok s ← pure $ parsec.parse (parse_string_literal : parsec' _) atom.val
+    | failure,
+  pure s
+
 def ident.parser : parser :=
 lift $ try $ do {
   it ← left_over,
diff --git a/src/frontends/lean/vm_elaborator.cpp b/src/frontends/lean/vm_elaborator.cpp
index 19f5572b00..679eca5dd5 100644
--- a/src/frontends/lean/vm_elaborator.cpp
+++ b/src/frontends/lean/vm_elaborator.cpp
@@ -29,6 +29,7 @@ Lean interface to the old elaborator/elaboration parts of the parser
 #include "frontends/lean/inductive_cmds.h"
 #include "frontends/lean/structure_cmd.h"
 #include "frontends/lean/util.h"
+#include "frontends/lean/pp.h"
 
 namespace lean {
 struct resolve_names_fn : public replace_visitor {
@@ -593,16 +594,16 @@ options to_options(vm_obj o) {
     for (auto const & kv : m) {
         switch (kv.snd().kind()) {
             case data_value_kind::Bool:
-                opts.update(kv.fst(), kv.snd().get_bool());
+                opts = opts.update(kv.fst(), kv.snd().get_bool());
                 break;
             case data_value_kind::Name:
-                opts.update(kv.fst(), kv.snd().get_name());
+                opts = opts.update(kv.fst(), kv.snd().get_name());
                 break;
             case data_value_kind::Nat:
-                opts.update(kv.fst(), kv.snd().get_nat().get_small_value());
+                opts = opts.update(kv.fst(), kv.snd().get_nat().get_small_value());
                 break;
             case data_value_kind::String:
-                opts.update(kv.fst(), kv.snd().get_string());
+                opts = opts.update(kv.fst(), kv.snd().get_string());
                 break;
         }
     }
@@ -657,11 +658,8 @@ vm_obj to_obj(message_log const & log) {
 vm_obj vm_elaborate_command(vm_obj const & vm_filename, vm_obj const & vm_cmd, vm_obj const & vm_st) {
     auto vm_e = cfield(vm_st, 0);
     auto env = to_env(vm_e);
-    io_state const & ios = get_dummy_ios();
     auto filename = to_string(vm_filename);
     std::stringstream in;
-    parser p(env, ios, in, filename);
-    auto s = p.mk_snapshot();
     auto ngen = to_name_generator(cfield(vm_st, 1));
     auto vm_lds = cfield(vm_st, 2);
     local_level_decls lds;
@@ -688,58 +686,71 @@ vm_obj vm_elaborate_command(vm_obj const & vm_filename, vm_obj const & vm_cmd, v
     }
     auto includes = to_name_set(cfield(vm_st, 4));
     auto options = to_options(cfield(vm_st, 5));
-    p.reset(snapshot(p.env(), ngen, lds, eds, lvars, vars, includes, options, true, false,
-            parser_scope_stack(), to_unsigned(cfield(vm_st, 6)), pos_info {1, 0}));
-    auto ns = to_name(cfield(vm_st, 7));
-    p.set_env(set_namespace(env, ns));
 
     auto cmd = to_expr(vm_cmd);
+    auto pos = get_pos(cmd).value_or(pos_info {1, 0});
     message_log log;
-    scope_message_log _(log);
     vm_obj vm_out = mk_vm_none();
-    try {
-        elaborate_command(p, cmd);
-        s = p.mk_snapshot();
+    {
+        scope_message_log scope3(log);
+        io_state ios(options, mk_pretty_formatter_factory());
+        ios.set_regular_channel(ios.get_diagnostic_channel_ptr());
+        scope_global_ios scope_ios(ios);
+        type_context_old tc(env, options);
+        scope_trace_env scope(env, options, tc);
+        scope_traces_as_messages scope2(filename, pos);
 
-        // sort levels by reverse insertion order. ugh.
-        rb_map<unsigned, name, unsigned_rev_cmp> new_lds;
-        s->m_lds.for_each([&](name const & n, level const &) {
-            new_lds.insert(s->m_lds.find_idx(n), n);
-        });
-        new_lds.for_each([&](unsigned const &, name const & n) {
-            auto vm_n = to_obj(n);
-            auto vm_ld = mk_vm_constructor(0, vm_n, mk_vm_constructor(4, vm_n));
-            vm_lds = mk_vm_constructor(1, vm_ld, vm_lds);
-        });
+        parser p(env, ios, in, filename);
+        auto s = p.mk_snapshot();
+        p.reset(snapshot(p.env(), ngen, lds, eds, lvars, vars, includes, options, true, false,
+                         parser_scope_stack(), to_unsigned(cfield(vm_st, 6)), pos_info{1, 0}));
+        auto ns = to_name(cfield(vm_st, 7));
+        p.set_env(set_namespace(env, ns));
 
-        for (auto const & ed : s->m_eds.get_entries()) {
-            if (!is_local_p(ed.second)) {
-                // obsolete local ref, ignore
-                continue;
+        try {
+            elaborate_command(p, cmd);
+            s = p.mk_snapshot();
+
+            // sort levels by reverse insertion order. ugh.
+            rb_map<unsigned, name, unsigned_rev_cmp> new_lds;
+            s->m_lds.for_each([&](name const & n, level const &) {
+                new_lds.insert(s->m_lds.find_idx(n), n);
+            });
+            new_lds.for_each([&](unsigned const &, name const & n) {
+                auto vm_n = to_obj(n);
+                auto vm_ld = mk_vm_constructor(0, vm_n, mk_vm_constructor(4, vm_n));
+                vm_lds = mk_vm_constructor(1, vm_ld, vm_lds);
+            });
+
+            for (auto const & ed : s->m_eds.get_entries()) {
+                if (!is_local_p(ed.second)) {
+                    // obsolete local ref, ignore
+                    continue;
+                }
+                auto vm_ed = mk_vm_constructor(0, to_obj(ed.first), mk_vm_constructor(0,
+                                                                                      to_obj(local_name_p(ed.second)),
+                                                                                      mk_vm_external(new vm_expr(
+                                                                                              local_type_p(ed.second))),
+                                                                                      to_obj(local_info_p(ed.second))));
+                vm_eds = mk_vm_constructor(1, vm_ed, vm_eds);
             }
-            auto vm_ed = mk_vm_constructor(0, to_obj(ed.first), mk_vm_constructor(0,
-                    to_obj(local_name_p(ed.second)),
-                    mk_vm_external(new vm_expr(local_type_p(ed.second))),
-                    to_obj(local_info_p(ed.second))));
-            vm_eds = mk_vm_constructor(1, vm_ed, vm_eds);
-        }
 
-        auto vm_st2 = mk_vm_constructor(0, {
-            mk_vm_external(new vm_env(p.env())),
-            to_obj(s->m_ngen),
-            vm_lds,
-            vm_eds,
-            cfield(vm_st, 4),
-            cfield(vm_st, 5),
-            cfield(vm_st, 6),
-            cfield(vm_st, 7)
-        });
-        vm_out = mk_vm_some(vm_st2);
-    } catch (exception & e) {
-        message_builder builder(env, ios, filename, get_pos_info_provider()->get_pos_info_or_some(cmd),
-                message_severity::ERROR);
-        builder.set_exception(e);
-        builder.report();
+            auto vm_st2 = mk_vm_constructor(0, {
+                    mk_vm_external(new vm_env(p.env())),
+                    to_obj(s->m_ngen),
+                    vm_lds,
+                    vm_eds,
+                    cfield(vm_st, 4),
+                    cfield(vm_st, 5),
+                    cfield(vm_st, 6),
+                    cfield(vm_st, 7)
+            });
+            vm_out = mk_vm_some(vm_st2);
+        } catch (exception & e) {
+            message_builder builder(env, ios, filename, pos, message_severity::ERROR);
+            builder.set_exception(e);
+            builder.report();
+        }
     }
     return mk_vm_constructor(0, vm_out, to_obj(log));
 }