diff --git a/library/init/lean/attributes.lean b/library/init/lean/attributes.lean
index 86e85fb590..3308fac238 100644
--- a/library/init/lean/attributes.lean
+++ b/library/init/lean/attributes.lean
@@ -4,10 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.lean.environment init.lean.parser.syntax
+import init.lean.environment
 
 namespace Lean
-open Lean.Parser
+def Syntax := Unit -- Temporary hack
+def Syntax.missing := () -- Temporary hack
 
 /- Scope management -/
 
diff --git a/library/init/lean/default.lean b/library/init/lean/default.lean
index c6409573fd..473f5acd1a 100644
--- a/library/init/lean/default.lean
+++ b/library/init/lean/default.lean
@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.lean.compiler
-import init.lean.frontend
 import init.lean.extern
 import init.lean.environment
 import init.lean.modifiers
diff --git a/library/init/lean/name_mangling.lean b/library/init/lean/name_mangling.lean
index d65ed26467..5d5900f57c 100644
--- a/library/init/lean/name_mangling.lean
+++ b/library/init/lean/name_mangling.lean
@@ -4,10 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import init.lean.name init.lean.parser.stringliteral
+import init.lean.name
 namespace Lean
-open Lean.Parser
-open Lean.Parser.MonadParsec
 
 private def String.mangleAux : Nat → String.Iterator → String → String
 | 0     it r := r
diff --git a/library/init/lean/position.lean b/library/init/lean/position.lean
index 70678be580..e82cada81d 100644
--- a/library/init/lean/position.lean
+++ b/library/init/lean/position.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
-import init.data.nat init.data.rbmap init.lean.format init.lean.parser.parsec
+import init.data.nat init.data.rbmap init.lean.format
 
 namespace Lean
 
@@ -29,27 +29,4 @@ instance : HasFormat Position :=
 instance : Inhabited Position := ⟨⟨1, 0⟩⟩
 end Position
 
-/-- A precomputed cache for quickly mapping Char offsets to positionitions. -/
-structure FileMap :=
--- A mapping from Char offset of line start to line index
-(lines : RBMap Nat Nat (λ a b, a < b))
-
-namespace FileMap
-private def fromStringAux : Nat → String.OldIterator → Nat → List (Nat × Nat)
-| 0     it line := []
-| (k+1) it line :=
-  if it.hasNext = false then []
-  else match it.curr with
-       | '\n'  := (it.next.offset, line+1) :: fromStringAux k it.next (line+1)
-       | other := fromStringAux k it.next line
-
-def fromString (s : String) : FileMap :=
-{lines := RBMap.ofList $ fromStringAux s.length s.mkOldIterator 1}
-
-def toPosition (m : FileMap) (off : Nat) : Position :=
-match m.lines.lowerBound off with
-| some ⟨start, l⟩ := ⟨l, off - start⟩
-| none            := ⟨1, off⟩
-end FileMap
-
 end Lean
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index c00c7f7ad0..6bc6163916 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -154,7 +154,7 @@ int getopt_long(int argc, char *in_argv[], const char *optstring, const option *
 
 using namespace lean; // NOLINT
 
-object * lean_process_file(object * filename, object * contents, uint8 json, object * env, object * world);
+// object * lean_process_file(object * filename, object * contents, uint8 json, object * env, object * world);
 
 #ifndef LEAN_SERVER_DEFAULT_MAX_MEMORY
 #define LEAN_SERVER_DEFAULT_MAX_MEMORY 1024
@@ -505,6 +505,7 @@ int main(int argc, char ** argv) {
 
         bool ok;
         if (new_frontend) {
+#if 0
             env.set_main_module(main_module_name);
             // Some C++ parts like profiling need a global message log. We may want to refactor them into a
             // message_log-passing state monad in the future.
@@ -521,6 +522,7 @@ int main(int argc, char ** argv) {
                 ok = true;
                 env = environment(cnstr_get(io_result_get_value(res.raw()), 1), true);
             }
+#endif
         } else {
             message_log l;
             scope_message_log scope_log(l);
diff --git a/library/init/lean/elaborator.lean b/tmp/new-frontend/elaborator.lean
similarity index 100%
rename from library/init/lean/elaborator.lean
rename to tmp/new-frontend/elaborator.lean
diff --git a/library/init/lean/expander.lean b/tmp/new-frontend/expander.lean
similarity index 100%
rename from library/init/lean/expander.lean
rename to tmp/new-frontend/expander.lean
diff --git a/library/init/lean/frontend.lean b/tmp/new-frontend/frontend.lean
similarity index 100%
rename from library/init/lean/frontend.lean
rename to tmp/new-frontend/frontend.lean
diff --git a/library/init/lean/parser/basic.lean b/tmp/new-frontend/parser/basic.lean
similarity index 100%
rename from library/init/lean/parser/basic.lean
rename to tmp/new-frontend/parser/basic.lean
diff --git a/library/init/lean/parser/combinators.lean b/tmp/new-frontend/parser/combinators.lean
similarity index 100%
rename from library/init/lean/parser/combinators.lean
rename to tmp/new-frontend/parser/combinators.lean
diff --git a/library/init/lean/parser/command.lean b/tmp/new-frontend/parser/command.lean
similarity index 100%
rename from library/init/lean/parser/command.lean
rename to tmp/new-frontend/parser/command.lean
diff --git a/library/init/lean/parser/declaration.lean b/tmp/new-frontend/parser/declaration.lean
similarity index 100%
rename from library/init/lean/parser/declaration.lean
rename to tmp/new-frontend/parser/declaration.lean
diff --git a/library/init/lean/parser/identifier.lean b/tmp/new-frontend/parser/identifier.lean
similarity index 100%
rename from library/init/lean/parser/identifier.lean
rename to tmp/new-frontend/parser/identifier.lean
diff --git a/library/init/lean/parser/level.lean b/tmp/new-frontend/parser/level.lean
similarity index 100%
rename from library/init/lean/parser/level.lean
rename to tmp/new-frontend/parser/level.lean
diff --git a/library/init/lean/parser/module.lean b/tmp/new-frontend/parser/module.lean
similarity index 100%
rename from library/init/lean/parser/module.lean
rename to tmp/new-frontend/parser/module.lean
diff --git a/library/init/lean/parser/notation.lean b/tmp/new-frontend/parser/notation.lean
similarity index 100%
rename from library/init/lean/parser/notation.lean
rename to tmp/new-frontend/parser/notation.lean
diff --git a/library/init/lean/parser/parsec.lean b/tmp/new-frontend/parser/parsec.lean
similarity index 100%
rename from library/init/lean/parser/parsec.lean
rename to tmp/new-frontend/parser/parsec.lean
diff --git a/library/init/lean/parser/pratt.lean b/tmp/new-frontend/parser/pratt.lean
similarity index 100%
rename from library/init/lean/parser/pratt.lean
rename to tmp/new-frontend/parser/pratt.lean
diff --git a/library/init/lean/parser/rec.lean b/tmp/new-frontend/parser/rec.lean
similarity index 100%
rename from library/init/lean/parser/rec.lean
rename to tmp/new-frontend/parser/rec.lean
diff --git a/library/init/lean/parser/stringliteral.lean b/tmp/new-frontend/parser/stringliteral.lean
similarity index 100%
rename from library/init/lean/parser/stringliteral.lean
rename to tmp/new-frontend/parser/stringliteral.lean
diff --git a/library/init/lean/parser/syntax.lean b/tmp/new-frontend/parser/syntax.lean
similarity index 100%
rename from library/init/lean/parser/syntax.lean
rename to tmp/new-frontend/parser/syntax.lean
diff --git a/library/init/lean/parser/term.lean b/tmp/new-frontend/parser/term.lean
similarity index 100%
rename from library/init/lean/parser/term.lean
rename to tmp/new-frontend/parser/term.lean
diff --git a/library/init/lean/parser/token.lean b/tmp/new-frontend/parser/token.lean
similarity index 100%
rename from library/init/lean/parser/token.lean
rename to tmp/new-frontend/parser/token.lean
diff --git a/library/init/lean/parser/trie.lean b/tmp/new-frontend/parser/trie.lean
similarity index 100%
rename from library/init/lean/parser/trie.lean
rename to tmp/new-frontend/parser/trie.lean