chore: remove leanpkg

RELEASES.md

@@ -15,3 +15,5 @@ theorem dep_congr [DecidableEq ι] {p : ι → Set α} [∀ i, Inhabited (p i)]
 * [Partially applied congruence theorems.](https://github.com/leanprover/lean4/issues/988)
 
 * Improve elaboration postponement heuristic when expected type is a metavariable. Lean now reduces the expected type before performing the test.
+
+* [Remove deprecated leanpkg](https://github.com/leanprover/lean4/pull/985) in favor of [Lake](https://github.com/leanprover/lake) now bundled with Lean.

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`

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.

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,15 +122,14 @@ 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}";
         buildCommand = ''
           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
         '';

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; };

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

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 => pure <| 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"
         pure <| lakePath.withExtension System.FilePath.exeExtension
     let (headerEnv, msgLog) ← try
       if let some path := m.uri.toPath? then