diff --git a/flake.nix b/flake.nix
index e9de8d915d..2315321c08 100644
--- a/flake.nix
+++ b/flake.nix
@@ -18,14 +18,14 @@
       # An old nixpkgs for creating releases with an old glibc
       pkgsDist-old-aarch = import inputs.nixpkgs-old { localSystem.config = "aarch64-unknown-linux-gnu"; };
 
-      lean-packages = pkgs.callPackage (./nix/packages.nix) { src = ./.; };
+      llvmPackages = pkgs.llvmPackages_15;
 
       devShellWithDist = pkgsDist: pkgs.mkShell.override {
-          stdenv = pkgs.overrideCC pkgs.stdenv lean-packages.llvmPackages.clang;
+          stdenv = pkgs.overrideCC pkgs.stdenv llvmPackages.clang;
         } ({
           buildInputs = with pkgs; [
             cmake gmp libuv ccache pkg-config
-            lean-packages.llvmPackages.llvm  # llvm-symbolizer for asan/lsan
+            llvmPackages.llvm  # llvm-symbolizer for asan/lsan
             gdb
             tree  # for CI
           ];
@@ -60,12 +60,6 @@
           GDB = pkgsDist.gdb;
         });
     in {
-      packages.${system} = {
-        # to be removed when Nix CI is not needed anymore
-        inherit (lean-packages) cacheRoots test update-stage0-commit ciShell;
-        deprecated = lean-packages;
-      };
-
       devShells.${system} = {
         # The default development shell for working on lean itself
         default = devShellWithDist pkgs;
diff --git a/nix/bareStdenv/setup b/nix/bareStdenv/setup
deleted file mode 100644
index 8ff2a2571a..0000000000
--- a/nix/bareStdenv/setup
+++ /dev/null
@@ -1,7 +0,0 @@
-set -eo pipefail
-
-for pkg in $buildInputs; do
-  export PATH=$PATH:$pkg/bin
-done
-
-: ${outputs:=out}
diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix
deleted file mode 100644
index dbcde3707b..0000000000
--- a/nix/bootstrap.nix
+++ /dev/null
@@ -1,208 +0,0 @@
-{ src, debug ? false, stage0debug ? false, extraCMakeFlags ? [],
-  stdenv, lib, cmake, pkg-config, gmp, libuv, cadical, git, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir, perl, gnused, darwin, llvmPackages, linkFarmFromDrvs,
-  ... } @ args:
-with builtins;
-lib.warn "The Nix-based build is deprecated" rec {
-  inherit stdenv;
-  sourceByRegex = p: rs: lib.sourceByRegex p (map (r: "(/src/)?${r}") rs);
-  buildCMake = args: stdenv.mkDerivation ({
-    nativeBuildInputs = [ cmake pkg-config ];
-    buildInputs = [ gmp libuv llvmPackages.llvm ];
-    # https://github.com/NixOS/nixpkgs/issues/60919
-    hardeningDisable = [ "all" ];
-    dontStrip = (args.debug or debug);
-
-    postConfigure = ''
-      patchShebangs .
-    '';
-  } // args // {
-    src = args.realSrc or (sourceByRegex args.src [ "[a-z].*" "CMakeLists\.txt" ]);
-    cmakeFlags = ["-DSMALL_ALLOCATOR=ON" "-DUSE_MIMALLOC=OFF"] ++ (args.cmakeFlags or [ "-DSTAGE=1" "-DPREV_STAGE=./faux-prev-stage" "-DUSE_GITHASH=OFF" "-DCADICAL=${cadical}/bin/cadical" ]) ++ (args.extraCMakeFlags or extraCMakeFlags) ++ lib.optional (args.debug or debug) [ "-DCMAKE_BUILD_TYPE=Debug" ];
-    preConfigure = args.preConfigure or "" + ''
-      # ignore absence of submodule
-      sed -i 's!lake/Lake.lean!!' CMakeLists.txt
-    '';
-  });
-  lean-bin-tools-unwrapped = buildCMake {
-    name = "lean-bin-tools";
-    outputs = [ "out" "leanc_src" ];
-    realSrc = sourceByRegex (src + "/src") [ "CMakeLists\.txt" "[a-z].*" ".*\.in" "Leanc\.lean" ];
-    dontBuild = true;
-    installPhase = ''
-      mkdir $out $leanc_src
-      mv bin/ include/ share/ $out/
-      mv leanc.sh $out/bin/leanc
-      mv leanc/Leanc.lean $leanc_src/
-      substituteInPlace $out/bin/leanc --replace '$root' "$out" --replace " sed " " ${gnused}/bin/sed "
-      substituteInPlace $out/bin/leanmake --replace "make" "${gnumake}/bin/make"
-      substituteInPlace $out/share/lean/lean.mk --replace "/usr/bin/env bash" "${bash}/bin/bash"
-    '';
-  };
-  leancpp = buildCMake {
-    name = "leancpp";
-    src = src + "/src";
-    buildFlags = [ "leancpp" "leanrt" "leanrt_initial-exec" "leanshell" "leanmain" ];
-    installPhase = ''
-      mkdir -p $out
-      mv lib/ $out/
-      mv runtime/libleanrt_initial-exec.a $out/lib
-    '';
-  };
-  stage0 = args.stage0 or (buildCMake {
-    name = "lean-stage0";
-    realSrc = src + "/stage0/src";
-    debug = stage0debug;
-    cmakeFlags = [ "-DSTAGE=0" ];
-    extraCMakeFlags = [];
-    preConfigure = ''
-      ln -s ${src + "/stage0/stdlib"} ../stdlib
-    '';
-    installPhase = ''
-      mkdir -p $out/bin $out/lib/lean
-      mv bin/lean $out/bin/
-      mv lib/lean/*.{so,dylib} $out/lib/lean
-    '';
-    meta.mainProgram = "lean";
-  });
-  stage = { stage, prevStage, self }:
-    let
-      desc = "stage${toString stage}";
-      build = args: buildLeanPackage.override {
-        lean = prevStage;
-        leanc = lean-bin-tools-unwrapped;
-        # use same stage for retrieving dependencies
-        lean-leanDeps = stage0;
-        lean-final = self;
-      } ({
-        src = src + "/src";
-        roots = [ { mod = args.name; glob = "andSubmodules"; } ];
-        fullSrc = src;
-        srcPath = "$PWD/src:$PWD/src/lake";
-        inherit debug;
-        leanFlags = [ "-DwarningAsError=true" ];
-      } // args);
-      Init' = build { name = "Init"; deps = []; };
-      Std' = build { name = "Std"; deps = [ Init' ]; };
-      Lean' = build { name = "Lean"; deps = [ Std' ]; };
-      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 = [ Std ]; };
-      Lake = build {
-        name = "Lake";
-        sharedLibName = "Lake_shared";
-        src = src + "/src/lake";
-        deps = [ Init Lean ];
-      };
-      Lake-Main = build {
-        name = "LakeMain";
-        roots = [{ glob = "one"; mod = "LakeMain"; }];
-        executableName = "lake";
-        deps = [ Lake ];
-        linkFlags = lib.optional stdenv.isLinux "-rdynamic";
-        src = src + "/src/lake";
-      };
-      stdlib = [ Init Std Lean Lake ];
-      modDepsFiles = symlinkJoin { name = "modDepsFiles"; paths = map (l: l.modDepsFile) (stdlib ++ [ Leanc ]); };
-      depRoots = symlinkJoin { name = "depRoots"; paths = map (l: l.depRoots) stdlib; };
-      iTree = symlinkJoin { name = "ileans"; paths = map (l: l.iTree) stdlib; };
-      Leanc = build { name = "Leanc"; src = lean-bin-tools-unwrapped.leanc_src; deps = stdlib; roots = [ "Leanc" ]; };
-      stdlibLinkFlags = "${lib.concatMapStringsSep " " (l: "-L${l.staticLib}") stdlib} -L${leancpp}/lib/lean";
-      libInit_shared = runCommand "libInit_shared" { buildInputs = [ stdenv.cc ]; libName = "libInit_shared${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
-        mkdir $out
-        touch empty.c
-        ${stdenv.cc}/bin/cc -shared -o $out/$libName empty.c
-      '';
-      leanshared_1 = runCommand "leanshared_1" { buildInputs = [ stdenv.cc ]; libName = "leanshared_1${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
-        mkdir $out
-        touch empty.c
-        ${stdenv.cc}/bin/cc -shared -o $out/$libName empty.c
-      '';
-      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 "-Wl,-Bsymbolic"} \
-          -Wl,--whole-archive ${leancpp}/lib/temp/libleanshell.a -lInit -lStd -lLean -lleancpp ${leancpp}/lib/libleanrt_initial-exec.a -Wl,--no-whole-archive -lstdc++ \
-          -lm ${stdlibLinkFlags} \
-          $(${llvmPackages.libllvm.dev}/bin/llvm-config --ldflags --libs) \
-          -o $out/$libName
-      '';
-      mods = foldl' (mods: pkg: mods // pkg.mods) {} stdlib;
-      print-paths = Lean.makePrintPathsFor [] mods;
-      leanc = writeShellScriptBin "leanc" ''
-        LEAN_CC=${stdenv.cc}/bin/cc ${Leanc.executable}/bin/leanc -I${lean-bin-tools-unwrapped}/include ${stdlibLinkFlags} -L${libInit_shared} -L${leanshared_1} -L${leanshared} -L${Lake.sharedLib} "$@"
-      '';
-      lean = runCommand "lean" { buildInputs = lib.optional stdenv.isDarwin darwin.cctools; } ''
-        mkdir -p $out/bin
-        ${leanc}/bin/leanc ${leancpp}/lib/temp/libleanmain.a ${libInit_shared}/* ${leanshared_1}/* ${leanshared}/* -o $out/bin/lean
-      '';
-      # derivation following the directory layout of the "basic" setup, mostly useful for running tests
-      lean-all = 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 stdlib)} ${libInit_shared}/* ${leanshared_1}/* ${leanshared}/* ${Lake.sharedLib}/* $out/lib/lean/
-          # put everything in a single final derivation so `IO.appDir` references work
-          cp ${lean}/bin/lean ${leanc}/bin/leanc ${Lake-Main.executable}/bin/lake $out/bin
-          # NOTE: `lndir` will not override existing `bin/leanc`
-          ${lndir}/bin/lndir -silent ${lean-bin-tools-unwrapped} $out
-        '';
-        meta.mainProgram = "lean";
-      };
-      cacheRoots = linkFarmFromDrvs "cacheRoots" ([
-        stage0 lean leanc lean-all iTree modDepsFiles depRoots Leanc.src
-      ] ++ map (lib: lib.oTree) stdlib);
-      test = buildCMake {
-        name = "lean-test-${desc}";
-        realSrc = lib.sourceByRegex src [ "src.*" "tests.*" ];
-        buildInputs = [ gmp libuv perl git cadical ];
-        preConfigure = ''
-          cd src
-        '';
-        extraCMakeFlags = [ "-DLLVM=OFF" ];
-        postConfigure = ''
-          patchShebangs ../../tests ../lake
-          rm -r bin lib include share
-          ln -sf ${lean-all}/* .
-        '';
-        buildPhase = ''
-         ctest --output-junit test-results.xml --output-on-failure -E 'leancomptest_(doc_example|foreign)|leanlaketest_reverse-ffi|leanruntest_timeIO' -j$NIX_BUILD_CORES
-        '';
-        installPhase = ''
-          mkdir $out
-          mv test-results.xml $out
-        '';
-      };
-      update-stage0 =
-        let cTree = symlinkJoin { name = "cs"; paths = map (lib: lib.cTree) (stdlib ++ [Lake-Main]); }; in
-        writeShellScriptBin "update-stage0" ''
-          CSRCS=${cTree} CP_C_PARAMS="--dereference --no-preserve=all" ${src + "/script/lib/update-stage0"}
-        '';
-      update-stage0-commit = writeShellScriptBin "update-stage0-commit" ''
-        set -euo pipefail
-        ${update-stage0}/bin/update-stage0
-        git commit -m "chore: update stage0"
-      '';
-      link-ilean = writeShellScriptBin "link-ilean" ''
-        dest=''${1:-src}
-        rm -rf $dest/build/lib || true
-        mkdir -p $dest/build/lib
-        ln -s ${iTree}/* $dest/build/lib
-      '';
-      benchmarks =
-        let
-          entries = attrNames (readDir (src + "/tests/bench"));
-          leanFiles = map (n: elemAt n 0) (filter (n: n != null) (map (match "(.*)\.lean") entries));
-        in lib.genAttrs leanFiles (n: (buildLeanPackage {
-          name = n;
-          src = filterSource (e: _: baseNameOf e == "${n}.lean") (src + "/tests/bench");
-        }).executable);
-    };
-  stage1 = stage { stage = 1; prevStage = stage0; self = stage1; };
-  stage2 = stage { stage = 2; prevStage = stage1; self = stage2; };
-  stage3 = stage { stage = 3; prevStage = stage2; self = stage3; };
-}
diff --git a/nix/buildLeanPackage.nix b/nix/buildLeanPackage.nix
deleted file mode 100644
index dc04bb7ffb..0000000000
--- a/nix/buildLeanPackage.nix
+++ /dev/null
@@ -1,247 +0,0 @@
-{ lean, lean-leanDeps ? lean, lean-final ? lean, leanc,
-  stdenv, lib, coreutils, gnused, writeShellScriptBin, bash, substituteAll, symlinkJoin, linkFarmFromDrvs,
-  runCommand, darwin, mkShell, ... }:
-let lean-final' = lean-final; in
-lib.makeOverridable (
-{ name, src, fullSrc ? src, srcPrefix ? "", srcPath ? "$PWD/${srcPrefix}",
-  # Lean dependencies. Each entry should be an output of buildLeanPackage.
-  deps ? [ lean.Init lean.Std lean.Lean ],
-  # Static library dependencies. Each derivation `static` should contain a static library in the directory `${static}`.
-  staticLibDeps ? [],
-  # Whether to wrap static library inputs in a -Wl,--start-group [...] -Wl,--end-group to ensure dependencies are resolved.
-  groupStaticLibs ? false,
-  # Shared library dependencies included at interpretation with --load-dynlib and linked to. Each derivation `shared` should contain a
-  # shared library at the path `${shared}/${shared.libName or shared.name}` and a name to link to like `-l${shared.linkName or shared.name}`.
-  # These libs are also linked to in packages that depend on this one.
-  nativeSharedLibs ? [],
-  # Lean modules to include.
-  # A set of Lean modules names as strings (`"Foo.Bar"`) or attrsets (`{ name = "Foo.Bar"; glob = "one" | "submodules" | "andSubmodules"; }`);
-  # see Lake README for glob meanings. Dependencies of selected modules are always included.
-  roots ? [ name ],
-  # Output from `lean --deps-json` on package source files. Persist the corresponding output attribute to a file and pass it back in here to avoid IFD.
-  # Must be refreshed on any change in `import`s or set of source file names.
-  modDepsFile ? null,
-  # Whether to compile each module into a native shared library that is loaded whenever the module is imported in order to accelerate evaluation
-  precompileModules ? false,
-  # Whether to compile the package into a native shared library that is loaded whenever *any* of the package's modules is imported into another package.
-  # If `precompileModules` is also `true`, the latter only affects imports within the current package.
-  precompilePackage ? precompileModules,
-  # Lean plugin dependencies. Each derivation `plugin` should contain a plugin library at path `${plugin}/${plugin.name}`.
-  pluginDeps ? [],
-  # `overrideAttrs` for `buildMod`
-  overrideBuildModAttrs ? null,
-  debug ? false, leanFlags ? [], leancFlags ? [], linkFlags ? [], executableName ? lib.toLower name, libName ? name, sharedLibName ? libName,
-  srcTarget ? "..#stage0", srcArgs ? "(\${args[*]})", lean-final ? lean-final' }@args:
-with builtins; let
-  # "Init.Core" ~> "Init/Core"
-  modToPath = mod: replaceStrings ["."] ["/"] mod;
-  modToAbsPath = mod: "${src}/${modToPath mod}";
-  # sanitize file name before copying to store, except when already in store
-  copyToStoreSafe = base: suffix: if lib.isDerivation base then base + suffix else
-    builtins.path { name = lib.strings.sanitizeDerivationName (baseNameOf suffix); path = base + suffix; };
-  modToLean = mod: copyToStoreSafe src "/${modToPath mod}.lean";
-  bareStdenv = ./bareStdenv;
-  mkBareDerivation = args: derivation (args // {
-    name = lib.strings.sanitizeDerivationName args.name;
-    stdenv = bareStdenv;
-    inherit (stdenv) system;
-    buildInputs = (args.buildInputs or []) ++ [ coreutils ];
-    builder = stdenv.shell;
-    args = [ "-c" ''
-      source $stdenv/setup
-      set -u
-      ${args.buildCommand}
-    '' ];
-  }) // { overrideAttrs = f: mkBareDerivation (lib.fix (lib.extends f (_: args))); };
-  runBareCommand = name: args: buildCommand: mkBareDerivation (args // { inherit name buildCommand; });
-  runBareCommandLocal = name: args: buildCommand: runBareCommand name (args // {
-    preferLocalBuild = true;
-    allowSubstitutes = false;
-  }) buildCommand;
-  mkSharedLib = name: args: runBareCommand "${name}-dynlib" {
-    buildInputs = [ stdenv.cc ] ++ lib.optional stdenv.isDarwin darwin.cctools;
-    libName = "${name}${stdenv.hostPlatform.extensions.sharedLibrary}";
-  } ''
-    mkdir -p $out
-    ${leanc}/bin/leanc -shared ${args} -o $out/$libName
-  '';
-  depRoot = name: deps: mkBareDerivation {
-    name = "${name}-depRoot";
-    inherit deps;
-    depRoots = map (drv: drv.LEAN_PATH) deps;
-
-    passAsFile = [ "deps" "depRoots" ];
-    buildCommand = ''
-      mkdir -p $out
-      for i in $(cat $depRootsPath); do
-        cp -dru --no-preserve=mode $i/. $out
-      done
-      for i in $(cat $depsPath); do
-        cp -drsu --no-preserve=mode $i/. $out
-      done
-    '';
-  };
-  srcRoot = src;
-
-  # A flattened list of Lean-module dependencies (`deps`)
-  allExternalDeps = lib.unique (lib.foldr (dep: allExternalDeps: allExternalDeps ++ [ dep ] ++ dep.allExternalDeps) [] deps);
-  allNativeSharedLibs =
-    lib.unique (lib.flatten (nativeSharedLibs ++ (map (dep: dep.allNativeSharedLibs or []) allExternalDeps)));
-
-  # A flattened list of all static library dependencies: this and every dep module's explicitly provided `staticLibDeps`,
-  # plus every dep module itself: `dep.staticLib`
-  allStaticLibDeps =
-    lib.unique (lib.flatten (staticLibDeps ++ (map (dep: [dep.staticLib] ++ dep.staticLibDeps or []) allExternalDeps)));
-
-  pathOfSharedLib = dep: dep.libPath or "${dep}/${dep.libName or dep.name}";
-
-  leanPluginFlags = lib.concatStringsSep " " (map (dep: "--plugin=${pathOfSharedLib dep}") pluginDeps);
-  loadDynlibsOfDeps = deps: lib.unique (concatMap (d: d.propagatedLoadDynlibs) deps);
-
-  # submodules "Init" = ["Init.List.Basic", "Init.Core", ...]
-  submodules = mod: let
-    dir = readDir (modToAbsPath mod);
-    f = p: t:
-      if t == "directory" then
-        submodules "${mod}.${p}"
-      else
-        let m = builtins.match "(.*)\.lean" p;
-        in lib.optional (m != null) "${mod}.${head m}";
-  in concatLists (lib.mapAttrsToList f dir);
-
-  # conservatively approximate list of source files matched by glob
-  expandGlobAllApprox = g:
-    if typeOf g == "string" then
-      # we can't know the required files without parsing dependencies (which is what we want this
-      # function for), so we approximate to the entire package.
-      let root = (head (split "\\." g));
-      in lib.optional (pathExists (src + "/${modToPath root}.lean")) root ++ lib.optionals (pathExists (modToAbsPath root)) (submodules root)
-    else if g.glob == "one" then expandGlobAllApprox g.mod
-    else if g.glob == "submodules" then submodules g.mod
-    else if g.glob == "andSubmodules" then [g.mod] ++ submodules g.mod
-    else throw "unknown glob kind '${g}'";
-  # list of modules that could potentially be involved in the build
-  candidateMods = lib.unique (concatMap expandGlobAllApprox roots);
-  candidateFiles = map modToLean candidateMods;
-  modDepsFile = args.modDepsFile or mkBareDerivation {
-    name = "${name}-deps.json";
-    candidateFiles = lib.concatStringsSep " " candidateFiles;
-    passAsFile = [ "candidateFiles" ];
-    buildCommand = ''
-      mkdir $out
-      ${lean-leanDeps}/bin/lean --deps-json --stdin < $candidateFilesPath > $out/$name
-    '';
-  };
-  modDeps = fromJSON (
-    # the only possible references to store paths in the JSON should be inside errors, so no chance of missed dependencies from this
-    unsafeDiscardStringContext (readFile "${modDepsFile}/${modDepsFile.name}"));
-  # map from module name to list of imports
-  modDepsMap = listToAttrs (lib.zipListsWith lib.nameValuePair candidateMods modDeps.imports);
-  maybeOverrideAttrs = f: x: if f != null then x.overrideAttrs f else x;
-  # build module (.olean and .c) given derivations of all (immediate) dependencies
-  # TODO: make `rec` parts override-compatible?
-  buildMod = mod: deps: maybeOverrideAttrs overrideBuildModAttrs (mkBareDerivation rec {
-    name = "${mod}";
-    LEAN_PATH = depRoot mod deps;
-    LEAN_ABORT_ON_PANIC = "1";
-    relpath = modToPath mod;
-    buildInputs = [ lean ];
-    leanPath = relpath + ".lean";
-    # should be either single .lean file or directory directly containing .lean file plus dependencies
-    src = copyToStoreSafe srcRoot ("/" + leanPath);
-    outputs = [ "out" "ilean" "c" ];
-    oleanPath = relpath + ".olean";
-    ileanPath = relpath + ".ilean";
-    cPath = relpath + ".c";
-    inherit leanFlags leanPluginFlags;
-    leanLoadDynlibFlags = map (p: "--load-dynlib=${pathOfSharedLib p}") (loadDynlibsOfDeps deps);
-    buildCommand = ''
-      dir=$(dirname $relpath)
-      mkdir -p $dir $out/$dir $ilean/$dir $c/$dir
-      if [ -d $src ]; then cp -r $src/. .; else cp $src $leanPath; fi
-      lean -o $out/$oleanPath -i $out/$ileanPath -c $c/$cPath $leanPath $leanFlags $leanPluginFlags $leanLoadDynlibFlags
-    '';
-  }) // {
-    inherit deps;
-    propagatedLoadDynlibs = loadDynlibsOfDeps deps;
-  };
-  compileMod = mod: drv: mkBareDerivation {
-    name = "${mod}-cc";
-    buildInputs = [ leanc stdenv.cc ];
-    hardeningDisable = [ "all" ];
-    oPath = drv.relpath + ".o";
-    inherit leancFlags;
-    buildCommand = ''
-      mkdir -p $out/$(dirname ${drv.relpath})
-      # make local "copy" so `drv`'s Nix store path doesn't end up in ccache's hash
-      ln -s ${drv.c}/${drv.cPath} src.c
-      # on the other hand, a debug build is pretty fast anyway, so preserve the path for gdb
-      leanc -c -o $out/$oPath $leancFlags -fPIC ${if debug then "${drv.c}/${drv.cPath} -g" else "src.c -O3 -DNDEBUG -DLEAN_EXPORTING"}
-    '';
-  };
-  mkMod = mod: deps:
-    let drv = buildMod mod deps;
-        obj = compileMod mod drv;
-        # this attribute will only be used if any dependent module is precompiled
-        sharedLib = mkSharedLib mod "${obj}/${obj.oPath} ${lib.concatStringsSep " " (map (d: pathOfSharedLib d.sharedLib) deps)}";
-    in drv // {
-      inherit obj sharedLib;
-    } // lib.optionalAttrs precompileModules {
-      propagatedLoadDynlibs = [sharedLib];
-    };
-  externalModMap = lib.foldr (dep: depMap: depMap // dep.mods) {} allExternalDeps;
-  # map from module name to derivation
-  modCandidates = mapAttrs (mod: header:
-    let
-      deps = if header.errors == []
-             then map (m: m.module) header.result.imports
-             else abort "errors while parsing imports of ${mod}:\n${lib.concatStringsSep "\n" header.errors}";
-    in mkMod mod (map (dep: if modDepsMap ? ${dep} then modCandidates.${dep} else externalModMap.${dep}) deps)) modDepsMap;
-  expandGlob = g:
-    if typeOf g == "string" then [g]
-    else if g.glob == "one" then [g.mod]
-    else if g.glob == "submodules" then submodules g.mod
-    else if g.glob == "andSubmodules" then [g.mod] ++ submodules g.mod
-    else throw "unknown glob kind '${g}'";
-  # subset of `modCandidates` that is transitively reachable from `roots`
-  mods' = listToAttrs (map (e: { name = e.key; value = modCandidates.${e.key}; }) (genericClosure {
-    startSet = map (m: { key = m; }) (concatMap expandGlob roots);
-    operator = e: if modDepsMap ? ${e.key} then map (m: { key = m.module; }) (filter (m: modCandidates ? ${m.module}) modDepsMap.${e.key}.result.imports) else [];
-  }));
-  allLinkFlags = lib.foldr (shared: acc: acc ++ [ "-L${shared}" "-l${shared.linkName or shared.name}" ]) linkFlags allNativeSharedLibs;
-
-  objects   = mapAttrs (_: m: m.obj) mods';
-  bintools = if stdenv.isDarwin then darwin.cctools else stdenv.cc.bintools.bintools;
-  staticLib = runCommand "${name}-lib" { buildInputs = [ bintools ]; } ''
-    mkdir -p $out
-    ar Trcs $out/lib${libName}.a ${lib.concatStringsSep " " (map (drv: "${drv}/${drv.oPath}") (attrValues objects))};
-  '';
-
-  staticLibLinkWrapper = libs: if groupStaticLibs && !stdenv.isDarwin
-    then "-Wl,--start-group ${libs} -Wl,--end-group"
-    else "${libs}";
-in rec {
-  inherit name lean deps staticLibDeps allNativeSharedLibs allLinkFlags allExternalDeps src objects staticLib modDepsFile;
-  mods = mapAttrs (_: m:
-      m //
-      # if neither precompilation option was set but a dependent module wants to be precompiled, default to precompiling this package whole
-      lib.optionalAttrs (precompilePackage || !precompileModules) { inherit sharedLib; } //
-      lib.optionalAttrs precompilePackage { propagatedLoadDynlibs = [sharedLib]; })
-    mods';
-  modRoot   = depRoot name (attrValues mods);
-  depRoots  = linkFarmFromDrvs "depRoots" (map (m: m.LEAN_PATH) (attrValues mods));
-  cTree     = symlinkJoin { name = "${name}-cTree"; paths = map (mod: mod.c) (attrValues mods); };
-  oTree     = symlinkJoin { name = "${name}-oTree"; paths = (attrValues objects); };
-  iTree     = symlinkJoin { name = "${name}-iTree"; paths = map (mod: mod.ilean) (attrValues mods); };
-  sharedLib = mkSharedLib "lib${sharedLibName}" ''
-    ${if stdenv.isDarwin then "-Wl,-force_load,${staticLib}/lib${libName}.a" else "-Wl,--whole-archive ${staticLib}/lib${libName}.a -Wl,--no-whole-archive"} \
-    ${lib.concatStringsSep " " (map (d: "${d.sharedLib}/*") deps)}'';
-  executable = lib.makeOverridable ({ withSharedStdlib ? true }: let
-      objPaths = map (drv: "${drv}/${drv.oPath}") (attrValues objects) ++ lib.optional withSharedStdlib "${lean-final.leanshared}/*";
-    in runCommand executableName { buildInputs = [ stdenv.cc leanc ]; } ''
-      mkdir -p $out/bin
-      leanc ${staticLibLinkWrapper (lib.concatStringsSep " " (objPaths ++ map (d: "${d}/*.a") allStaticLibDeps))} \
-        -o $out/bin/${executableName} \
-        ${lib.concatStringsSep " " allLinkFlags}
-    '') {};
-})
diff --git a/nix/lake-dev.in b/nix/lake-dev.in
deleted file mode 100644
index aa8a9f7101..0000000000
--- a/nix/lake-dev.in
+++ /dev/null
@@ -1,42 +0,0 @@
-#!@bash@/bin/bash
-
-set -euo pipefail
-
-function pebkac() {
-    echo 'This is just a simple Nix adapter for `lake print-paths|serve`.'
-    exit 1
-}
-
-[[ $# -gt 0 ]] || pebkac
-case $1 in
-    --version)
-        # minimum version for `lake serve` with fallback
-        echo 3.1.0
-        ;;
-    print-paths)
-        shift
-        deps="$@"
-        root=.
-        # fall back to initial package if not in package
-        [[ ! -f "$root/flake.nix" ]] && root="@srcRoot@"
-        target="$root#print-paths"
-        args=()
-        # HACK: use stage 0 instead of 1 inside Lean's own `src/`
-        [[ -d Lean && -f ../flake.nix ]] && target="@srcTarget@print-paths" && args=@srcArgs@
-        for dep in $deps; do
-            target="$target.\"$dep\""
-        done
-        echo "Building dependencies..." >&2
-        # -v only has "built ...", but "-vv" is a bit too verbose
-        exec @nix@/bin/nix run "$target" ${args[*]} -v
-        ;;
-    serve)
-        shift
-        [[ ${1:-} == "--" ]] && shift
-        # `link-ilean` puts them there
-        LEAN_PATH=${LEAN_PATH:+$LEAN_PATH:}$PWD/build/lib exec $(dirname $0)/lean --server "$@"
-        ;;
-    *)
-        pebkac
-        ;;
-esac
diff --git a/nix/lean-dev.in b/nix/lean-dev.in
deleted file mode 100644
index 909d66956e..0000000000
--- a/nix/lean-dev.in
+++ /dev/null
@@ -1,28 +0,0 @@
-#!@bash@/bin/bash
-
-set -euo pipefail
-
-root="."
-# find package root
-while [[ "$root" != / ]]; do
-    [ -f "$root/flake.nix" ] && break
-    root="$(realpath "$root/..")"
-done
-# fall back to initial package if not in package
-[[ ! -f "$root/flake.nix" ]] && root="@srcRoot@"
-
-# use Lean w/ package unless in server mode (which has its own LEAN_PATH logic)
-target="$root#lean-package"
-for arg in "$@"; do
-    case $arg in
-        --server | --worker | -v | --version)
-            target="$root#lean"
-            ;;
-    esac
-done
-
-args=(-- "$@")
-# HACK: use stage 0 instead of 1 inside Lean's own `src/`
-[[ -d Lean && -f ../flake.nix ]] && target="@srcTarget@" && args=@srcArgs@
-
-LEAN_SYSROOT="$(dirname "$0")/.." exec @nix@/bin/nix ${LEAN_NIX_ARGS:-} run "$target" ${args[*]}
diff --git a/nix/packages.nix b/nix/packages.nix
deleted file mode 100644
index c8e8bbe22f..0000000000
--- a/nix/packages.nix
+++ /dev/null
@@ -1,52 +0,0 @@
-{ src, pkgs, ... } @ args:
-with pkgs;
-let
-  # https://github.com/NixOS/nixpkgs/issues/130963
-  llvmPackages = if stdenv.isDarwin then llvmPackages_11 else llvmPackages_15;
-  cc = (ccacheWrapper.override rec {
-    cc = llvmPackages.clang;
-    extraConfig = ''
-      export CCACHE_DIR=/nix/var/cache/ccache
-      export CCACHE_UMASK=007
-      export CCACHE_BASE_DIR=$NIX_BUILD_TOP
-      # https://github.com/NixOS/nixpkgs/issues/109033
-      args=("$@")
-      for ((i=0; i<"''${#args[@]}"; i++)); do
-        case ''${args[i]} in
-          -frandom-seed=*) unset args[i]; break;;
-        esac
-      done
-      set -- "''${args[@]}"
-      [ -d $CCACHE_DIR ] || exec ${cc}/bin/$(basename "$0") "$@"
-    '';
-  }).overrideAttrs (old: {
-    # https://github.com/NixOS/nixpkgs/issues/119779
-    installPhase = builtins.replaceStrings ["use_response_file_by_default=1"] ["use_response_file_by_default=0"] old.installPhase;
-  });
-  stdenv' = if stdenv.isLinux then useGoldLinker stdenv else stdenv;
-  lean = callPackage (import ./bootstrap.nix) (args // {
-    stdenv = overrideCC stdenv' cc;
-    inherit src buildLeanPackage llvmPackages;
-  });
-  makeOverridableLeanPackage = f:
-    let newF = origArgs: f origArgs // {
-      overrideArgs = newArgs: makeOverridableLeanPackage f (origArgs // newArgs);
-    };
-    in lib.setFunctionArgs newF (lib.getFunctionArgs f) // {
-      override = args: makeOverridableLeanPackage (f.override args);
-    };
-  buildLeanPackage = makeOverridableLeanPackage (callPackage (import ./buildLeanPackage.nix) (args // {
-    inherit (lean) stdenv;
-    lean = lean.stage1;
-    inherit (lean.stage1) leanc;
-  }));
-in {
-  inherit cc buildLeanPackage llvmPackages;
-  nixpkgs = pkgs;
-  ciShell = writeShellScriptBin "ciShell" ''
-    set -o pipefail
-    export PATH=${moreutils}/bin:$PATH
-    # prefix lines with cumulative and individual execution time
-    "$@" |& ts -i "(%.S)]" | ts -s "[%M:%S"
-  '';
-} // lean.stage1
diff --git a/nix/templates/pkg/MyPackage.lean b/nix/templates/pkg/MyPackage.lean
deleted file mode 100644
index 75229fb67c..0000000000
--- a/nix/templates/pkg/MyPackage.lean
+++ /dev/null
@@ -1 +0,0 @@
-#eval "Hello, world!"
diff --git a/nix/templates/pkg/flake.nix b/nix/templates/pkg/flake.nix
deleted file mode 100644
index 42bf6f46b1..0000000000
--- a/nix/templates/pkg/flake.nix
+++ /dev/null
@@ -1,21 +0,0 @@
-{
-  description = "My Lean package";
-
-  inputs.lean.url = "github:leanprover/lean4";
-  inputs.flake-utils.url = "github:numtide/flake-utils";
-
-  outputs = { self, lean, flake-utils }: flake-utils.lib.eachDefaultSystem (system:
-    let
-      leanPkgs = lean.packages.${system};
-      pkg = leanPkgs.buildLeanPackage {
-        name = "MyPackage";  # must match the name of the top-level .lean file
-        src = ./.;
-      };
-    in {
-      packages = pkg // {
-        inherit (leanPkgs) lean;
-      };
-
-      defaultPackage = pkg.modRoot;
-    });
-}