chore: move Std -> Bootstrap

.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-*)

doc/BoolExpr.lean

@@ -1,4 +1,4 @@
-import Std
+import Bootstrap
 open Std
 open Lean
 

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/

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} "$@"
       '';

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

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

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

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

src/Bootstrap/Data/DList.lean

@@ -62,6 +62,3 @@ def push : DList α → α → DList α
   }
 
 instance : Append (DList α) := ⟨DList.append⟩
-
-end DList
-end Std

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

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

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

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

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

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

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

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

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

src/Bootstrap/System.lean

@@ -0,0 +1 @@
+import Bootstrap.System.Uri

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

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

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)

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
 

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

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

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

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

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

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

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

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

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
 

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

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

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.

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

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
 

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
 

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 -/
 

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.
 

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
 

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

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
 

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.  -/

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.

src/Std/Data.lean

@@ -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

src/Std/System.lean

@@ -1 +0,0 @@
-import Std.System.Uri

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();

src/lake

@@ -1 +1 @@
-Subproject commit 6cfb4e3fd7ff700ace8c2cfdb85056d59f321920
+Subproject commit b71e2f3a6c4d59b6ada8e22e297626e701dfd875

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}
 

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
 

tests/compiler/binomial.lean

@@ -1,4 +1,4 @@
-import Std.Data.BinomialHeap
+import Bootstrap.Data.BinomialHeap
 
 open Std
 

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

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
 

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
 

tests/compiler/rbmap_library.lean

@@ -1,4 +1,4 @@
-import Std
+import Bootstrap
 open Std
 
 def check (b : Bool) : IO Unit := do

tests/lean/1206.lean

@@ -1,4 +1,4 @@
-import Std
+import Bootstrap
 
 set_option linter.unusedVariables true
 

tests/lean/629.lean

@@ -1,4 +1,4 @@
-import Std.Data.BinomialHeap
+import Bootstrap.Data.BinomialHeap
 
 open Std
 

tests/lean/Uri.lean

@@ -1,4 +1,4 @@
-import Std.System.Uri
+import Bootstrap.System.Uri
 
 open Lean
 open System.Uri

tests/lean/binomialHeap.lean

@@ -1,4 +1,4 @@
-import Std
+import Bootstrap
 
 open Std
 open BinomialHeap

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

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'

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 :=

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

tests/lean/run/ac_expr.lean

@@ -1,4 +1,4 @@
-import Std
+import Bootstrap
 
 inductive Expr where
   | var (i : Nat)

tests/lean/run/arthur1.lean

@@ -1,4 +1,4 @@
-import Std
+import Bootstrap
 
 inductive NEList (α : Type)
   | uno  : α → NEList α

tests/lean/run/arthur2.lean

@@ -1,4 +1,4 @@
-import Std
+import Bootstrap
 
 inductive NEList (α : Type)
   | uno  : α → NEList α

tests/lean/run/assertAfterBug.lean

@@ -1,4 +1,4 @@
-import Std
+import Bootstrap
 
 inductive Expr where
   | var (i : Nat)

tests/lean/run/dynamic.lean

@@ -1,4 +1,4 @@
-import Std
+import Bootstrap
 open Std
 
 deriving instance TypeName for Nat

tests/lean/run/flat_expr.lean

@@ -1,4 +1,4 @@
-import Std
+import Bootstrap
 
 inductive Expr where
   | var (i : Nat)

tests/lean/run/forInElabBug.lean

@@ -1,4 +1,4 @@
-import Std
+import Bootstrap
 
 namespace Std.BinomialHeapImp
 

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

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

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

tests/lean/run/sizeof6.lean

@@ -1,4 +1,4 @@
-import Std
+import Bootstrap
 
 inductive Foo where
   | mk (args : Std.PersistentArray Foo)