diff --git a/doc/changes.md b/doc/changes.md
index 53a6ac3fb37c0..4e54b8a55b16f 100644
--- a/doc/changes.md
+++ b/doc/changes.md
@@ -1,2 +1,4 @@
 v4.0.0-m4
 ---------
+
+* Removed the deprecated `leanpkg` tool in favor of [`lake`](https://github.com/leanprover/lake).
diff --git a/doc/dev/testing.md b/doc/dev/testing.md
index fa061fc315056..77f945054332b 100644
--- a/doc/dev/testing.md
+++ b/doc/dev/testing.md
@@ -87,12 +87,3 @@ All these tests are included by [/src/shell/CMakeLists.txt](https://github.com/l
 
 - `tests/plugin`: tests that compiled Lean code can be loaded into
   `lean` via the `--plugin` command line option.
-
-- `tests/leanpkg`: tests the `leanpkg` program, where each sub-folder
-  is a complete "lean package", including:
-    - `cyclic`
-    - `user_ext`
-    - `user_attr`
-    - `user_opt`
-    - `prv`
-    - `user_attr_app`
diff --git a/doc/setup.md b/doc/setup.md
index d0e1f95635580..9783f62d0d6db 100644
--- a/doc/setup.md
+++ b/doc/setup.md
@@ -81,7 +81,7 @@ From a Lean shell, run
 $ nix flake new mypkg -t github:leanprover/lean4
 ```
 to create a new Lean package in directory `mypkg` using the latest commit of Lean 4.
-Such packages follow the same directory layout as described in the basic setup above, except for a `leanpkg.toml`/`lakefile.lean` replaced by a `flake.nix` file set up so you can run Nix commands on it, for example:
+Such packages follow the same directory layout as described in the basic setup above, except for a `lakefile.lean` replaced by a `flake.nix` file set up so you can run Nix commands on it, for example:
 ```bash
 $ nix build  # build package and all dependencies
 $ nix build .#executable  # compile `main` definition into executable (after you've added one)
@@ -116,5 +116,5 @@ nix-collect-garbage
 ```
 This will remove everything not reachable from "GC roots" such as the `./result` symlink created by `nix build`.
 
-Note that the package information in `flake.nix` is currently completely independent from `leanpkg.toml` used in the basic setup.
+Note that the package information in `flake.nix` is currently completely independent from `lakefile.lean` used in the basic setup.
 Unifying the two formats is TBD.
diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix
index 6a1f890751507..e6593ec8a04c8 100644
--- a/nix/bootstrap.nix
+++ b/nix/bootstrap.nix
@@ -104,8 +104,7 @@ rec {
       Lean = attachSharedLib leanshared Lean' // { allExternalDeps = [ Init Std ]; };
       stdlib = [ Init Std Lean ];
       iTree = symlinkJoin { name = "ileans"; paths = map (l: l.iTree) stdlib; };
-      Leanpkg = build { name = "Leanpkg"; deps = stdlib; linkFlags = ["-L${gmp}/lib -L${leanshared}"]; };
-      extlib = stdlib ++ [ Leanpkg ];
+      extlib = stdlib;  # TODO: add Lake
       Leanc = build { name = "Leanc"; src = lean-bin-tools-unwrapped.leanc_src; deps = stdlib; linkFlags = ["-L${gmp}/lib -L${leanshared}"]; };
       stdlibLinkFlags = "-L${gmp}/lib -L${Init.staticLib} -L${Std.staticLib} -L${Lean.staticLib} -L${leancpp}/lib/lean";
       leanshared = runCommand "leanshared" { buildInputs = [ stdenv.cc ]; libName = "libleanshared${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
@@ -123,7 +122,6 @@ rec {
         mkdir -p $out/bin
         ${leanc}/bin/leanc ${leancpp}/lib/lean.cpp.o ${leanshared}/* -o $out/bin/lean
       '';
-      leanpkg = Leanpkg.executable.withSharedStdlib;
       # derivation following the directory layout of the "basic" setup, mostly useful for running tests
       lean-all = wrapStage(stdenv.mkDerivation {
         name = "lean-${desc}";
@@ -131,7 +129,7 @@ rec {
           mkdir -p $out/bin $out/lib/lean
           ln -sf ${leancpp}/lib/lean/* ${lib.concatMapStringsSep " " (l: "${l.modRoot}/* ${l.staticLib}/*") (lib.reverseList extlib)} ${leanshared}/* $out/lib/lean/
           # put everything in a single final derivation so `IO.appDir` references work
-          cp ${lean}/bin/lean ${leanpkg}/bin/leanpkg ${leanc}/bin/leanc $out/bin
+          cp ${lean}/bin/lean ${leanc}/bin/leanc $out/bin
           # NOTE: `lndir` will not override existing `bin/leanc`
           ${lndir}/bin/lndir -silent ${lean-bin-tools-unwrapped} $out
         '';
diff --git a/nix/packages.nix b/nix/packages.nix
index 86a7c251cc839..b7ac881bf407d 100644
--- a/nix/packages.nix
+++ b/nix/packages.nix
@@ -88,7 +88,7 @@ let
   doc-test = stdenv.mkDerivation {
     name ="lean-doc-test";
     src = doc-src;
-    buildInputs = [ lean-mdbook lean.stage1.Leanpkg.lean-package strace ];
+    buildInputs = [ lean-mdbook lean.stage1.Lean.lean-package strace ];
     patchPhase = ''
       cd doc
       patchShebangs test
@@ -102,7 +102,7 @@ let
 in {
   inherit cc lean4-mode buildLeanPackage llvmPackages vscode-lean4;
   lean = lean.stage1;
-  stage0print-paths = lean.stage1.Leanpkg.print-paths;
+  stage0print-paths = lean.stage1.Lean.print-paths;
   HEAD-as-stage0 = (lean.stage1.Lean.overrideArgs { srcTarget = "..#stage0-from-input.stage0"; srcArgs = "(--override-input lean-stage0 ..\?rev=$(git rev-parse HEAD) -- -Dinterpreter.prefer_native=false \"$@\")"; });
   HEAD-as-stage1 = (lean.stage1.Lean.overrideArgs { srcTarget = "..\?rev=$(git rev-parse HEAD)#stage0"; });
   temci = (import temci {}).override { doCheck = false; };
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 34484c7102f01..b2b21b25d1967 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -470,12 +470,6 @@ add_custom_target(leanshared ALL
   VERBATIM)
 
 if(${STAGE} GREATER 0)
-  add_custom_target(leanpkg ALL
-    WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
-    DEPENDS leanshared
-    COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Leanpkg
-    VERBATIM)
-
   if(NOT EXISTS ${LEAN_SOURCE_DIR}/lake/Lake.lean)
     message(FATAL_ERROR "src/lake does not exist. Please check out the Lake submodule using `git submodule update --init src/lake`.")
   endif()
diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index 688bf39b23a26..b549e5be6f798 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -182,9 +182,6 @@ section Initialization
     let stderr ← IO.ofExcept stderr.get
     match (← lakeProc.wait) with
     | 0 =>
-      -- ignore any output up to the last line
-      -- TODO: leanpkg should instead redirect nested stdout output to stderr
-      let stdout := stdout.split (· == '\n') |>.getLast!
       let Except.ok (paths : LeanPaths) ← pure (Json.parse stdout >>= fromJson?)
         | throwServerError s!"invalid output from `{cmdStr}`:\n{stdout}\nstderr:\n{stderr}"
       initSearchPath (← getBuildDir) paths.oleanPath
@@ -201,13 +198,9 @@ section Initialization
     let lakePath ← match (← IO.getEnv "LAKE") with
       | some path => System.FilePath.mk path
       | none =>
-        let lakePath :=
-          -- backward compatibility, kill when `leanpkg` is removed
-          if (← System.FilePath.pathExists "leanpkg.toml") && !(← System.FilePath.pathExists "lakefile.lean") then "leanpkg"
-          else "lake"
         let lakePath ← match (← IO.getEnv "LEAN_SYSROOT") with
-          | some path => pure <| System.FilePath.mk path / "bin" / lakePath
-          | _         => pure <| (← appDir) / lakePath
+          | some path => pure <| System.FilePath.mk path / "bin" / "lake"
+          | _         => pure <| (← appDir) / "lake"
         lakePath.withExtension System.FilePath.exeExtension
     let (headerEnv, msgLog) ← try
       if let some path := m.uri.toPath? then
diff --git a/src/Leanpkg.lean b/src/Leanpkg.lean
deleted file mode 100644
index 7587ab1d23355..0000000000000
--- a/src/Leanpkg.lean
+++ /dev/null
@@ -1,228 +0,0 @@
-/-
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Sebastian Ullrich
--/
-import Leanpkg.Resolve
-import Leanpkg.Git
-import Leanpkg.Build
-import Lean.Util.Paths
-
-open System
-
-namespace Leanpkg
-
-def readManifest : IO Manifest := do
-  let m ← Manifest.fromFile leanpkgTomlFn
-  if m.leanVersion ≠ leanVersionString then
-    IO.eprintln $ "\nWARNING: Lean version mismatch: installed version is " ++ leanVersionString
-       ++ ", but package requires " ++ m.leanVersion ++ "\n"
-  return m
-
-def writeManifest (manifest : Lean.Syntax) (fn : FilePath) : IO Unit := do
-  IO.FS.writeFile fn manifest.reprint.get!
-
-def lockFileName : System.FilePath := ⟨".leanpkg-lock"⟩
-
-partial def withLockFile (x : IO α) : IO α := do
-  acquire
-  try
-    x
-  finally
-    IO.FS.removeFile lockFileName
-  where
-    acquire (firstTime := true) :=
-      try
-        -- TODO: lock file should ideally contain PID
-        if !System.Platform.isWindows then
-          discard <| IO.FS.Handle.mkPrim lockFileName "wx"
-        else
-          -- `x` mode doesn't seem to work on Windows even though it's listed at
-          -- https://docs.microsoft.com/en-us/cpp/c-runtime-library/reference/fopen-wfopen?view=msvc-160
-          -- ...? Let's use the slightly racy approach then.
-          if ← lockFileName.pathExists then
-            throw <| IO.Error.alreadyExists none 0 ""
-          discard <| IO.FS.Handle.mk lockFileName IO.FS.Mode.write
-      catch
-        | IO.Error.alreadyExists .. => do
-          if firstTime then
-            IO.eprintln s!"Waiting for prior leanpkg invocation to finish... (remove '{lockFileName}' if stuck)"
-          IO.sleep (ms := 300)
-          acquire (firstTime := false)
-        | e => throw e
-
-def getRootPart (pkg : FilePath := ".") : IO Lean.Name := do
-  let entries ← pkg.readDir
-  match entries.filter (FilePath.extension ·.fileName == "lean") with
-  | #[rootFile] => FilePath.withExtension rootFile.fileName "" |>.toString
-  | #[]         => throw <| IO.userError s!"no '.lean' file found in {← IO.FS.realPath "."}"
-  | _           => throw <| IO.userError s!"{← IO.FS.realPath "."} must contain a unique '.lean' file as the package root"
-
-structure Configuration extends Lean.LeanPaths :=
-  moreDeps    : List FilePath
-
-def configure : IO Configuration := do
-  let d ← readManifest
-  IO.eprintln $ "configuring " ++ d.name ++ " " ++ d.version
-  let assg ← solveDeps d
-  let paths ← constructPath assg
-  let mut moreDeps := [leanpkgTomlFn]
-  for path in paths do
-    unless path == FilePath.mk "." / "." do
-      -- build recursively
-      -- TODO: share build of common dependencies
-      execCmd {
-        cmd := (← IO.appPath).toString
-        cwd := path
-        args := #["build"]
-      }
-      moreDeps := (path / Build.buildPath / (← getRootPart path).toString |>.withExtension "olean") :: moreDeps
-  return {
-    oleanPath := paths.map (· / Build.buildPath)
-    srcPath   := paths
-    moreDeps
-  }
-
-def execMake (makeArgs : List String) (cfg : Build.Config) : IO Unit := withLockFile do
-  let manifest ← readManifest
-  let leanArgs := (match manifest.timeout with | some t => ["-T", toString t] | none => []) ++ cfg.leanArgs
-  let mut spawnArgs := {
-    cmd := "sh"
-    cwd := manifest.effectivePath
-    args := #["-c", s!"\"{← IO.appDir}/leanmake\" PKG={cfg.pkg} LEAN_OPTS=\"{" ".intercalate leanArgs}\" LEAN_PATH=\"{cfg.leanPath}\" {" ".intercalate makeArgs} MORE_DEPS+=\"{" ".intercalate (cfg.moreDeps.map toString)}\" >&2"]
-  }
-  execCmd spawnArgs
-
-def buildImports (imports : List String) (leanArgs : List String) : IO UInt32 := do
-  unless ← leanpkgTomlFn.pathExists do
-    return 2
-  let manifest ← readManifest
-  let cfg ← configure
-  let imports := imports.map (·.toName)
-  let root ← getRootPart
-  let localImports := imports.filter (·.getRoot == root)
-  if localImports != [] then
-    let buildCfg : Build.Config := { pkg := root, leanArgs, leanPath := cfg.oleanPath.toString, moreDeps := cfg.moreDeps }
-    if ← FilePath.pathExists "Makefile" then
-      let oleans := localImports.map fun i => Lean.modToFilePath "build" i "olean" |>.toString
-      execMake oleans buildCfg
-    else
-      Build.buildModules buildCfg localImports
-  IO.println <| Lean.Json.compress <| Lean.toJson cfg.toLeanPaths
-  return 0
-
-def build (makeArgs leanArgs : List String) : IO Unit := do
-  let cfg ← configure
-  let root ← getRootPart
-  let buildCfg : Build.Config := { pkg := root, leanArgs, leanPath := cfg.oleanPath.toString, moreDeps := cfg.moreDeps }
-  if makeArgs != [] || (← FilePath.pathExists "Makefile") then
-    execMake makeArgs buildCfg
-  else
-    Build.buildModules buildCfg [root]
-
-def initGitignoreContents :=
-  "/build
-"
-
-def initPkg (n : String) (fromNew : Bool) : IO Unit := do
-  IO.FS.writeFile leanpkgTomlFn s!"[package]
-name = \"{n}\"
-version = \"0.1\"
-lean_version = \"{leanVersionString}\"
-"
-  IO.FS.writeFile ⟨s!"{n.capitalize}.lean"⟩ "def main : IO Unit :=
-  IO.println \"Hello, world!\"
-"
-  let h ← IO.FS.Handle.mk ⟨".gitignore"⟩ IO.FS.Mode.append (bin := false)
-  h.putStr initGitignoreContents
-  unless ← System.FilePath.isDir ⟨".git"⟩ do
-    (do
-      execCmd {cmd := "git", args := #["init", "-q"]}
-      unless upstreamGitBranch = "master" do
-        execCmd {cmd := "git", args := #["checkout", "-B", upstreamGitBranch]}
-    ) <|> IO.eprintln "WARNING: failed to initialize git repository"
-
-def init (n : String) := initPkg n false
-
-def usage :=
-  "Lean package manager, version " ++ uiLeanVersionString ++ "
-
-Usage: leanpkg <command>
-
-init <name>      create a Lean package in the current directory
-configure        download and build dependencies
-build [<args>]   configure and build *.olean files
-
-See `leanpkg help <command>` for more information on a specific command."
-
-def main : (cmd : String) → (leanpkgArgs leanArgs : List String) → IO UInt32
-  | "init",      [Name], []        => init Name *> pure 0
-  | "configure", [],     []        => configure *> pure 0
-  | "print-paths", leanpkgArgs, leanArgs => buildImports leanpkgArgs leanArgs
-  | "build",     makeArgs, leanArgs  => build makeArgs leanArgs *> pure 0
-  | "help",      ["configure"], [] => IO.println "Download dependencies
-
-Usage:
-  leanpkg configure
-
-This command sets up the `build/deps` directory.
-
-For each (transitive) git dependency, the specified commit is checked out
-into a sub-directory of `build/deps`. If there are dependencies on multiple
-versions of the same package, the version materialized is undefined. No copy
-is made of local dependencies." *> pure 0
-  | "help",       ["build"], []    => IO.println "download dependencies and build *.olean files
-
-Usage:
-  leanpkg build [<leanmake-args>] [-- <lean-args>]
-
-This command invokes `leanpkg configure` followed by `leanmake <leanmake-args> LEAN_OPTS=<lean-args>`.
-If defined, the `package.timeout` configuration value is passed to Lean via its `-T` parameter.
-If no <lean-args> are given, only .olean files will be produced in `build/`. If `lib` or `bin`
-is passed instead, the extracted C code is compiled with `c++` and a static library in `build/lib`
-or an executable in `build/bin`, respectively, is created. `leanpkg build bin` requires a declaration
-of name `main` in the root namespace, which must return `IO Unit` or `IO UInt32` (the exit code) and
-may accept the program's command line arguments as a `List String` parameter.
-
-NOTE: building and linking dependent libraries currently has to be done manually, e.g.
-```
-$ (cd a; leanpkg build lib)
-$ (cd b; leanpkg build bin LINK_OPTS=../a/build/lib/libA.a)
-```" *> pure 0
-  | "help",       ["init"], []     => IO.println "Create a new Lean package in the current directory
-
-Usage:
-  leanpkg init <name>
-
-This command creates a new Lean package with the given name in the current
-directory." *> pure 0
-  | "help",       _,     []        => IO.println usage *> pure 0
-  | _,            _,     _         => throw <| IO.userError usage
-
-private def splitCmdlineArgsCore : List String → List String × List String
-  | []           => ([], [])
-  | (arg::args)  => if arg == "--"
-                    then ([], args)
-                    else
-                      let (outerArgs, innerArgs) := splitCmdlineArgsCore args
-                      (arg::outerArgs, innerArgs)
-
-def splitCmdlineArgs : List String → IO (String × List String × List String)
-| [] => throw <| IO.userError usage
-| [cmd] => return (cmd, [], [])
-| (cmd::rest) =>
-  let (outerArgs, innerArgs) := splitCmdlineArgsCore rest
-  return (cmd, outerArgs, innerArgs)
-
-end Leanpkg
-
-unsafe def main (args : List String) : IO UInt32 := do
-  try
-    Lean.enableInitializersExecution
-    Lean.initSearchPath (← Lean.getBuildDir)
-    let (cmd, outerArgs, innerArgs) ← Leanpkg.splitCmdlineArgs args
-    IO.eprintln "warning: leanpkg has been deprecated in favor of Lake (https://github.com/leanprover/lake) and will be removed in the next release."
-    Leanpkg.main cmd outerArgs innerArgs
-  catch e =>
-    IO.eprintln e  -- avoid "uncaught exception: ..."
-    pure 1
diff --git a/src/Leanpkg/.gitignore b/src/Leanpkg/.gitignore
deleted file mode 100644
index b62f4dcf7714a..0000000000000
--- a/src/Leanpkg/.gitignore
+++ /dev/null
@@ -1 +0,0 @@
-/leanpkg/config_vars.lean
diff --git a/src/Leanpkg/Build.lean b/src/Leanpkg/Build.lean
deleted file mode 100644
index 8b396d7d6c3a1..0000000000000
--- a/src/Leanpkg/Build.lean
+++ /dev/null
@@ -1,104 +0,0 @@
-/-
-Copyright (c) 2021 Sebastian Ullrich. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Ullrich
--/
-import Lean.Data.Name
-import Lean.Elab.Import
-import Leanpkg.Proc
-
-open Lean
-open System
-
-namespace Leanpkg.Build
-
-def buildPath : FilePath := "build"
-def tempBuildPath := buildPath / "temp"
-
-structure Config where
-  pkg      : Name
-  leanArgs : List String
-  leanPath : String
-  -- things like `leanpkg.toml` and olean roots of dependencies that should also trigger rebuilds
-  moreDeps : List FilePath
-
-structure Context extends Config where
-  parents       : List Name := []
-  moreDepsMTime : IO.FS.SystemTime
-
-structure Result where
-  maxMTime : IO.FS.SystemTime
-  task     : Task (Except IO.Error Unit)
-  deriving Inhabited
-
-structure State where
-  modTasks : NameMap Result := ∅
-
-abbrev BuildM := ReaderT Context <| StateT State IO
-
-partial def buildModule (mod : Name) : BuildM Result := do
-  let ctx ← read
-  if ctx.parents.contains mod then
-    -- cyclic import
-    let cycle := mod :: (ctx.parents.partition (· != mod)).1 ++ [mod]
-    let cycle := cycle.map (s!"  {·}")
-    throw <| IO.userError s!"import cycle detected:\n{"\n".intercalate cycle}"
-
-  if let some r := (← get).modTasks.find? mod then
-    -- already visited
-    return r
-
-  let leanFile := modToFilePath "." mod "lean"
-  let leanMData ← leanFile.metadata
-
-  -- recursively build dependencies and calculate transitive `maxMTime`
-  let (imports, _, _) ← Elab.parseImports (← IO.FS.readFile leanFile) leanFile.toString
-  let localImports := imports.filter (·.module.getRoot == ctx.pkg)
-  let deps ← localImports.mapM fun i =>
-    withReader (fun ctx => { ctx with parents := mod :: ctx.parents }) <|
-      buildModule i.module
-  let depMTimes ← deps.mapM (·.maxMTime)
-  let maxMTime := List.maximum? (leanMData.modified :: ctx.moreDepsMTime :: depMTimes) |>.get!
-
-  -- check whether we have an up-to-date .olean
-  let oleanFile := modToFilePath buildPath mod "olean"
-  try
-    if (← oleanFile.metadata).modified >= maxMTime then
-      let r := { maxMTime, task := Task.pure (Except.ok ()) }
-      modify fun st => { st with modTasks := st.modTasks.insert mod r }
-      return r
-  catch
-    | IO.Error.noFileOrDirectory .. => pure ()
-    | e                             => throw e
-
-  let task ← IO.mapTasks (tasks := deps.map (·.task)) fun rs => do
-    if let some e := rs.findSome? (fun | Except.error e => some e | Except.ok _ => none) then
-      -- propagate failure
-      throw e
-    try
-      let cFile := modToFilePath tempBuildPath mod "c"
-      IO.FS.createDirAll oleanFile.parent.get!
-      IO.FS.createDirAll cFile.parent.get!
-      execCmd {
-        cmd := (← IO.appDir) / "lean" |>.withExtension FilePath.exeExtension |>.toString
-        args := ctx.leanArgs.toArray ++ #["-o", oleanFile.toString, "-c", cFile.toString, leanFile.toString]
-        env := #[("LEAN_PATH", ctx.leanPath)]
-      }
-    catch e =>
-      -- print errors early
-      IO.eprintln e
-      throw e
-
-  let r := { maxMTime, task := task }
-  modify fun st => { st with modTasks := st.modTasks.insert mod r }
-  return r
-
-def buildModules (cfg : Config) (mods : List Name) : IO Unit := do
-  let moreDepsMTime := (← cfg.moreDeps.mapM (·.metadata)).map (·.modified) |>.maximum? |>.getD ⟨0, 0⟩
-  let rs ← mods.mapM buildModule |>.run { toConfig := cfg, moreDepsMTime } |>.run' {}
-  for r in rs do
-    if let Except.error _ ← IO.wait r.task then
-      -- actual error has already been printed above
-      throw <| IO.userError "Build failed."
-
-end Leanpkg.Build
diff --git a/src/Leanpkg/Git.lean b/src/Leanpkg/Git.lean
deleted file mode 100644
index 55ce109228d27..0000000000000
--- a/src/Leanpkg/Git.lean
+++ /dev/null
@@ -1,40 +0,0 @@
-/-
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Sebastian Ullrich
--/
-import Leanpkg.LeanVersion
-
-open System
-
-namespace Leanpkg
-
-def upstreamGitBranch :=
-  "master"
-
-def gitdefaultRevision : Option String → String
-  | none => upstreamGitBranch
-  | some branch => branch
-
-def gitParseRevision (gitRepo : FilePath) (rev : String) : IO String := do
-  let rev ← IO.Process.run {cmd := "git", args := #["rev-parse", "-q", "--verify", rev], cwd := gitRepo}
-  rev.trim -- remove newline at end
-
-def gitHeadRevision (gitRepo : FilePath) : IO String :=
-  gitParseRevision gitRepo "HEAD"
-
-def gitParseOriginRevision (gitRepo : FilePath) (rev : String) : IO String :=
-  (gitParseRevision gitRepo $ "origin/" ++ rev) <|> gitParseRevision gitRepo rev
-    <|> throw (IO.userError s!"cannot find revision {rev} in repository {gitRepo}")
-
-def gitLatestOriginRevision (gitRepo : FilePath) (branch : Option String) : IO String := do
-  discard <| IO.Process.run {cmd := "git", args := #["fetch"], cwd := gitRepo}
-  gitParseOriginRevision gitRepo (gitdefaultRevision branch)
-
-def gitRevisionExists (gitRepo : FilePath) (rev : String) : IO Bool := do
-  try
-    discard <| gitParseRevision gitRepo (rev ++ "^{commit}")
-    true
-  catch _ => false
-
-end Leanpkg
diff --git a/src/Leanpkg/LeanVersion.lean b/src/Leanpkg/LeanVersion.lean
deleted file mode 100644
index b1cfeb72089ff..0000000000000
--- a/src/Leanpkg/LeanVersion.lean
+++ /dev/null
@@ -1,29 +0,0 @@
-/-
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Sebastian Ullrich
--/
-namespace Leanpkg
-
-def leanVersionStringCore :=
-  s!"{Lean.version.major}.{Lean.version.minor}.{Lean.version.patch}"
-
-def origin := "leanprover/lean4"
-
-def leanVersionString :=
-  if Lean.version.isRelease then
-      s!"{origin}:{leanVersionStringCore}"
-  else if Lean.version.specialDesc ≠ "" then
-      s!"{origin}:{Lean.version.specialDesc}"
-  else
-      s!"{origin}:master"
-
-def uiLeanVersionString :=
-if Lean.version.isRelease then
-    leanVersionStringCore
-else if Lean.version.specialDesc ≠ "" then
-    Lean.version.specialDesc
-else
-    s!"master ({leanVersionStringCore})"
-
-end Leanpkg
diff --git a/src/Leanpkg/Manifest.lean b/src/Leanpkg/Manifest.lean
deleted file mode 100644
index e993564abb374..0000000000000
--- a/src/Leanpkg/Manifest.lean
+++ /dev/null
@@ -1,87 +0,0 @@
-/-
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Sebastian Ullrich
--/
-import Leanpkg.Toml
-import Leanpkg.LeanVersion
-
-open System
-
-namespace Leanpkg
-
-inductive Source where
-  | path (dir : System.FilePath) : Source
-  | git (url rev : String) (branch : Option String) : Source
-
-namespace Source
-
-def fromToml (v : Toml.Value) : OptionM Source :=
-  (do let Toml.Value.str dir ← v.lookup "path" | none
-      path ⟨dir⟩) <|>
-  (do let Toml.Value.str url ← v.lookup "git" | none
-      let Toml.Value.str rev ← v.lookup "rev" | none
-      match v.lookup "branch" with
-      | none                         => git url rev none
-      | some (Toml.Value.str branch) => git url rev (some branch)
-      | _ => none)
-
-def toToml : Source → Toml.Value
-  | path dir => Toml.Value.table [("path", Toml.Value.str dir.toString)]
-  | git url rev none =>
-    Toml.Value.table [("git", Toml.Value.str url), ("rev", Toml.Value.str rev)]
-  | git url rev (some branch) =>
-    Toml.Value.table [("git", Toml.Value.str url), ("branch", Toml.Value.str branch), ("rev", Toml.Value.str rev)]
-
-end Source
-
-structure Dependency where
-  name : String
-  src : Source
-
-structure Manifest where
-  name : String
-  version : String
-  leanVersion : String := leanVersionString
-  timeout : Option Nat := none
-  path : Option FilePath := none
-  dependencies : List Dependency := []
-
-namespace Manifest
-
-def effectivePath (m : Manifest) : FilePath :=
-  m.path.getD ⟨"."⟩
-
-def fromToml (t : Toml.Value) : Option Manifest := OptionM.run do
-  let pkg ← t.lookup "package"
-  let Toml.Value.str n ← pkg.lookup "name" | none
-  let Toml.Value.str ver ← pkg.lookup "version" | none
-  let leanVer ← match pkg.lookup "lean_version" with
-    | some (Toml.Value.str leanVer) => some leanVer
-    | none => some leanVersionString
-    | _ => none
-  let tm ← match pkg.lookup "timeout" with
-    | some (Toml.Value.nat timeout) => some (some timeout)
-    | none => some none
-    | _ => none
-  let path ← match pkg.lookup "path" with
-    | some (Toml.Value.str path) => some (some ⟨path⟩)
-    | none => some none
-    | _ => none
-  let Toml.Value.table deps ← t.lookup "dependencies" <|> some (Toml.Value.table []) | none
-  let deps ← deps.mapM fun ⟨n, src⟩ => do Dependency.mk n (← Source.fromToml src)
-  return { name := n, version := ver, leanVersion := leanVer,
-           path := path, dependencies := deps, timeout := tm }
-
-def fromFile (fn : System.FilePath) : IO Manifest := do
-  let cnts ← IO.FS.readFile fn
-  let toml ← Toml.parse cnts
-  let some manifest ← pure (fromToml toml)
-    | throw <| IO.userError s!"cannot read manifest from {fn}"
-  manifest
-
-end Manifest
-
-def leanpkgTomlFn : System.FilePath := ⟨"leanpkg.toml"⟩
-
-end Leanpkg
diff --git a/src/Leanpkg/Proc.lean b/src/Leanpkg/Proc.lean
deleted file mode 100644
index cd4db43195a73..0000000000000
--- a/src/Leanpkg/Proc.lean
+++ /dev/null
@@ -1,20 +0,0 @@
-/-
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Sebastian Ullrich
--/
-namespace Leanpkg
-
-def execCmd (args : IO.Process.SpawnArgs) : IO Unit := do
-  let envstr := String.join <| args.env.toList.map fun (k, v) => s!"{k}={v.getD ""} "
-  let cmdstr := " ".intercalate (args.cmd :: args.args.toList)
-  IO.eprintln <| "> " ++ envstr ++
-    match args.cwd with
-    | some cwd => s!"{cmdstr}    # in directory {cwd}"
-    | none     => cmdstr
-  let child ← IO.Process.spawn args
-  let exitCode ← child.wait
-  if exitCode != 0 then
-    throw <| IO.userError <| s!"external command exited with status {exitCode}"
-
-end Leanpkg
diff --git a/src/Leanpkg/Resolve.lean b/src/Leanpkg/Resolve.lean
deleted file mode 100644
index 57f76c1b02c79..0000000000000
--- a/src/Leanpkg/Resolve.lean
+++ /dev/null
@@ -1,84 +0,0 @@
-/-
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Sebastian Ullrich
--/
-import Leanpkg.Manifest
-import Leanpkg.Proc
-import Leanpkg.Git
-
-open System
-
-namespace Leanpkg
-
-def Assignment := List (String × FilePath)
-
-namespace Assignment
-def empty : Assignment := []
-
-def contains (a : Assignment) (s : String) : Bool :=
-  (a.lookup s).isSome
-
-def insert (a : Assignment) (k : String) (v : FilePath) : Assignment :=
-  if a.contains k then a else (k, v) :: a
-
-def fold {α} (i : α) (f : α → String → FilePath → α) : Assignment → α :=
-  List.foldl (fun a ⟨k, v⟩ => f a k v) i
-
-end Assignment
-
-abbrev Solver := StateT Assignment IO
-
-def notYetAssigned (d : String) : Solver Bool := do
-  ¬ (← get).contains d
-
-def resolvedPath (d : String) : Solver FilePath := do
-  let some path ← pure ((← get).lookup d) | unreachable!
-  path
-
-def materialize (relpath : FilePath) (dep : Dependency) : Solver Unit :=
-  match dep.src with
-  | Source.path dir => do
-    let depdir := dir / relpath
-    IO.eprintln s!"{dep.name}: using local path {depdir}"
-    modify (·.insert dep.name depdir)
-  | Source.git url rev branch => do
-    let depdir := FilePath.mk "build" / "deps" / dep.name
-    if ← depdir.isDir then
-      IO.eprint s!"{dep.name}: trying to update {depdir} to revision {rev}"
-      IO.eprintln (match branch with | none => "" | some branch => "@" ++ branch)
-      let hash ← gitParseOriginRevision depdir rev
-      let revEx ← gitRevisionExists depdir hash
-      unless revEx do
-        execCmd {cmd := "git", args := #["fetch"], cwd := depdir}
-    else
-      IO.eprintln s!"{dep.name}: cloning {url} to {depdir}"
-      execCmd {cmd := "git", args := #["clone", url, depdir.toString]}
-    let hash ← gitParseOriginRevision depdir rev
-    execCmd {cmd := "git", args := #["checkout", "--detach", hash], cwd := depdir}
-    modify (·.insert dep.name depdir)
-
-def solveDepsCore (relPath : FilePath) (d : Manifest) : (maxDepth : Nat) → Solver Unit
-  | 0 => throw <| IO.userError "maximum dependency resolution depth reached"
-  | maxDepth + 1 => do
-    let deps ← d.dependencies.filterM (notYetAssigned ·.name)
-    deps.forM (materialize relPath)
-    for dep in deps do
-      let p ← resolvedPath dep.name
-      let d' ← Manifest.fromFile $ p / "leanpkg.toml"
-      unless d'.name = dep.name do
-        throw <| IO.userError s!"{d.name} (in {relPath}) depends on {d'.name}, but resolved dependency has name {dep.name} (in {p})"
-      solveDepsCore p d' maxDepth
-
-def solveDeps (d : Manifest) : IO Assignment := do
-  let (_, assg) ← (solveDepsCore ⟨"."⟩ d 1024).run <| Assignment.empty.insert d.name ⟨"."⟩
-  assg
-
-def constructPathCore (depname : String) (dirname : FilePath) : IO FilePath := do
-  let path ← Manifest.effectivePath (← Manifest.fromFile <| dirname / leanpkgTomlFn)
-  return dirname / path
-
-def constructPath (assg : Assignment) : IO (List FilePath) := do
-  assg.reverse.mapM fun ⟨depname, dirname⟩ => constructPathCore depname dirname
-
-end Leanpkg
diff --git a/src/Leanpkg/Toml.lean b/src/Leanpkg/Toml.lean
deleted file mode 100644
index 31d910a63e7c1..0000000000000
--- a/src/Leanpkg/Toml.lean
+++ /dev/null
@@ -1,72 +0,0 @@
-/-
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Sebastian Ullrich
--/
-import Lean.Parser
-
-namespace Toml
-
-inductive Value : Type where
-  | str : String → Value
-  | nat : Nat → Value
-  | bool : Bool → Value
-  | table : List (String × Value) → Value
-  deriving Inhabited
-
-def Value.lookup : Value → String → Option Value
-  | Value.table cs, k => cs.lookup k
-  | _, _ => none
-
--- TODO: custom whitespace and other inaccuracies
-declare_syntax_cat val
-syntax "True" : val
-syntax "False" : val
-syntax str : val
-syntax num : val
-syntax bareKey := ident  -- TODO
-syntax key := bareKey <|> str
-declare_syntax_cat keyCat @[keyCatParser] def key' := key  -- HACK: for the antiquotation
-syntax keyVal := key " = " val
-syntax table := "[" key "]" keyVal*
-syntax inlineTable := "{" keyVal,* "}"
-syntax inlineTable : val
-syntax file := table*
-declare_syntax_cat fileCat @[fileCatParser] def file' := file  -- HACK: for the antiquotation
-
-open Lean
-
-partial def ofSyntax : Syntax → Value
-  | `(val|True) => Value.bool true
-  | `(val|False) => Value.bool false
-  | `(val|$s:strLit) => Value.str <| s.isStrLit?.get!
-  | `(val|$n:numLit) => Value.nat <| n.isNatLit?.get!
-  | `(val|{$[$keys:key = $values],*}) => toTable keys (values.map ofSyntax)
-  | `(fileCat|$[[$keys] $kvss*]*) => toTable keys <| kvss.map fun kvs => ofSyntax <| Lean.Unhygienic.run `(val|{$kvs,*})
-  | stx => unreachable!
-  where
-    toKey : Syntax → String
-      | `(keyCat|$key:ident)  => key.getId.toString
-      | `(keyCat|$key:strLit) => key.isStrLit?.get!
-      | _                     => unreachable!
-    toTable (keys : Array Syntax) (vals : Array Value) : Value :=
-      Value.table <| Array.toList <| keys.zipWith vals fun k v => (toKey k, v)
-
-open Lean.Parser
-
-def parse (input : String) : IO Value := do
-  -- HACKHACKHACK
-  let env ← importModules [{ module := `Leanpkg.Toml }] {}
-  let fileParser ← compileParserDescr (parserExtension.getState env).categories file { env := env, opts := {} }
-  let c := mkParserContext (mkInputContext input "") { env := env, options := {} }
-  let s := mkParserState input
-  let s := whitespace c s
-  let s := fileParser.fn c s
-  if s.hasError then
-    throw <| IO.userError (s.toErrorMsg c)
-  else if input.atEnd s.pos then
-    ofSyntax s.stxStack.back
-  else
-    throw <| IO.userError ((s.mkError "end of input").toErrorMsg c)
-
-end Toml
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index e61d47f927dab..d8c9a40ec35ca 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -148,82 +148,8 @@ FOREACH(T ${LEANTESTS})
   endif()
 ENDFOREACH(T)
 
-add_test(NAME leanpkgtest
-         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/b"
-         COMMAND bash -c "
-           set -eu
-           export ${TEST_VARS}
-           leanpkg build
-           # linking requires some manual steps
-           (cd ../a; leanpkg build lib)
-           leanpkg build bin LINK_OPTS=../a/build/lib/libA.a
-           ./build/bin/B")
-
-add_test(NAME leanpkgtest_cyclic
-         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/cyclic"
-         COMMAND bash -c "
-           set -eu
-           export ${TEST_VARS}
-           leanpkg build 2>&1 | grep 'import cycle'")
-
-add_test(NAME leanpkgtest_user_ext
-         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/user_ext"
-         COMMAND bash -c "
-           set -eu
-           export ${TEST_VARS}
-           find . -name '*.olean' -delete
-           leanmake | grep 'world, hello, test'")
-
-add_test(NAME leanpkgtest_user_attr
-         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/user_attr"
-         COMMAND bash -c "
-           set -eu
-           export ${TEST_VARS}
-           find . -name '*.olean' -delete
-           leanmake")
-
-add_test(NAME leanpkgtest_user_deriving
-         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/deriving"
-         COMMAND bash -c "
-           set -eu
-           export ${TEST_VARS}
-           find . -name '*.olean' -delete
-           leanmake")
-
-add_test(NAME leanpkgtest_user_opt
-         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/user_opt"
-         COMMAND bash -c "
-           set -eu
-           export ${TEST_VARS}
-           find . -name '*.olean' -delete
-           leanmake")
-
-add_test(NAME leanpkgtest_prv
-         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/prv"
-         COMMAND bash -c "
-           set -eu
-           export ${TEST_VARS}
-           find . -name '*.olean' -delete
-           leanmake 2>&1 | grep 'error: field.*private'")
-
-add_test(NAME leanpkgtest_user_attr_app
-         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/user_attr_app"
-         COMMAND bash -c "
-           set -eu
-           export ${TEST_VARS}
-           find . -name '*.olean' -delete
-           leanmake bin LINK_OPTS='${LEAN_DYN_EXE_LINKER_FLAGS}' && build/bin/UserAttr")
-
-add_test(NAME leanpkgtest_builtin_attr
-         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/builtin_attr"
-         COMMAND bash -c "
-           set -eu
-           export PATH=${LEAN_BIN}:$PATH
-           find . -name '*.olean' -delete
-           leanmake")
-
 # Create a lake test for each subdirectory of `lake/examples` which contains a `test.sh` file.
-# We skip the subdirectories `lean_packages` and `bootstrap` since `lake/examples/Makefile` do no consider them.
+# We skip the subdirectories `lean_packages` and `bootstrap` since `lake/examples/Makefile` does not consider them either.
 file(GLOB_RECURSE LEANLAKETESTS "${LEAN_SOURCE_DIR}/lake/examples/test.sh")
 FOREACH(T ${LEANLAKETESTS})
   if(NOT T MATCHES ".*lean_packages.*")
diff --git a/src/stdlib.make.in b/src/stdlib.make.in
index 0bc4c1fee3544..72f0278e7a9b4 100644
--- a/src/stdlib.make.in
+++ b/src/stdlib.make.in
@@ -24,7 +24,7 @@ ifeq "${STAGE}" "0"
   LEANMAKE_OPTS+=C_ONLY=1 C_OUT=../stdlib/
 endif
 
-.PHONY: Init Std Lean leanshared Leanpkg Lake lean
+.PHONY: Init Std Lean leanshared Lake lean
 
 # These can be phony since the inner Makefile will have the correct dependencies and avoid rebuilds
 Init:
@@ -46,9 +46,6 @@ ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}: $
 
 leanshared: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}
 
-Leanpkg:
-	+"${LEAN_BIN}/leanmake" bin PKG=Leanpkg BIN_NAME=leanpkg${CMAKE_EXECUTABLE_SUFFIX} $(LEANMAKE_OPTS) LINK_OPTS='-lleanshared ${CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE}'
-
 Lake:
 # must put lake in its own directory because of submodule, so must adjust relative paths...
 	+"${LEAN_BIN}/leanmake" -C lake bin PKG=Lake BIN_NAME=lake${CMAKE_EXECUTABLE_SUFFIX} $(LEANMAKE_OPTS) LINK_OPTS='-lleanshared ${CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE}' OUT="../${LIB}" LIB_OUT="../${LIB}/lean" OLEAN_OUT="../${LIB}/lean"
diff --git a/tests/bench/cross.nix b/tests/bench/cross.nix
index 9525befc816f0..ae0f29b53d481 100644
--- a/tests/bench/cross.nix
+++ b/tests/bench/cross.nix
@@ -32,7 +32,7 @@ let
   temci = import (builtins.fetchGit { url = http://github.com/parttimenerd/temci.git; rev = "64eca12970e8096aa20557c35fd089dd6c668e1b"; }) { inherit pkgs; };
 in pkgs.stdenv.mkDerivation rec {
   name = "bench";
-  src = pkgs.lib.sourceFilesBySuffices ./. ["Makefile" "leanpkg.path" "temci.yaml" ".py" ".lean" ".hs" ".ml" ".sml"];
+  src = pkgs.lib.sourceFilesBySuffices ./. ["Makefile" "temci.yaml" ".py" ".lean" ".hs" ".ml" ".sml"];
   LEAN_BIN = "${lean}/bin";
   #LEAN_GCC_BIN = "${lean { stdenv = pkgs.gcc9Stdenv; }}/bin";
   LEAN_NO_REUSE_BIN = "${lean.overrideAttrs (attrs: {
diff --git a/tests/leanpkg/a/.gitignore b/tests/leanpkg/a/.gitignore
deleted file mode 100644
index 796b96d1c4023..0000000000000
--- a/tests/leanpkg/a/.gitignore
+++ /dev/null
@@ -1 +0,0 @@
-/build
diff --git a/tests/leanpkg/a/A.lean b/tests/leanpkg/a/A.lean
deleted file mode 100644
index 7ee5f376002da..0000000000000
--- a/tests/leanpkg/a/A.lean
+++ /dev/null
@@ -1 +0,0 @@
-def name := "world"
diff --git a/tests/leanpkg/a/leanpkg.toml b/tests/leanpkg/a/leanpkg.toml
deleted file mode 100644
index 123e4c53fb6cd..0000000000000
--- a/tests/leanpkg/a/leanpkg.toml
+++ /dev/null
@@ -1,3 +0,0 @@
-[package]
-name = "a"
-version = "0.1"
diff --git a/tests/leanpkg/b/.gitignore b/tests/leanpkg/b/.gitignore
deleted file mode 100644
index 796b96d1c4023..0000000000000
--- a/tests/leanpkg/b/.gitignore
+++ /dev/null
@@ -1 +0,0 @@
-/build
diff --git a/tests/leanpkg/b/B.lean b/tests/leanpkg/b/B.lean
deleted file mode 100644
index fc5594b7a61c8..0000000000000
--- a/tests/leanpkg/b/B.lean
+++ /dev/null
@@ -1,6 +0,0 @@
-import A
-import B.Bar
-import B.Baz
-
-def main : IO Unit :=
-  IO.println s!"Hello, {foo} {name}!"
diff --git a/tests/leanpkg/b/B/Bar.lean b/tests/leanpkg/b/B/Bar.lean
deleted file mode 100644
index 7ca89339f6a16..0000000000000
--- a/tests/leanpkg/b/B/Bar.lean
+++ /dev/null
@@ -1,3 +0,0 @@
-import B.Foo
-
-def bar := "bar"
diff --git a/tests/leanpkg/b/B/Baz.lean b/tests/leanpkg/b/B/Baz.lean
deleted file mode 100644
index 4823066822f7a..0000000000000
--- a/tests/leanpkg/b/B/Baz.lean
+++ /dev/null
@@ -1,3 +0,0 @@
-import B.Foo
-
-def baz := "baz"
diff --git a/tests/leanpkg/b/B/Foo.lean b/tests/leanpkg/b/B/Foo.lean
deleted file mode 100644
index 060b281a849c1..0000000000000
--- a/tests/leanpkg/b/B/Foo.lean
+++ /dev/null
@@ -1,2 +0,0 @@
-def foo := "foo"
---#eval IO.sleep 3000
diff --git a/tests/leanpkg/b/leanpkg.toml b/tests/leanpkg/b/leanpkg.toml
deleted file mode 100644
index 4dfec95d814a0..0000000000000
--- a/tests/leanpkg/b/leanpkg.toml
+++ /dev/null
@@ -1,6 +0,0 @@
-[package]
-name = "b"
-version = "0.1"
-
-[dependencies]
-a = { path = "../a" }
diff --git a/tests/leanpkg/builtin_attr/.gitignore b/tests/leanpkg/builtin_attr/.gitignore
deleted file mode 100644
index 796b96d1c4023..0000000000000
--- a/tests/leanpkg/builtin_attr/.gitignore
+++ /dev/null
@@ -1 +0,0 @@
-/build
diff --git a/tests/leanpkg/builtin_attr/UserAttr.lean b/tests/leanpkg/builtin_attr/UserAttr.lean
deleted file mode 100644
index 28b59b3472406..0000000000000
--- a/tests/leanpkg/builtin_attr/UserAttr.lean
+++ /dev/null
@@ -1 +0,0 @@
-import UserAttr.Tst
diff --git a/tests/leanpkg/builtin_attr/UserAttr/BlaAttr.lean b/tests/leanpkg/builtin_attr/UserAttr/BlaAttr.lean
deleted file mode 100644
index 6fb03c4e86d60..0000000000000
--- a/tests/leanpkg/builtin_attr/UserAttr/BlaAttr.lean
+++ /dev/null
@@ -1,11 +0,0 @@
-import Lean
-
-open Lean
-
--- initialize discard <| registerTagAttribute `foo ""
-
-initialize registerBuiltinAttribute {
-    name := `bar,
-    descr := "",
-    add := fun _ _ _ => ()
-  }
diff --git a/tests/leanpkg/builtin_attr/UserAttr/Tst.lean b/tests/leanpkg/builtin_attr/UserAttr/Tst.lean
deleted file mode 100644
index 76870872c46d5..0000000000000
--- a/tests/leanpkg/builtin_attr/UserAttr/Tst.lean
+++ /dev/null
@@ -1,4 +0,0 @@
-import UserAttr.BlaAttr
-
-@[bar] def f (x : Nat) := x + 2
-@[bar] def g (x : Nat) := x + 1
diff --git a/tests/leanpkg/builtin_attr/leanpkg.toml b/tests/leanpkg/builtin_attr/leanpkg.toml
deleted file mode 100644
index 155f689776372..0000000000000
--- a/tests/leanpkg/builtin_attr/leanpkg.toml
+++ /dev/null
@@ -1,3 +0,0 @@
-[package]
-name = "UserAttr"
-version = "0.1"
diff --git a/tests/leanpkg/cyclic/Cyclic.lean b/tests/leanpkg/cyclic/Cyclic.lean
deleted file mode 100644
index 5af4f224d9523..0000000000000
--- a/tests/leanpkg/cyclic/Cyclic.lean
+++ /dev/null
@@ -1 +0,0 @@
-import Cyclic.A
diff --git a/tests/leanpkg/cyclic/Cyclic/A.lean b/tests/leanpkg/cyclic/Cyclic/A.lean
deleted file mode 100644
index 31d5d96dcc615..0000000000000
--- a/tests/leanpkg/cyclic/Cyclic/A.lean
+++ /dev/null
@@ -1 +0,0 @@
-import Cyclic.A.B
diff --git a/tests/leanpkg/cyclic/Cyclic/A/B.lean b/tests/leanpkg/cyclic/Cyclic/A/B.lean
deleted file mode 100644
index 41c84985d2a23..0000000000000
--- a/tests/leanpkg/cyclic/Cyclic/A/B.lean
+++ /dev/null
@@ -1 +0,0 @@
-import Cyclic
diff --git a/tests/leanpkg/cyclic/leanpkg.toml b/tests/leanpkg/cyclic/leanpkg.toml
deleted file mode 100644
index 8f7f2d5db653b..0000000000000
--- a/tests/leanpkg/cyclic/leanpkg.toml
+++ /dev/null
@@ -1,4 +0,0 @@
-[package]
-name = "cyclic"
-version = "0.1"
-lean_version = "leanprover/lean4:master"
diff --git a/tests/leanpkg/deriving/UserDeriving.lean b/tests/leanpkg/deriving/UserDeriving.lean
deleted file mode 100644
index 92d1187af1726..0000000000000
--- a/tests/leanpkg/deriving/UserDeriving.lean
+++ /dev/null
@@ -1 +0,0 @@
-import UserDeriving.Tst
diff --git a/tests/leanpkg/deriving/UserDeriving/Simple.lean b/tests/leanpkg/deriving/UserDeriving/Simple.lean
deleted file mode 100644
index 23026e847a7c1..0000000000000
--- a/tests/leanpkg/deriving/UserDeriving/Simple.lean
+++ /dev/null
@@ -1,15 +0,0 @@
-import Lean
-
-class Simple (α : Type u) where
-  val : α
-
-open Lean
-open Lean.Elab
-open Lean.Elab.Command
-def mkSimpleHandler (declNames : Array Name) : CommandElabM Bool := do
-  dbg_trace ">> mkSimpleHandler {declNames}"
-  -- TODO: see examples at src/Lean/Elab/Deriving
-  return true
-
-initialize
-  registerBuiltinDerivingHandler ``Simple mkSimpleHandler
diff --git a/tests/leanpkg/deriving/UserDeriving/Tst.lean b/tests/leanpkg/deriving/UserDeriving/Tst.lean
deleted file mode 100644
index 51970ac3d99c7..0000000000000
--- a/tests/leanpkg/deriving/UserDeriving/Tst.lean
+++ /dev/null
@@ -1,6 +0,0 @@
-import UserDeriving.Simple
-
-inductive Foo where
-  | mk₁
-  | mk₂
-  deriving Simple
diff --git a/tests/leanpkg/deriving/leanpkg.toml b/tests/leanpkg/deriving/leanpkg.toml
deleted file mode 100644
index bc4f17da39bb2..0000000000000
--- a/tests/leanpkg/deriving/leanpkg.toml
+++ /dev/null
@@ -1,3 +0,0 @@
-[package]
-name = "UserDeriving"
-version = "0.1"
diff --git a/tests/leanpkg/prv/Prv.lean b/tests/leanpkg/prv/Prv.lean
deleted file mode 100644
index 7d4ffe3509608..0000000000000
--- a/tests/leanpkg/prv/Prv.lean
+++ /dev/null
@@ -1,5 +0,0 @@
-import Prv.Foo
-
-#check { name := "leo", val := 15 : Foo }
-#check { name := "leo", val := 15 : Foo }.name
-#check { name := "leo", val := 15 : Foo }.val -- Error
diff --git a/tests/leanpkg/prv/Prv/Foo.lean b/tests/leanpkg/prv/Prv/Foo.lean
deleted file mode 100644
index 5a386ecd88a24..0000000000000
--- a/tests/leanpkg/prv/Prv/Foo.lean
+++ /dev/null
@@ -1,6 +0,0 @@
-structure Foo where
-  private val : Nat
-  name : String
-
-#check { name := "leo", val := 15 : Foo }
-#check { name := "leo", val := 15 : Foo }.val
diff --git a/tests/leanpkg/prv/leanpkg.toml b/tests/leanpkg/prv/leanpkg.toml
deleted file mode 100644
index f9c5e825ef488..0000000000000
--- a/tests/leanpkg/prv/leanpkg.toml
+++ /dev/null
@@ -1,3 +0,0 @@
-[package]
-name = "Prv"
-version = "0.1"
diff --git a/tests/leanpkg/user_attr/.gitignore b/tests/leanpkg/user_attr/.gitignore
deleted file mode 100644
index 796b96d1c4023..0000000000000
--- a/tests/leanpkg/user_attr/.gitignore
+++ /dev/null
@@ -1 +0,0 @@
-/build
diff --git a/tests/leanpkg/user_attr/UserAttr.lean b/tests/leanpkg/user_attr/UserAttr.lean
deleted file mode 100644
index ec633fea1cf11..0000000000000
--- a/tests/leanpkg/user_attr/UserAttr.lean
+++ /dev/null
@@ -1,12 +0,0 @@
-import UserAttr.Tst
-
-open Lean
-
-def tst : MetaM Unit := do
-  let env ← getEnv
-  assert! (blaAttr.hasTag env `f)
-  assert! (blaAttr.hasTag env `g)
-  assert! !(blaAttr.hasTag env `id)
-  pure ()
-
-#eval tst
diff --git a/tests/leanpkg/user_attr/UserAttr/BlaAttr.lean b/tests/leanpkg/user_attr/UserAttr/BlaAttr.lean
deleted file mode 100644
index 7314fc152b60f..0000000000000
--- a/tests/leanpkg/user_attr/UserAttr/BlaAttr.lean
+++ /dev/null
@@ -1,5 +0,0 @@
-import Lean
-
-open Lean
-
-initialize blaAttr : TagAttribute ← registerTagAttribute `bla "simple user defined attribute"
diff --git a/tests/leanpkg/user_attr/UserAttr/Tst.lean b/tests/leanpkg/user_attr/UserAttr/Tst.lean
deleted file mode 100644
index f80db320f8829..0000000000000
--- a/tests/leanpkg/user_attr/UserAttr/Tst.lean
+++ /dev/null
@@ -1,4 +0,0 @@
-import UserAttr.BlaAttr
-
-@[bla] def f (x : Nat) := x + 2
-@[bla] def g (x : Nat) := x + 1
diff --git a/tests/leanpkg/user_attr/leanpkg.toml b/tests/leanpkg/user_attr/leanpkg.toml
deleted file mode 100644
index 155f689776372..0000000000000
--- a/tests/leanpkg/user_attr/leanpkg.toml
+++ /dev/null
@@ -1,3 +0,0 @@
-[package]
-name = "UserAttr"
-version = "0.1"
diff --git a/tests/leanpkg/user_attr_app/.gitignore b/tests/leanpkg/user_attr_app/.gitignore
deleted file mode 100644
index 796b96d1c4023..0000000000000
--- a/tests/leanpkg/user_attr_app/.gitignore
+++ /dev/null
@@ -1 +0,0 @@
-/build
diff --git a/tests/leanpkg/user_attr_app/UserAttr.lean b/tests/leanpkg/user_attr_app/UserAttr.lean
deleted file mode 100644
index 219093ee95d0e..0000000000000
--- a/tests/leanpkg/user_attr_app/UserAttr.lean
+++ /dev/null
@@ -1,16 +0,0 @@
-import UserAttr.Tst
-
-open Lean
-
-def tst : MetaM Unit := do
-  let env ← getEnv
-  assert! (blaAttr.hasTag env `f)
-  assert! (blaAttr.hasTag env `g)
-  assert! !(blaAttr.hasTag env `id)
-  pure ()
-
-#eval tst
-
-unsafe def main : IO Unit := do
-  initSearchPath (← Lean.findSysroot?) ["build"]
-  withImportModules [{ module := `UserAttr.Tst : Import }] {} 0 fun env => ()
diff --git a/tests/leanpkg/user_attr_app/UserAttr/BlaAttr.lean b/tests/leanpkg/user_attr_app/UserAttr/BlaAttr.lean
deleted file mode 100644
index 7314fc152b60f..0000000000000
--- a/tests/leanpkg/user_attr_app/UserAttr/BlaAttr.lean
+++ /dev/null
@@ -1,5 +0,0 @@
-import Lean
-
-open Lean
-
-initialize blaAttr : TagAttribute ← registerTagAttribute `bla "simple user defined attribute"
diff --git a/tests/leanpkg/user_attr_app/UserAttr/Tst.lean b/tests/leanpkg/user_attr_app/UserAttr/Tst.lean
deleted file mode 100644
index f80db320f8829..0000000000000
--- a/tests/leanpkg/user_attr_app/UserAttr/Tst.lean
+++ /dev/null
@@ -1,4 +0,0 @@
-import UserAttr.BlaAttr
-
-@[bla] def f (x : Nat) := x + 2
-@[bla] def g (x : Nat) := x + 1
diff --git a/tests/leanpkg/user_attr_app/leanpkg.toml b/tests/leanpkg/user_attr_app/leanpkg.toml
deleted file mode 100644
index 155f689776372..0000000000000
--- a/tests/leanpkg/user_attr_app/leanpkg.toml
+++ /dev/null
@@ -1,3 +0,0 @@
-[package]
-name = "UserAttr"
-version = "0.1"
diff --git a/tests/leanpkg/user_ext/.gitignore b/tests/leanpkg/user_ext/.gitignore
deleted file mode 100644
index 796b96d1c4023..0000000000000
--- a/tests/leanpkg/user_ext/.gitignore
+++ /dev/null
@@ -1 +0,0 @@
-/build
diff --git a/tests/leanpkg/user_ext/UserExt.lean b/tests/leanpkg/user_ext/UserExt.lean
deleted file mode 100644
index b8531c360c5ad..0000000000000
--- a/tests/leanpkg/user_ext/UserExt.lean
+++ /dev/null
@@ -1,5 +0,0 @@
-import UserExt.Tst1
-import UserExt.Tst2
-
-show_foo_set
-show_bla_set
diff --git a/tests/leanpkg/user_ext/UserExt/BlaExt.lean b/tests/leanpkg/user_ext/UserExt/BlaExt.lean
deleted file mode 100644
index 5284117fe934c..0000000000000
--- a/tests/leanpkg/user_ext/UserExt/BlaExt.lean
+++ /dev/null
@@ -1,23 +0,0 @@
-import Lean
-
-open Lean
-
-initialize blaExtension : SimplePersistentEnvExtension Name NameSet ←
-  registerSimplePersistentEnvExtension {
-    name          := `blaExt
-    addEntryFn    := NameSet.insert
-    addImportedFn := fun es => mkStateFromImportedEntries NameSet.insert {} es
-  }
-
-syntax (name := insertBla) "insert_bla " ident : command
-syntax (name := showBla) "show_bla_set" : command
-
-open Lean.Elab
-open Lean.Elab.Command
-
-@[commandElab insertBla] def elabInsertBla : CommandElab := fun stx => do
-  IO.println s!"inserting {stx[1].getId}"
-  modifyEnv fun env => blaExtension.addEntry env stx[1].getId
-
-@[commandElab showBla] def elabShowBla : CommandElab := fun stx => do
-  IO.println s!"bla set: {blaExtension.getState (← getEnv) |>.toList}"
diff --git a/tests/leanpkg/user_ext/UserExt/FooExt.lean b/tests/leanpkg/user_ext/UserExt/FooExt.lean
deleted file mode 100644
index 686ec53f824b3..0000000000000
--- a/tests/leanpkg/user_ext/UserExt/FooExt.lean
+++ /dev/null
@@ -1,26 +0,0 @@
-import Lean
-
-open Lean
-
-initialize fooExtension : SimplePersistentEnvExtension Name NameSet ←
-  registerSimplePersistentEnvExtension {
-    name          := `fooExt
-    addEntryFn    := NameSet.insert
-    addImportedFn := fun es => mkStateFromImportedEntries NameSet.insert {} es
-  }
-
-initialize registerTraceClass `myDebug
-
-syntax (name := insertFoo) "insert_foo " ident : command
-syntax (name := showFoo) "show_foo_set" : command
-
-open Lean.Elab
-open Lean.Elab.Command
-
-@[commandElab insertFoo] def elabInsertFoo : CommandElab := fun stx => do
-  trace[myDebug] "testing trace message at insert foo '{stx}'"
-  IO.println s!"inserting {stx[1].getId}"
-  modifyEnv fun env => fooExtension.addEntry env stx[1].getId
-
-@[commandElab showFoo] def elabShowFoo : CommandElab := fun stx => do
-  IO.println s!"foo set: {fooExtension.getState (← getEnv) |>.toList}"
diff --git a/tests/leanpkg/user_ext/UserExt/Tst1.lean b/tests/leanpkg/user_ext/UserExt/Tst1.lean
deleted file mode 100644
index 9c15cbfac203c..0000000000000
--- a/tests/leanpkg/user_ext/UserExt/Tst1.lean
+++ /dev/null
@@ -1,14 +0,0 @@
-import UserExt.FooExt
-import UserExt.BlaExt
-
-set_option trace.myDebug true
-
-insert_foo hello
-
-set_option trace.myDebug false
-
-insert_foo world
-show_foo_set
-
-insert_bla abc
-show_bla_set
diff --git a/tests/leanpkg/user_ext/UserExt/Tst2.lean b/tests/leanpkg/user_ext/UserExt/Tst2.lean
deleted file mode 100644
index c7743d2044b76..0000000000000
--- a/tests/leanpkg/user_ext/UserExt/Tst2.lean
+++ /dev/null
@@ -1,6 +0,0 @@
-import UserExt.BlaExt
-import UserExt.FooExt
-
-insert_foo test
-insert_bla defg
-insert_bla hij
diff --git a/tests/leanpkg/user_ext/leanpkg.toml b/tests/leanpkg/user_ext/leanpkg.toml
deleted file mode 100644
index 2606dd26d397e..0000000000000
--- a/tests/leanpkg/user_ext/leanpkg.toml
+++ /dev/null
@@ -1,3 +0,0 @@
-[package]
-name = "UserExt"
-version = "0.1"
diff --git a/tests/leanpkg/user_opt/.gitignore b/tests/leanpkg/user_opt/.gitignore
deleted file mode 100644
index 796b96d1c4023..0000000000000
--- a/tests/leanpkg/user_opt/.gitignore
+++ /dev/null
@@ -1 +0,0 @@
-/build
diff --git a/tests/leanpkg/user_opt/UserOpt.lean b/tests/leanpkg/user_opt/UserOpt.lean
deleted file mode 100644
index 6a4ef2093cf58..0000000000000
--- a/tests/leanpkg/user_opt/UserOpt.lean
+++ /dev/null
@@ -1,20 +0,0 @@
-import UserOpt.Opts
-
-open Lean
-
-def tst1 : MetaM Unit := do
-  assert! !(myBoolOpt.get (← getOptions))
-  assert! myNatOpt.get (← getOptions) == 100
-  pure ()
-
-#eval tst1
-
-set_option myBoolOpt true
-set_option myNatOpt 4
-
-def tst2 : MetaM Unit := do
-  assert! myBoolOpt.get (← getOptions)
-  assert! myNatOpt.get (← getOptions) == 4
-  pure ()
-
-#eval tst2
diff --git a/tests/leanpkg/user_opt/UserOpt/Opts.lean b/tests/leanpkg/user_opt/UserOpt/Opts.lean
deleted file mode 100644
index 9b656a13ebd43..0000000000000
--- a/tests/leanpkg/user_opt/UserOpt/Opts.lean
+++ /dev/null
@@ -1,11 +0,0 @@
-import Lean
-
-register_option myBoolOpt : Bool := {
-  defValue := false
-  descr    := "my Boolean option"
-}
-
-register_option myNatOpt : Nat := {
-  defValue := 100
-  descr    := "my Nat option"
-}
diff --git a/tests/leanpkg/user_opt/leanpkg.toml b/tests/leanpkg/user_opt/leanpkg.toml
deleted file mode 100644
index 3fdce28bf6f7a..0000000000000
--- a/tests/leanpkg/user_opt/leanpkg.toml
+++ /dev/null
@@ -1,3 +0,0 @@
-[package]
-name = "UserOpt"
-version = "0.1"