diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index d7e7d6245b..73efa31cf2 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -173,7 +173,7 @@ jobs:
       - name: List Install Tree
         run: |
           # omit contents of Init/, ...
-          tree --du -h lean-* | grep -E ' (Init|Std|Lean|Lake|LICENSE|[a-z])'
+          tree --du -h lean-* | grep -E ' (Init|Bootstrap|Lean|Lake|LICENSE|[a-z])'
       - name: Pack
         run: |
           dir=$(echo lean-*)
diff --git a/doc/BoolExpr.lean b/doc/BoolExpr.lean
index a5cb9010ea..a564b5d638 100644
--- a/doc/BoolExpr.lean
+++ b/doc/BoolExpr.lean
@@ -1,4 +1,4 @@
-import Std
+import Bootstrap
 open Std
 open Lean
 
diff --git a/doc/dev/bootstrap.md b/doc/dev/bootstrap.md
index 2e5aba9d6d..c62fdc0480 100644
--- a/doc/dev/bootstrap.md
+++ b/doc/dev/bootstrap.md
@@ -22,7 +22,7 @@ stage1/
   lib/
     lean/**/*.olean  # the Lean library (incl. the compiler) compiled by the previous stage's `lean`
     temp/**/*.{c,o}  # the library extracted to C and compiled by `leanc`
-    libInit.a libStd.a libLean.a  # static libraries of the Lean library
+    libInit.a libBootstrap.a libLean.a  # static libraries of the Lean library
     libleancpp.a  # a static library of the C++ sources of Lean
     libleanshared.so  # a dynamic library including the static libraries above
   bin/
diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix
index e49e98a149..ffd1e3e11a 100644
--- a/nix/bootstrap.nix
+++ b/nix/bootstrap.nix
@@ -93,32 +93,32 @@ rec {
         srcPrefix = "src";
         inherit debug;
       } // args);
-      Init' = build { name = "Init"; deps = []; };
-      Std'  = build { name = "Std";  deps = [ Init' ]; };
-      Lean' = build { name = "Lean"; deps = [ Init' Std' ]; };
+      Init'      = build { name = "Init"; deps = []; };
+      Bootstrap' = build { name = "Bootstrap";  deps = [ Init' ]; };
+      Lean'      = build { name = "Lean"; deps = [ Init' Bootstrap' ]; };
       attachSharedLib = sharedLib: pkg: pkg // {
         inherit sharedLib;
         mods = mapAttrs (_: m: m // { inherit sharedLib; propagatedLoadDynlibs = []; }) pkg.mods;
       };
     in (all: all // all.lean) rec {
       inherit (Lean) emacs-dev emacs-package vscode-dev vscode-package;
-      Init = attachSharedLib leanshared Init';
-      Std  = attachSharedLib leanshared Std'  // { allExternalDeps = [ Init ]; };
-      Lean = attachSharedLib leanshared Lean' // { allExternalDeps = [ Init Std ]; };
-      stdlib = [ Init Std Lean ];
+      Init      = attachSharedLib leanshared Init';
+      Bootstrap = attachSharedLib leanshared Bootstrap'  // { allExternalDeps = [ Init ]; };
+      Lean      = attachSharedLib leanshared Lean' // { allExternalDeps = [ Init Bootstrap ]; };
+      stdlib = [ Init Bootstrap Lean ];
       modDepsFiles = symlinkJoin { name = "modDepsFiles"; paths = map (l: l.modDepsFile) (stdlib ++ [ Leanc ]); };
       iTree = symlinkJoin { name = "ileans"; paths = map (l: l.iTree) stdlib; };
       extlib = stdlib;  # TODO: add Lake
       Leanc = build { name = "Leanc"; src = lean-bin-tools-unwrapped.leanc_src; deps = stdlib; roots = [ "Leanc" ]; };
-      stdlibLinkFlags = "-L${Init.staticLib} -L${Std.staticLib} -L${Lean.staticLib} -L${leancpp}/lib/lean";
+      stdlibLinkFlags = "-L${Init.staticLib} -L${Bootstrap.staticLib} -L${Lean.staticLib} -L${leancpp}/lib/lean";
       leanshared = runCommand "leanshared" { buildInputs = [ stdenv.cc ]; libName = "libleanshared${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
         mkdir $out
         LEAN_CC=${stdenv.cc}/bin/cc ${lean-bin-tools-unwrapped}/bin/leanc -shared ${lib.optionalString stdenv.isLinux "-Bsymbolic"} \
-          ${if stdenv.isDarwin then "-Wl,-force_load,${Init.staticLib}/libInit.a -Wl,-force_load,${Std.staticLib}/libStd.a -Wl,-force_load,${Lean.staticLib}/libLean.a -Wl,-force_load,${leancpp}/lib/lean/libleancpp.a ${leancpp}/lib/libleanrt_initial-exec.a -lc++"
-            else "-Wl,--whole-archive -lInit -lStd -lLean -lleancpp ${leancpp}/lib/libleanrt_initial-exec.a -Wl,--no-whole-archive -lstdc++"} -lm ${stdlibLinkFlags} \
+          ${if stdenv.isDarwin then "-Wl,-force_load,${Init.staticLib}/libInit.a -Wl,-force_load,${Bootstrap.staticLib}/libBootstrap.a -Wl,-force_load,${Lean.staticLib}/libLean.a -Wl,-force_load,${leancpp}/lib/lean/libleancpp.a ${leancpp}/lib/libleanrt_initial-exec.a -lc++"
+            else "-Wl,--whole-archive -lInit -lBootstrap -lLean -lleancpp ${leancpp}/lib/libleanrt_initial-exec.a -Wl,--no-whole-archive -lstdc++"} -lm ${stdlibLinkFlags} \
           -o $out/$libName
       '';
-      mods = Init.mods // Std.mods // Lean.mods;
+      mods = Init.mods // Bootstrap.mods // Lean.mods;
       leanc = writeShellScriptBin "leanc" ''
         LEAN_CC=${stdenv.cc}/bin/cc ${Leanc.executable.override { withSharedStdlib = true; }}/bin/leanc -I${lean-bin-tools-unwrapped}/include ${stdlibLinkFlags} -L${leanshared} "$@"
       '';
diff --git a/script/update-stage0 b/script/update-stage0
index cccf9e55fc..4179d024d6 100755
--- a/script/update-stage0
+++ b/script/update-stage0
@@ -2,7 +2,7 @@
 set -euo pipefail
 
 rm -r stage0 || true
-for pkg in Init Std Lean; do
+for pkg in Init Bootstrap Lean; do
     # ensure deterministic ordering
     c_files="$pkg.c $(cd src; find $pkg -name '*.lean' | sed 's/\.lean/.c/' | LC_ALL=C sort | tr '\n' ' ')"
     for f in $c_files; do mkdir -p $(dirname stage0/stdlib/$f); cp ${CP_PARAMS:-} $CSRCS/$f stage0/stdlib/$f; done
diff --git a/src/Std.lean b/src/Bootstrap.lean
similarity index 62%
rename from src/Std.lean
rename to src/Bootstrap.lean
index 84ec85555d..200bbe45c2 100644
--- a/src/Std.lean
+++ b/src/Bootstrap.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import Std.Data
-import Std.ShareCommon
-import Std.Dynamic
-import Std.System
+import Bootstrap.Data
+import Bootstrap.ShareCommon
+import Bootstrap.Dynamic
+import Bootstrap.System
diff --git a/src/Bootstrap/Data.lean b/src/Bootstrap/Data.lean
new file mode 100644
index 0000000000..3dc761b815
--- /dev/null
+++ b/src/Bootstrap/Data.lean
@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Bootstrap.Data.BinomialHeap
+import Bootstrap.Data.DList
+import Bootstrap.Data.Stack
+import Bootstrap.Data.Queue
+import Bootstrap.Data.HashMap
+import Bootstrap.Data.HashSet
+import Bootstrap.Data.PersistentArray
+import Bootstrap.Data.PersistentHashMap
+import Bootstrap.Data.PersistentHashSet
+import Bootstrap.Data.AssocList
+import Bootstrap.Data.RBTree
+import Bootstrap.Data.RBMap
diff --git a/src/Std/Data/AssocList.lean b/src/Bootstrap/Data/AssocList.lean
similarity index 100%
rename from src/Std/Data/AssocList.lean
rename to src/Bootstrap/Data/AssocList.lean
diff --git a/src/Std/Data/BinomialHeap.lean b/src/Bootstrap/Data/BinomialHeap.lean
similarity index 99%
rename from src/Std/Data/BinomialHeap.lean
rename to src/Bootstrap/Data/BinomialHeap.lean
index e062dcd6a5..d99d696db7 100644
--- a/src/Std/Data/BinomialHeap.lean
+++ b/src/Bootstrap/Data/BinomialHeap.lean
@@ -234,6 +234,3 @@ def ofArray (le : α → α → Bool) (as : Array α) : BinomialHeap α le :=
 /-- O(n) -/
 @[inline] def toArrayUnordered : BinomialHeap α le → Array α
   | ⟨b, _⟩ => BinomialHeapImp.toArrayUnordered b
-
-end BinomialHeap
-end Std
diff --git a/src/Std/Data/DList.lean b/src/Bootstrap/Data/DList.lean
similarity index 98%
rename from src/Std/Data/DList.lean
rename to src/Bootstrap/Data/DList.lean
index 5c37e3071b..4c1d7a121e 100644
--- a/src/Std/Data/DList.lean
+++ b/src/Bootstrap/Data/DList.lean
@@ -62,6 +62,3 @@ def push : DList α → α → DList α
   }
 
 instance : Append (DList α) := ⟨DList.append⟩
-
-end DList
-end Std
diff --git a/src/Std/Data/HashMap.lean b/src/Bootstrap/Data/HashMap.lean
similarity index 99%
rename from src/Std/Data/HashMap.lean
rename to src/Bootstrap/Data/HashMap.lean
index e9cecaeb86..579510cb8c 100644
--- a/src/Std/Data/HashMap.lean
+++ b/src/Bootstrap/Data/HashMap.lean
@@ -3,7 +3,7 @@ Copyright (c) 2018 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
-import Std.Data.AssocList
+import Bootstrap.Data.AssocList
 namespace Std
 universe u v w
 
@@ -222,6 +222,3 @@ def ofListWith (l : List (α × β)) (f : β → β → β) : HashMap α β :=
       match m.find? p.fst with
         | none   => m.insert p.fst p.snd
         | some v => m.insert p.fst $ f v p.snd)
-
-end HashMap
-end Std
diff --git a/src/Std/Data/HashSet.lean b/src/Bootstrap/Data/HashSet.lean
similarity index 99%
rename from src/Std/Data/HashSet.lean
rename to src/Bootstrap/Data/HashSet.lean
index d63e787686..3152c279e8 100644
--- a/src/Std/Data/HashSet.lean
+++ b/src/Bootstrap/Data/HashSet.lean
@@ -177,6 +177,3 @@ def toArray (m : HashSet α) : Array α :=
 
 def numBuckets (m : HashSet α) : Nat :=
   m.val.buckets.val.size
-
-end HashSet
-end Std
diff --git a/src/Std/Data/PersistentArray.lean b/src/Bootstrap/Data/PersistentArray.lean
similarity index 100%
rename from src/Std/Data/PersistentArray.lean
rename to src/Bootstrap/Data/PersistentArray.lean
diff --git a/src/Std/Data/PersistentHashMap.lean b/src/Bootstrap/Data/PersistentHashMap.lean
similarity index 99%
rename from src/Std/Data/PersistentHashMap.lean
rename to src/Bootstrap/Data/PersistentHashMap.lean
index 89df04062e..08e33e6095 100644
--- a/src/Std/Data/PersistentHashMap.lean
+++ b/src/Bootstrap/Data/PersistentHashMap.lean
@@ -348,6 +348,3 @@ def Stats.toString (s : Stats) : String :=
   s!"\{ nodes := {s.numNodes}, null := {s.numNull}, collisions := {s.numCollisions}, depth := {s.maxDepth}}"
 
 instance : ToString Stats := ⟨Stats.toString⟩
-
-end PersistentHashMap
-end Std
diff --git a/src/Std/Data/PersistentHashSet.lean b/src/Bootstrap/Data/PersistentHashSet.lean
similarity index 96%
rename from src/Std/Data/PersistentHashSet.lean
rename to src/Bootstrap/Data/PersistentHashSet.lean
index 1d444f3181..b58343da12 100644
--- a/src/Std/Data/PersistentHashSet.lean
+++ b/src/Bootstrap/Data/PersistentHashSet.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
-import Std.Data.PersistentHashMap
+import Bootstrap.Data.PersistentHashMap
 
 namespace Std
 universe u v
@@ -51,6 +51,3 @@ variable {_ : BEq α} {_ : Hashable α}
 
 @[inline] def fold {β : Type v} (f : β → α → β) (init : β) (s : PersistentHashSet α) : β :=
   Id.run $ s.foldM f init
-
-end PersistentHashSet
-end Std
diff --git a/src/Std/Data/Queue.lean b/src/Bootstrap/Data/Queue.lean
similarity index 98%
rename from src/Std/Data/Queue.lean
rename to src/Bootstrap/Data/Queue.lean
index 75d9494d8d..b7610fe9ea 100644
--- a/src/Std/Data/Queue.lean
+++ b/src/Bootstrap/Data/Queue.lean
@@ -36,6 +36,3 @@ def dequeue? (q : Queue α) : Option (α × Queue α) :=
     match q.eList.reverse with
     | []    => none
     | d::ds => some (d, { eList := [], dList := ds })
-
-end Queue
-end Std
diff --git a/src/Std/Data/RBMap.lean b/src/Bootstrap/Data/RBMap.lean
similarity index 99%
rename from src/Std/Data/RBMap.lean
rename to src/Bootstrap/Data/RBMap.lean
index 005c32b2ba..dd3186f49c 100644
--- a/src/Std/Data/RBMap.lean
+++ b/src/Bootstrap/Data/RBMap.lean
@@ -352,5 +352,3 @@ end RBMap
 
 def rbmapOf {α : Type u} {β : Type v} (l : List (α × β)) (cmp : α → α → Ordering) : RBMap α β cmp :=
   RBMap.fromList l cmp
-
-end Std
diff --git a/src/Std/Data/RBTree.lean b/src/Bootstrap/Data/RBTree.lean
similarity index 99%
rename from src/Std/Data/RBTree.lean
rename to src/Bootstrap/Data/RBTree.lean
index 042668213e..c6dc62543d 100644
--- a/src/Std/Data/RBTree.lean
+++ b/src/Bootstrap/Data/RBTree.lean
@@ -3,7 +3,7 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import Std.Data.RBMap
+import Bootstrap.Data.RBMap
 namespace Std
 universe u v w
 
@@ -114,4 +114,3 @@ end RBTree
 
 def rbtreeOf {α : Type u} (l : List α) (cmp : α → α → Ordering) : RBTree α cmp :=
   RBTree.fromList l cmp
-end Std
diff --git a/src/Std/Data/Stack.lean b/src/Bootstrap/Data/Stack.lean
similarity index 97%
rename from src/Std/Data/Stack.lean
rename to src/Bootstrap/Data/Stack.lean
index 95a4b20d59..5fd76f7b17 100644
--- a/src/Std/Data/Stack.lean
+++ b/src/Bootstrap/Data/Stack.lean
@@ -34,6 +34,3 @@ def pop [Inhabited α] (s : Stack α) : Stack α :=
 
 def modify [Inhabited α] (s : Stack α) (f : α → α) : Stack α :=
   { s with vals := s.vals.modify (s.vals.size-1) f }
-
-end Stack
-end Std
diff --git a/src/Std/Dynamic.lean b/src/Bootstrap/Dynamic.lean
similarity index 100%
rename from src/Std/Dynamic.lean
rename to src/Bootstrap/Dynamic.lean
diff --git a/src/Std/ShareCommon.lean b/src/Bootstrap/ShareCommon.lean
similarity index 97%
rename from src/Std/ShareCommon.lean
rename to src/Bootstrap/ShareCommon.lean
index de4dec84af..8efd107c92 100644
--- a/src/Std/ShareCommon.lean
+++ b/src/Bootstrap/ShareCommon.lean
@@ -3,10 +3,10 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import Std.Data.HashSet
-import Std.Data.HashMap
-import Std.Data.PersistentHashMap
-import Std.Data.PersistentHashSet
+import Bootstrap.Data.HashSet
+import Bootstrap.Data.HashMap
+import Bootstrap.Data.PersistentHashMap
+import Bootstrap.Data.PersistentHashSet
 namespace Std
 universe u v
 
@@ -153,5 +153,3 @@ instance PShareCommonT.monadShareCommon [Monad m] : MonadShareCommon (PShareComm
 
 def shareCommon (a : α) : α :=
   (withShareCommon a : ShareCommonM α).run
-
-end Std
diff --git a/src/Bootstrap/System.lean b/src/Bootstrap/System.lean
new file mode 100644
index 0000000000..b345620a9e
--- /dev/null
+++ b/src/Bootstrap/System.lean
@@ -0,0 +1 @@
+import Bootstrap.System.Uri
diff --git a/src/Std/System/Uri.lean b/src/Bootstrap/System/Uri.lean
similarity index 100%
rename from src/Std/System/Uri.lean
rename to src/Bootstrap/System/Uri.lean
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 72f99a64a6..b3c97201e9 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -263,14 +263,14 @@ find_package(PythonInterp)
 
 include_directories(${CMAKE_BINARY_DIR}/include)
 
-# libleancpp/Lean as well as libleanrt/Init/Std are cyclically dependent. This works by default on macOS, which also doesn't like
+# libleancpp/Lean as well as libleanrt/Init/Bootstrap are cyclically dependent. This works by default on macOS, which also doesn't like
 # the linker flags necessary on other platforms.
 if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
-  string(APPEND LEANC_STATIC_LINKER_FLAGS " -lleancpp -lInit -lStd -lLean -lleanrt")
+  string(APPEND LEANC_STATIC_LINKER_FLAGS " -lleancpp -lInit -lBootstrap -lLean -lleanrt")
 elseif(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
-  string(APPEND LEANC_STATIC_LINKER_FLAGS " -lleancpp -lInit -lStd -lLean -lnodefs.js -lleanrt")
+  string(APPEND LEANC_STATIC_LINKER_FLAGS " -lleancpp -lInit -lBootstrap -lLean -lnodefs.js -lleanrt")
 else()
-  string(APPEND LEANC_STATIC_LINKER_FLAGS " -Wl,--start-group -lleancpp -lLean -Wl,--end-group -Wl,--start-group -lInit -lStd -lleanrt -Wl,--end-group")
+  string(APPEND LEANC_STATIC_LINKER_FLAGS " -Wl,--start-group -lleancpp -lLean -Wl,--end-group -Wl,--start-group -lInit -lBootstrap -lleanrt -Wl,--end-group")
 endif()
 
 set(LEAN_CXX_STDLIB "-lstdc++" CACHE STRING "C++ stdlib linker flags")
@@ -445,9 +445,9 @@ string(REGEX REPLACE "^([a-zA-Z]):" "/\\1" LEAN_BIN "${CMAKE_BINARY_DIR}/bin")
 file(RELATIVE_PATH LIB ${LEAN_SOURCE_DIR} ${CMAKE_BINARY_DIR}/lib)
 
 if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
-  set(LEANSHARED_LINKER_FLAGS "-Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libStd.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
+  set(LEANSHARED_LINKER_FLAGS "-Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libBootstrap.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
 else()
-  set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit -lStd -lLean -lleancpp -Wl,--no-whole-archive ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
+  set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit -lBootstrap -lLean -lleancpp -Wl,--no-whole-archive ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
   if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
     string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a")
   endif()
@@ -462,7 +462,7 @@ add_custom_target(make_stdlib ALL
   # The actual rule is in a separate makefile because we want to prefix it with '+' to use the Make job server
   # for a parallelized nested build, but CMake doesn't let us do that.
   # We use `lean` from the previous stage, but `leanc`, headers, etc. from the current stage
-  COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Init Std Lean
+  COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Init Bootstrap Lean
   VERBATIM)
 
 # We declare these as separate custom targets so they use separate `make` invocations, which makes `make` recompute which dependencies
diff --git a/src/Lean/Data/Json/Basic.lean b/src/Lean/Data/Json/Basic.lean
index 07bc528877..44dfbc6332 100644
--- a/src/Lean/Data/Json/Basic.lean
+++ b/src/Lean/Data/Json/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Authors: Gabriel Ebner, Marc Huisinga
 -/
-import Std.Data.RBTree
+import Bootstrap.Data.RBTree
 namespace Lean
 
 -- mantissa * 10^-exponent
diff --git a/src/Lean/Data/JsonRpc.lean b/src/Lean/Data/JsonRpc.lean
index 83a0c5499c..7db8243999 100644
--- a/src/Lean/Data/JsonRpc.lean
+++ b/src/Lean/Data/JsonRpc.lean
@@ -6,7 +6,7 @@ Authors: Marc Huisinga, Wojciech Nawrocki
 -/
 import Init.Control
 import Init.System.IO
-import Std.Data.RBTree
+import Bootstrap.Data.RBTree
 import Lean.Data.Json
 
 /-! Implementation of JSON-RPC 2.0 (https://www.jsonrpc.org/specification)
diff --git a/src/Lean/Data/Name.lean b/src/Lean/Data/Name.lean
index 5c6c092db9..a9475672d2 100644
--- a/src/Lean/Data/Name.lean
+++ b/src/Lean/Data/Name.lean
@@ -3,9 +3,9 @@ Copyright (c) 2018 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
-import Std.Data.HashSet
-import Std.Data.RBMap
-import Std.Data.RBTree
+import Bootstrap.Data.HashSet
+import Bootstrap.Data.RBMap
+import Bootstrap.Data.RBTree
 import Lean.Data.SSet
 namespace Lean
 
diff --git a/src/Lean/Data/PrefixTree.lean b/src/Lean/Data/PrefixTree.lean
index 2ad20bab33..e3460cbb1c 100644
--- a/src/Lean/Data/PrefixTree.lean
+++ b/src/Lean/Data/PrefixTree.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import Std.Data.RBMap
+import Bootstrap.Data.RBMap
 
 namespace Lean
 open Std
diff --git a/src/Lean/Data/SMap.lean b/src/Lean/Data/SMap.lean
index 38d9e1a4d3..bb698e1eba 100644
--- a/src/Lean/Data/SMap.lean
+++ b/src/Lean/Data/SMap.lean
@@ -3,8 +3,8 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import Std.Data.HashMap
-import Std.Data.PersistentHashMap
+import Bootstrap.Data.HashMap
+import Bootstrap.Data.PersistentHashMap
 universe u v w w'
 
 namespace Lean
diff --git a/src/Lean/Data/Xml/Basic.lean b/src/Lean/Data/Xml/Basic.lean
index 3f9d4fb507..fd4b18d19b 100644
--- a/src/Lean/Data/Xml/Basic.lean
+++ b/src/Lean/Data/Xml/Basic.lean
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Dany Fabian
 -/
 
-import Std.Data.RBMap
+import Bootstrap.Data.RBMap
 namespace Lean
 namespace Xml
 
@@ -13,8 +13,8 @@ def Attributes := Std.RBMap String String compare
 instance : ToString Attributes := ⟨λ as => as.fold (λ s n v => s ++ s!" {n}=\"{v}\"") ""⟩
 
 mutual
-inductive Element 
-| Element 
+inductive Element
+| Element
   (name : String)
   (attributes : Attributes)
   (content : Array Content)
@@ -27,7 +27,7 @@ deriving Inhabited
 end
 
 mutual
-private partial def eToString : Element → String 
+private partial def eToString : Element → String
 | Element.Element n a c => s!"<{n}{a}>{c.map cToString |>.foldl (· ++ ·) ""}</{n}>"
 
 private partial def cToString : Content → String
diff --git a/src/Lean/Elab/DefView.lean b/src/Lean/Elab/DefView.lean
index a6570d5717..675a48fa6b 100644
--- a/src/Lean/Elab/DefView.lean
+++ b/src/Lean/Elab/DefView.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
-import Std.ShareCommon
+import Bootstrap.ShareCommon
 import Lean.Parser.Command
 import Lean.Util.CollectLevelParams
 import Lean.Util.FoldConsts
diff --git a/src/Lean/Elab/Deriving/TypeName.lean b/src/Lean/Elab/Deriving/TypeName.lean
index dc1d792fd8..baad9aa9df 100644
--- a/src/Lean/Elab/Deriving/TypeName.lean
+++ b/src/Lean/Elab/Deriving/TypeName.lean
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner
 -/
 import Lean.Elab.Deriving.Basic
-import Std.Dynamic
+import Bootstrap.Dynamic
 
 namespace Lean.Elab
 open Command Std Parser Term
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 04171e87cc..89b3bfa466 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import Std.Data.HashMap
+import Bootstrap.Data.HashMap
 import Lean.ImportingFlag
 import Lean.Data.SMap
 import Lean.Declaration
@@ -468,7 +468,7 @@ namespace SimplePersistentEnvExtension
 instance {α σ : Type} [Inhabited σ] : Inhabited (SimplePersistentEnvExtension α σ) :=
   inferInstanceAs (Inhabited (PersistentEnvExtension α α (List α × σ)))
 
-/-- Get the list of values used to update the state of the given 
+/-- Get the list of values used to update the state of the given
 `SimplePersistentEnvExtension` in the current file. -/
 def getEntries {α σ : Type} [Inhabited σ] (ext : SimplePersistentEnvExtension α σ) (env : Environment) : List α :=
   (PersistentEnvExtension.getState ext env).1
diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean
index c52afa33d0..4d758ae290 100644
--- a/src/Lean/Level.lean
+++ b/src/Lean/Level.lean
@@ -3,10 +3,10 @@ Copyright (c) 2018 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import Std.Data.HashMap
-import Std.Data.HashSet
-import Std.Data.PersistentHashMap
-import Std.Data.PersistentHashSet
+import Bootstrap.Data.HashMap
+import Bootstrap.Data.HashSet
+import Bootstrap.Data.PersistentHashMap
+import Bootstrap.Data.PersistentHashSet
 import Lean.Hygiene
 import Lean.Data.Name
 import Lean.Data.Format
diff --git a/src/Lean/Linter/UnusedVariables.lean b/src/Lean/Linter/UnusedVariables.lean
index cec35d72bd..4b17f7901e 100644
--- a/src/Lean/Linter/UnusedVariables.lean
+++ b/src/Lean/Linter/UnusedVariables.lean
@@ -3,7 +3,7 @@ import Lean.Linter.Util
 import Lean.Elab.InfoTree
 import Lean.Server.InfoUtils
 import Lean.Server.References
-import Std.Data.HashMap
+import Bootstrap.Data.HashMap
 
 namespace Lean.Linter
 open Lean.Elab.Command Lean.Server Std
diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean
index d3b708e831..06830ddbf2 100644
--- a/src/Lean/LocalContext.lean
+++ b/src/Lean/LocalContext.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import Std.Data.PersistentArray
+import Bootstrap.Data.PersistentArray
 import Lean.Expr
 import Lean.Hygiene
 
diff --git a/src/Lean/Meta/Closure.lean b/src/Lean/Meta/Closure.lean
index 474ba06a1c..613e392f06 100644
--- a/src/Lean/Meta/Closure.lean
+++ b/src/Lean/Meta/Closure.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import Std.ShareCommon
+import Bootstrap.ShareCommon
 import Lean.MetavarContext
 import Lean.Environment
 import Lean.Util.FoldConsts
diff --git a/src/Lean/Meta/Tactic/FVarSubst.lean b/src/Lean/Meta/Tactic/FVarSubst.lean
index e502987efc..ac06b93b15 100644
--- a/src/Lean/Meta/Tactic/FVarSubst.lean
+++ b/src/Lean/Meta/Tactic/FVarSubst.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import Std.Data.AssocList
+import Bootstrap.Data.AssocList
 import Lean.Expr
 import Lean.LocalContext
 import Lean.Util.ReplaceExpr
diff --git a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean
index 1688e672d1..36d2a0c67f 100644
--- a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean
@@ -5,7 +5,7 @@ Authors: Sebastian Ullrich, Daniel Selsam, Wojciech Nawrocki
 -/
 import Lean.Meta.Basic
 import Lean.SubExpr
-import Std.Data.RBMap
+import Bootstrap.Data.RBMap
 
 /-!
 # Subexpr utilities for delaborator.
diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
index cccd0e8927..c11956f913 100644
--- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Daniel Selsam
 -/
-import Std.Data.RBMap
+import Bootstrap.Data.RBMap
 import Lean.Meta.SynthInstance
 import Lean.Util.FindMVar
 import Lean.Util.FindLevelMVar
diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index 993199ff09..d253945d7c 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Marc Huisinga, Wojciech Nawrocki
 -/
 import Init.System.IO
-import Std.Data.RBMap
-import Std.System.Uri
+import Bootstrap.Data.RBMap
+import Bootstrap.System.Uri
 
 import Lean.Environment
 
diff --git a/src/Lean/Server/GoTo.lean b/src/Lean/Server/GoTo.lean
index a47a55c508..d81e5857cd 100644
--- a/src/Lean/Server/GoTo.lean
+++ b/src/Lean/Server/GoTo.lean
@@ -7,7 +7,7 @@ Authors: Sebastian Ullrich, Lars König, Wojciech Nawrocki
 import Lean.Data.Json.FromToJson
 import Lean.Util.Path
 import Lean.Server.Utils
-import Std.System.Uri
+import Bootstrap.System.Uri
 
 namespace Lean.Server
 
diff --git a/src/Lean/Server/References.lean b/src/Lean/Server/References.lean
index 21c551ca16..721341c1d4 100644
--- a/src/Lean/Server/References.lean
+++ b/src/Lean/Server/References.lean
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joscha Mennicken
 -/
 import Lean.Server.Utils
-import Std.System.Uri
+import Bootstrap.System.Uri
 
 /-! # Representing collected and deduplicated definitions and usages -/
 
diff --git a/src/Lean/Server/Rpc/Basic.lean b/src/Lean/Server/Rpc/Basic.lean
index e8e1bd95ad..4ca7d32973 100644
--- a/src/Lean/Server/Rpc/Basic.lean
+++ b/src/Lean/Server/Rpc/Basic.lean
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Wojciech Nawrocki
 -/
 import Lean.Data.Json
-import Std.Dynamic
+import Bootstrap.Dynamic
 
 /-! Allows LSP clients to make Remote Procedure Calls to the server.
 
diff --git a/src/Lean/Server/Utils.lean b/src/Lean/Server/Utils.lean
index 45a4eb2f7a..ef1d153c2e 100644
--- a/src/Lean/Server/Utils.lean
+++ b/src/Lean/Server/Utils.lean
@@ -9,7 +9,7 @@ import Lean.Data.Lsp
 import Lean.Server.InfoUtils
 import Init.System.FilePath
 import Lean.Parser.Basic
-import Std.System.Uri
+import Bootstrap.System.Uri
 
 namespace IO
 
diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean
index bb22b52f7b..be08e62f46 100644
--- a/src/Lean/Server/Watchdog.lean
+++ b/src/Lean/Server/Watchdog.lean
@@ -6,8 +6,8 @@ Authors: Marc Huisinga, Wojciech Nawrocki
 -/
 import Init.System.IO
 import Init.Data.ByteArray
-import Std.Data.RBMap
-import Std.System.Uri
+import Bootstrap.Data.RBMap
+import Bootstrap.System.Uri
 
 import Lean.Elab.Import
 import Lean.Util.Paths
diff --git a/src/Lean/SubExpr.lean b/src/Lean/SubExpr.lean
index 8dd256327b..3950414bc7 100644
--- a/src/Lean/SubExpr.lean
+++ b/src/Lean/SubExpr.lean
@@ -5,7 +5,7 @@ Authors: Sebastian Ullrich, Daniel Selsam, Wojciech Nawrocki, E.W.Ayers
 -/
 import Lean.Meta.Basic
 import Lean.Data.Json
-import Std.Data.RBMap
+import Bootstrap.Data.RBMap
 
 namespace Lean
 
diff --git a/src/Lean/Util/MonadCache.lean b/src/Lean/Util/MonadCache.lean
index 7857bc9300..d146461a17 100644
--- a/src/Lean/Util/MonadCache.lean
+++ b/src/Lean/Util/MonadCache.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import Std.Data.HashMap
+import Bootstrap.Data.HashMap
 
 namespace Lean
 /-- Interface for caching results.  -/
diff --git a/src/Lean/Util/SCC.lean b/src/Lean/Util/SCC.lean
index 93884e7534..ed0255b161 100644
--- a/src/Lean/Util/SCC.lean
+++ b/src/Lean/Util/SCC.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import Std.Data.HashMap
+import Bootstrap.Data.HashMap
 namespace Lean.SCC
 /-!
   Very simple implementation of Tarjan's SCC algorithm.
diff --git a/src/Std/Data.lean b/src/Std/Data.lean
deleted file mode 100644
index 0397c49f45..0000000000
--- a/src/Std/Data.lean
+++ /dev/null
@@ -1,17 +0,0 @@
-/-
-Copyright (c) 2020 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-import Std.Data.BinomialHeap
-import Std.Data.DList
-import Std.Data.Stack
-import Std.Data.Queue
-import Std.Data.HashMap
-import Std.Data.HashSet
-import Std.Data.PersistentArray
-import Std.Data.PersistentHashMap
-import Std.Data.PersistentHashSet
-import Std.Data.AssocList
-import Std.Data.RBTree
-import Std.Data.RBMap
diff --git a/src/Std/System.lean b/src/Std/System.lean
deleted file mode 100644
index dc8506a612..0000000000
--- a/src/Std/System.lean
+++ /dev/null
@@ -1 +0,0 @@
-import Std.System.Uri
diff --git a/src/initialize/init.cpp b/src/initialize/init.cpp
index fe47effa97..5bda8f3116 100644
--- a/src/initialize/init.cpp
+++ b/src/initialize/init.cpp
@@ -18,7 +18,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 extern "C" object* initialize_Init(object* w);
-extern "C" object* initialize_Std(object* w);
+extern "C" object* initialize_Bootstrap(object* w);
 extern "C" object* initialize_Lean(object* w);
 
 /* Initializes the Lean runtime. Before executing any code which uses the Lean package,
@@ -28,7 +28,7 @@ extern "C" LEAN_EXPORT void lean_initialize() {
     save_stack_info();
     initialize_util_module();
     consume_io_result(initialize_Init(io_mk_world()));
-    consume_io_result(initialize_Std(io_mk_world()));
+    consume_io_result(initialize_Bootstrap(io_mk_world()));
     consume_io_result(initialize_Lean(io_mk_world()));
     initialize_kernel_module();
     init_default_print_fn();
diff --git a/src/lake b/src/lake
index 6cfb4e3fd7..b71e2f3a6c 160000
--- a/src/lake
+++ b/src/lake
@@ -1 +1 @@
-Subproject commit 6cfb4e3fd7ff700ace8c2cfdb85056d59f321920
+Subproject commit b71e2f3a6c4d59b6ada8e22e297626e701dfd875
diff --git a/src/stdlib.make.in b/src/stdlib.make.in
index d0e836826a..875c56d03e 100644
--- a/src/stdlib.make.in
+++ b/src/stdlib.make.in
@@ -23,23 +23,23 @@ ifeq "${STAGE}" "0"
   LEANMAKE_OPTS+=C_ONLY=1 C_OUT=../stdlib/
 endif
 
-.PHONY: Init Std Lean leanshared Lake lean
+.PHONY: Init Bootstrap Lean leanshared Lake lean
 
 # These can be phony since the inner Makefile will have the correct dependencies and avoid rebuilds
 Init:
 # Use `+` to use the Make jobserver with `leanmake` for parallelized builds
 	+"${LEAN_BIN}/leanmake" lib PKG=Init $(LEANMAKE_OPTS) LEANC_OPTS+=-DLEAN_EXPORTING
 
-Std: Init
-	+"${LEAN_BIN}/leanmake" lib PKG=Std $(LEANMAKE_OPTS) LEANC_OPTS+=-DLEAN_EXPORTING
+Bootstrap: Init
+	+"${LEAN_BIN}/leanmake" lib PKG=Bootstrap $(LEANMAKE_OPTS) LEANC_OPTS+=-DLEAN_EXPORTING
 
-Lean: Init Std
+Lean: Init Bootstrap
 	+"${LEAN_BIN}/leanmake" lib PKG=Lean $(LEANMAKE_OPTS) LEANC_OPTS+=-DLEAN_EXPORTING
 
 # the following targets are all invoked by separate `make` calls; see src/CMakeLists.txt
 
 # we specify the precise file names here to avoid rebuilds
-${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${LIB}/lean/libInit.a ${LIB}/lean/libStd.a ${LIB}/lean/libLean.a ${LIB}/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a
+${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${LIB}/lean/libInit.a ${LIB}/lean/libBootstrap.a ${LIB}/lean/libLean.a ${LIB}/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a
 	@echo "[    ] Building $@"
 	"${CMAKE_BINARY_DIR}/leanc.sh" -shared -o $@ ${LEANSHARED_LINKER_FLAGS} ${LEANC_OPTS}
 
diff --git a/tests/bench/liasolver.lean b/tests/bench/liasolver.lean
index 1bce91cd56..074ce1c176 100644
--- a/tests/bench/liasolver.lean
+++ b/tests/bench/liasolver.lean
@@ -4,7 +4,7 @@ Linear Diophantine equation solver
 Author: Marc Huisinga
 -/
 
-import Std.Data.HashMap
+import Bootstrap.Data.HashMap
 
 open Std
 
diff --git a/tests/compiler/binomial.lean b/tests/compiler/binomial.lean
index 2dc8a77d86..72ad89a806 100644
--- a/tests/compiler/binomial.lean
+++ b/tests/compiler/binomial.lean
@@ -1,4 +1,4 @@
-import Std.Data.BinomialHeap
+import Bootstrap.Data.BinomialHeap
 
 open Std
 
diff --git a/tests/compiler/phashmap.lean b/tests/compiler/phashmap.lean
index e745908a51..2e9cd3f03b 100644
--- a/tests/compiler/phashmap.lean
+++ b/tests/compiler/phashmap.lean
@@ -1,4 +1,4 @@
-import Std.Data.PersistentHashMap
+import Bootstrap.Data.PersistentHashMap
 import Lean.Data.Format
 
 open Lean Std Std.PersistentHashMap
diff --git a/tests/compiler/phashmap2.lean b/tests/compiler/phashmap2.lean
index 6285c13184..ba7e4e19aa 100644
--- a/tests/compiler/phashmap2.lean
+++ b/tests/compiler/phashmap2.lean
@@ -1,4 +1,4 @@
-import Std.Data.PersistentHashMap
+import Bootstrap.Data.PersistentHashMap
 import Lean.Data.Format
 open Lean Std Std.PersistentHashMap
 
diff --git a/tests/compiler/phashmap3.lean b/tests/compiler/phashmap3.lean
index 481b7b0944..59a4df459f 100644
--- a/tests/compiler/phashmap3.lean
+++ b/tests/compiler/phashmap3.lean
@@ -1,4 +1,4 @@
-import Std.Data.PersistentHashMap
+import Bootstrap.Data.PersistentHashMap
 import Lean.Data.Format
 open Lean Std Std.PersistentHashMap
 
diff --git a/tests/compiler/rbmap_library.lean b/tests/compiler/rbmap_library.lean
index a35c09b01a..b97bf9c92c 100644
--- a/tests/compiler/rbmap_library.lean
+++ b/tests/compiler/rbmap_library.lean
@@ -1,4 +1,4 @@
-import Std
+import Bootstrap
 open Std
 
 def check (b : Bool) : IO Unit := do
diff --git a/tests/lean/1206.lean b/tests/lean/1206.lean
index 0553f06739..358e3232c5 100644
--- a/tests/lean/1206.lean
+++ b/tests/lean/1206.lean
@@ -1,4 +1,4 @@
-import Std
+import Bootstrap
 
 set_option linter.unusedVariables true
 
diff --git a/tests/lean/629.lean b/tests/lean/629.lean
index 2a854aeab6..3e9f861271 100644
--- a/tests/lean/629.lean
+++ b/tests/lean/629.lean
@@ -1,4 +1,4 @@
-import Std.Data.BinomialHeap
+import Bootstrap.Data.BinomialHeap
 
 open Std
 
diff --git a/tests/lean/Uri.lean b/tests/lean/Uri.lean
index 84edc94c8a..094d113f24 100644
--- a/tests/lean/Uri.lean
+++ b/tests/lean/Uri.lean
@@ -1,4 +1,4 @@
-import Std.System.Uri
+import Bootstrap.System.Uri
 
 open Lean
 open System.Uri
diff --git a/tests/lean/binomialHeap.lean b/tests/lean/binomialHeap.lean
index c2aa052ac4..88bd8bd321 100644
--- a/tests/lean/binomialHeap.lean
+++ b/tests/lean/binomialHeap.lean
@@ -1,4 +1,4 @@
-import Std
+import Bootstrap
 
 open Std
 open BinomialHeap
diff --git a/tests/lean/funInfoBug.lean b/tests/lean/funInfoBug.lean
index a3efb6ba09..926ef6bb28 100644
--- a/tests/lean/funInfoBug.lean
+++ b/tests/lean/funInfoBug.lean
@@ -1,4 +1,4 @@
-import Std.Data.AssocList
+import Bootstrap.Data.AssocList
 
 def l : List (Prod Nat Nat) := [(1, 1), (2, 2)]
 #eval l -- works
diff --git a/tests/lean/moduleOf.lean.expected.out b/tests/lean/moduleOf.lean.expected.out
index ec3944557d..8f2a984291 100644
--- a/tests/lean/moduleOf.lean.expected.out
+++ b/tests/lean/moduleOf.lean.expected.out
@@ -1,7 +1,7 @@
 (some Init.Prelude)
 (some Lean.CoreM)
 (some Lean.Elab.Term)
-(some Std.Data.HashMap)
+(some Bootstrap.Data.HashMap)
 none
 none
 moduleOf.lean:16:0-16:9: error: unknown constant 'foo'
diff --git a/tests/lean/phashmap_inst_coherence.lean b/tests/lean/phashmap_inst_coherence.lean
index 9985cf2695..72221644c9 100644
--- a/tests/lean/phashmap_inst_coherence.lean
+++ b/tests/lean/phashmap_inst_coherence.lean
@@ -1,4 +1,4 @@
-import Std.Data.PersistentHashMap
+import Bootstrap.Data.PersistentHashMap
 
 open Std
 def m : PersistentHashMap Nat Nat :=
diff --git a/tests/lean/run/PPTopDownAnalyze.lean b/tests/lean/run/PPTopDownAnalyze.lean
index 668e7b39f9..86328186c4 100644
--- a/tests/lean/run/PPTopDownAnalyze.lean
+++ b/tests/lean/run/PPTopDownAnalyze.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Daniel Selsam
 -/
 import Lean
-import Std
+import Bootstrap
 
 open Lean Lean.Meta Lean.Elab Lean.Elab.Term Lean.Elab.Command
 open Lean.PrettyPrinter
diff --git a/tests/lean/run/ac_expr.lean b/tests/lean/run/ac_expr.lean
index ee8ce1c51c..aa2eb03ddf 100644
--- a/tests/lean/run/ac_expr.lean
+++ b/tests/lean/run/ac_expr.lean
@@ -1,4 +1,4 @@
-import Std
+import Bootstrap
 
 inductive Expr where
   | var (i : Nat)
diff --git a/tests/lean/run/arthur1.lean b/tests/lean/run/arthur1.lean
index 0377d316c0..ed397f9555 100644
--- a/tests/lean/run/arthur1.lean
+++ b/tests/lean/run/arthur1.lean
@@ -1,4 +1,4 @@
-import Std
+import Bootstrap
 
 inductive NEList (α : Type)
   | uno  : α → NEList α
diff --git a/tests/lean/run/arthur2.lean b/tests/lean/run/arthur2.lean
index 9d6580f2f4..a0b4db2364 100644
--- a/tests/lean/run/arthur2.lean
+++ b/tests/lean/run/arthur2.lean
@@ -1,4 +1,4 @@
-import Std
+import Bootstrap
 
 inductive NEList (α : Type)
   | uno  : α → NEList α
diff --git a/tests/lean/run/assertAfterBug.lean b/tests/lean/run/assertAfterBug.lean
index c2547ece74..7fa3255d4d 100644
--- a/tests/lean/run/assertAfterBug.lean
+++ b/tests/lean/run/assertAfterBug.lean
@@ -1,4 +1,4 @@
-import Std
+import Bootstrap
 
 inductive Expr where
   | var (i : Nat)
diff --git a/tests/lean/run/dynamic.lean b/tests/lean/run/dynamic.lean
index 0361ed7eba..9566fd1e4c 100644
--- a/tests/lean/run/dynamic.lean
+++ b/tests/lean/run/dynamic.lean
@@ -1,4 +1,4 @@
-import Std
+import Bootstrap
 open Std
 
 deriving instance TypeName for Nat
diff --git a/tests/lean/run/flat_expr.lean b/tests/lean/run/flat_expr.lean
index aab6e13453..827f06b33c 100644
--- a/tests/lean/run/flat_expr.lean
+++ b/tests/lean/run/flat_expr.lean
@@ -1,4 +1,4 @@
-import Std
+import Bootstrap
 
 inductive Expr where
   | var (i : Nat)
diff --git a/tests/lean/run/forInElabBug.lean b/tests/lean/run/forInElabBug.lean
index e238290555..e03cb8ee6a 100644
--- a/tests/lean/run/forInElabBug.lean
+++ b/tests/lean/run/forInElabBug.lean
@@ -1,4 +1,4 @@
-import Std
+import Bootstrap
 
 namespace Std.BinomialHeapImp
 
diff --git a/tests/lean/run/forInPArray.lean b/tests/lean/run/forInPArray.lean
index 8edf42c375..5170678066 100644
--- a/tests/lean/run/forInPArray.lean
+++ b/tests/lean/run/forInPArray.lean
@@ -1,4 +1,4 @@
-import Std
+import Bootstrap
 
 def check (x : IO Nat) (expected : IO Nat) : IO Unit := do
 unless (← x) == (← expected) do
diff --git a/tests/lean/run/parray1.lean b/tests/lean/run/parray1.lean
index fe2112fdce..bf1dea69e9 100644
--- a/tests/lean/run/parray1.lean
+++ b/tests/lean/run/parray1.lean
@@ -1,4 +1,4 @@
-import Std.Data.PersistentArray
+import Bootstrap.Data.PersistentArray
 
 def check [BEq α] (as : List α) : Bool :=
   as.toPersistentArray.foldr (.::.) [] == as
diff --git a/tests/lean/run/sharecommon.lean b/tests/lean/run/sharecommon.lean
index a093c59c30..cda54f849b 100644
--- a/tests/lean/run/sharecommon.lean
+++ b/tests/lean/run/sharecommon.lean
@@ -1,4 +1,4 @@
-import Std.ShareCommon
+import Bootstrap.ShareCommon
 
 open Std
 def check (b : Bool) : ShareCommonT IO Unit := do
diff --git a/tests/lean/run/sizeof6.lean b/tests/lean/run/sizeof6.lean
index 06496411f9..0ebf0400f6 100644
--- a/tests/lean/run/sizeof6.lean
+++ b/tests/lean/run/sizeof6.lean
@@ -1,4 +1,4 @@
-import Std
+import Bootstrap
 
 inductive Foo where
   | mk (args : Std.PersistentArray Foo)