Update Trace.lean

Co-authored-by: Gabriel Ebner <gebner@gebner.org>

.github/workflows/ci.yml

@@ -67,13 +67,13 @@ jobs:
             os: ubuntu-latest
             CMAKE_OPTIONS: -DCMAKE_BUILD_TYPE=Debug
             # exclude seriously slow tests
-            CTEST_OPTIONS: -E 'interactivetest|leanpkgtest|laketest'
+            CTEST_OPTIONS: -E 'interactivetest|leanpkgtest|laketest|benchtest'
           - name: Linux fsanitize
             os: ubuntu-latest
             # turn off custom allocator & symbolic functions to make LSAN do its magic
             CMAKE_OPTIONS: -DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined -DLEANC_EXTRA_FLAGS='-fsanitize=address,undefined -fsanitize-link-c++-runtime' -DSMALL_ALLOCATOR=OFF -DBSYMBOLIC=OFF
             # exclude seriously slow/problematic tests (laketests crash)
-            CTEST_OPTIONS: -E 'interactivetest|leanpkgtest|laketest'
+            CTEST_OPTIONS: -E 'interactivetest|leanpkgtest|laketest|benchtest'
           - name: macOS
             os: macos-latest
             release: true
@@ -105,7 +105,7 @@ jobs:
             binary-check: ldd
           - name: Linux aarch64
             os: ubuntu-latest
-            CMAKE_OPTIONS: -DCMAKE_PREFIX_PATH=$GMP -DLEAN_INSTALL_SUFFIX=-linux_aarch64
+            CMAKE_OPTIONS: -DUSE_GMP=OFF -DLEAN_INSTALL_SUFFIX=-linux_aarch64
             release: true
             cross: true
             shell: nix-shell --arg pkgsDist "import (fetchTarball \"channel:nixos-19.03\") {{ localSystem.config = \"aarch64-unknown-linux-gnu\"; }}" --run "bash -euxo pipefail {0}"

.gitmodules

@@ -1,4 +0,0 @@
-[submodule "lake"]
-        path = src/lake
-        url = https://github.com/leanprover/lake.git
-        ignore = untracked

README.md

@@ -1,5 +1,5 @@
-This is the repository for **Lean 4**, which is currently being released as milestone releases towards a first stable release.
-[Lean 3](https://github.com/leanprover/lean) is still the latest stable release.
+This is the repository for **Lean 4**, which is being actively developed and published as nightly releases.
+Stable point releases are planned for a later date after establishing a robust release process.
 
 # About
 

RELEASES.md

@@ -818,7 +818,7 @@ v4.0.0-m4 (23 March 2022)
 
   initialize my_ext : SimpExtension ← registerSimpAttr `my_simp "my own simp attribute"
   ```
-  If you don't neet to acces `my_ext`, you can also use the macro
+  If you don't need to access `my_ext`, you can also use the macro
   ```lean
   import Lean
 

doc/SUMMARY.md

@@ -4,6 +4,7 @@
 - [Tour of Lean](./tour.md)
 - [Setting Up Lean](./quickstart.md)
   - [Extended Setup Notes](./setup.md)
+  - [Nix Setup](./setup/nix.md)
 - [Theorem Proving in Lean](./tpil.md)
 - [Functional Programming in Lean](fplean.md)
 - [Examples](./examples.md)

doc/dev/index.md

@@ -57,3 +57,10 @@ You might find that debugging through elan, e.g. via `gdb lean`, disables some
 things like symbol autocompletion because at first only the elan proxy binary
 is loaded. You can instead pass the explicit path to `bin/lean` in your build
 folder to gdb, or use `gdb $(elan which lean)`.
+
+It is also possible to generate releases that others can use,
+simply by pushing a tag to your fork of the Lean 4 github repository
+(and waiting about an hour; check the `Actions` tab for completion).
+If you push `my-tag` to a fork in your github account `my_name`,
+you can then put `my_name/lean4:my-tag` in your `lean-toolchain` file in a project using `lake`.
+(You must use a tag name that does not start with a numeral, or contain `_`).

doc/make/nix.md

@@ -83,7 +83,7 @@ Work on two adjacent stages at the same time without the need for repeatedly upd
 ```bash
 # open an editor that will use only committed changes (so first commit them when changing files)
 nix run .#HEAD-as-stage1.emacs-dev&
-# open a second editor that will use those commited changes as stage 0
+# open a second editor that will use those committed changes as stage 0
 # (so don't commit changes done here until you are done and ran a final `update-stage0-commit`)
 nix run .#HEAD-as-stage0.emacs-dev&
 ```

doc/monads/applicatives.lean

@@ -212,7 +212,7 @@ so you get a nice zipped list like this:
 -- [(1, 4), (2, 5), (3, 6)]
 /-!
 
-And of couse, as you would expect, there is an `unzip` also:
+And of course, as you would expect, there is an `unzip` also:
 
 -/
 #eval List.unzip (List.zip [1, 2, 3] [4, 5, 6])
@@ -286,7 +286,7 @@ But you will need to understand full Monads before this will make sense.
 Diving a bit deeper, (you can skip this and jump to the [Applicative
 Laws](laws.lean.md#what-are-the-applicative-laws) if don't want to dive into this implementation detail right
 now). But, if you write a simple `Option` example `(.*.) <$> some 4 <*> some 5` that produces `some 20`
-using `Seq.seq` you will see somthing interesting:
+using `Seq.seq` you will see something interesting:
 
 -/
 #eval Seq.seq ((.*.) <$> some 4) (fun (_ : Unit) => some 5) -- some 20

doc/quickstart.md

@@ -18,9 +18,11 @@ See quick [walkthrough demo video](https://www.youtube.com/watch?v=yZo6k48L0VY).
 
     ```
     info: syncing channel updates for 'nightly'
-    info: latest update on nightly, lean version nightly-2021-12-05
+    info: latest update on nightly, lean version nightly-2023-06-27
     info: downloading component 'lean'
     ```
+    If there is no popup, you probably have Elan installed already.
+    You may want to make sure that your default toolchain is Lean 4 in this case by running `elan default leanprover/lean4:nightly` and reopen the file, as the next step will fail otherwise.
 
 1. While it is installing, you can paste the following Lean program into the new file:
 
@@ -37,6 +39,8 @@ You are set up!
 
 ## Create a Lean Project
 
+*If your goal is to contribute to [mathlib4](https://github.com/leanprover-community/mathlib4) or use it as a depdency, please see its readme for specific instructions on how to do that.*
+
 You can now create a Lean project in a new folder. Run `lake init foo` from "View > Terminal" to create a package, followed by `lake build` to get an executable version of your Lean program.
 On Linux/macOS, you first have to follow the instructions printed by the Lean installation or log out and in again for the Lean executables to be available in you terminal.
 

doc/setup.md

@@ -2,7 +2,7 @@
 
 ### Tier 1
 
-Platforms built & tested by our CI, available as nightly & stable releases via elan (see above)
+Platforms built & tested by our CI, available as nightly releases via elan (see below)
 
 * x86-64 Linux with glibc 2.27+
 * x86-64 macOS 10.15+
@@ -10,13 +10,13 @@ Platforms built & tested by our CI, available as nightly & stable releases via e
 
 ### Tier 2
 
-Platforms cross-compiled but not tested by our CI, available as nightly & stable releases
+Platforms cross-compiled but not tested by our CI, available as nightly releases
 
 Releases may be silently broken due to the lack of automated testing.
 Issue reports and fixes are welcome.
 
 * aarch64 Linux with glibc 2.27+
-* aarch64 (M1) macOS
+* aarch64 (Apple Silicon) macOS
 
 <!--
 ### Tier 3
@@ -26,26 +26,17 @@ Platforms that are known to work from manual testing, but do not come with CI or
 
 # Setting Up Lean
 
-There are currently two ways to set up a Lean 4 development environment:
-
-* [basic setup](./setup.md#basic-setup) (Linux/macOS/Windows): uses [`elan`](https://github.com/leanprover/elan) + your preinstalled editor
-* [Nix setup](./setup.md#nix-setup) (Linux/macOS/WSL): uses the [Nix](https://nixos.org/nix/) package manager for installing all dependencies localized to your project
-
-See also the [quickstart](./quickstart.md) instructions for using the basic setup with VS Code as the editor.
-
-## Basic Setup
+See also the [quickstart](./quickstart.md) instructions for a standard setup with VS Code as the editor.
 
 Release builds for all supported platforms are available at <https://github.com/leanprover/lean4/releases>.
 Instead of downloading these and setting up the paths manually, however, it is recommended to use the Lean version manager [`elan`](https://github.com/leanprover/elan) instead:
 ```sh
 $ elan self update  # in case you haven't updated elan in a while
-# download & activate latest Lean 4 release (https://github.com/leanprover/lean4/releases)
-$ elan default leanprover/lean4:stable
-# alternatively, use the latest nightly build (https://github.com/leanprover/lean4-nightly/releases)
+# download & activate latest Lean 4 nightly release (https://github.com/leanprover/lean4-nightly/releases)
 $ elan default leanprover/lean4:nightly
 ```
 
-### `lake`
+## `lake`
 
 Lean 4 comes with a package manager named `lake`.
 Use `lake init foo` to initialize a Lean package `foo` in the current directory, and `lake build` to typecheck and build it as well as all its dependencies. Use `lake help` to learn about further commands.
@@ -65,80 +56,8 @@ After running `lake build` you will see a binary named `./build/bin/foo` and whe
 Hello, world!
 ```
 
-### Editing
+## Editing
 
 Lean implements the [Language Server Protocol](https://microsoft.github.io/language-server-protocol/) that can be used for interactive development in [Emacs](https://github.com/leanprover/lean4-mode), [VS Code](https://github.com/leanprover-community/vscode-lean4), and possibly other editors.
 
 Changes must be saved to be visible in other files, which must then be invalidated using an editor command (see links above).
-
-## Nix Setup
-
-The alternative setup based on Nix provides a perfectly reproducible development environment for your project from the Lean version down to the editor and Lean extension.
-However, it is still experimental and subject to change; in particular, it is heavily based on an unreleased version of Nix enabling [Nix Flakes](https://www.tweag.io/blog/2020-05-25-flakes/). The setup has been tested on NixOS, other Linux distributions, and macOS.
-
-After installing (any version of) Nix (<https://nixos.org/download.html>), you can easily open a shell with the particular pre-release version of Nix needed by and tested with our setup (called the "Lean shell" from here on):
-```bash
-$ nix-shell https://github.com/leanprover/lean4/archive/master.tar.gz -A nix
-```
-While this shell is sufficient for executing the steps below, it is recommended to also set the following options in `/etc/nix/nix.conf` (`nix.extraOptions` in NixOS):
-```
-max-jobs = auto  # Allow building multiple derivations in parallel
-keep-outputs = true  # Do not garbage-collect build time-only dependencies (e.g. clang)
-# Allow fetching build results from the Lean Cachix cache
-trusted-substituters = https://lean4.cachix.org/
-trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= lean4.cachix.org-1:mawtxSxcaiWE24xCXXgh3qnvlTkyU7evRRnGeAhD4Wk=
-```
-On a multi-user installation of Nix (the default), you need to restart the Nix daemon afterwards:
-```bash
-sudo pkill nix-daemon
-```
-
-The [Cachix](https://cachix.org/) integration will magically beam any build steps already executed by the CI right onto your machine when calling Nix commands in the shell opened above.
-It can be set up analogously as a cache for your own project.
-
-Note: Your system Nix might print warnings about not knowing some of the settings used by the Lean shell Nix, which can be ignored.
-
-### Basic Commands
-
-From a Lean shell, run
-```bash
-$ 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 `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)
-$ nix run .#emacs-dev  # open a pinned version of Emacs with lean4-mode fully set up
-$ nix run .#emacs-dev MyPackage.lean  # arguments can be passed as well, e.g. the file to open
-$ nix run .#vscode-dev MyPackage.lean  # ditto, using VS Code
-```
-Note that if you rename `MyPackage.lean`, you also have to adjust the `name` attribute in `flake.nix` accordingly.
-Also note that if you turn the package into a Git repository, only tracked files will be visible to Nix.
-
-As in the basic setup, changes need to be saved to be visible in other files, which have then to be invalidated via an editor command.
-
-If you don't want to or cannot start the pinned editor from Nix, e.g. because you're running Lean inside WSL/a container/on a different machine, you can manually point your editor at the `lean` wrapper script the commands above use internally:
-```bash
-$ nix build .#lean-dev -o result-lean-dev
-```
-The resulting `./result-lean-dev/bin/lean` script essentially runs `nix run .#lean` in the current project's root directory when you open a Lean file or use the "refresh dependencies" command such that the correct Lean version for that project is executed.
-This includes selecting the correct stage of Lean (which it will compile on the fly, though without progress output) if you are [working on Lean itself](./make/nix.md#editor-integration).
-
-Package dependencies can be added as further input flakes and passed to the `deps` list of `buildLeanPackage`. Example: <https://github.com/Kha/testpkg2/blob/master/flake.nix#L5>
-
-For hacking, it can be useful to temporarily override an input with a local checkout/different version of a dependency:
-```bash
-$ nix build --override-input somedep path/to/somedep
-```
-
-On a build error, Nix will show the last 10 lines of the output by default. You can pass `-L` to `nix build` to show all lines, or pass the shown `*.drv` path to `nix log` to show the full log after the fact.
-
-Keeping all outputs ever built on a machine alive can accumulate to quite impressive amounts of disk space, so you might want to trigger the Nix GC when `/nix/store/` has grown too large:
-```bash
-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 `lakefile.lean` used in the basic setup.
-Unifying the two formats is TBD.

doc/setup/nix.md

@@ -0,0 +1,71 @@
+# Nix Setup
+
+An alternative setup based on Nix provides a perfectly reproducible development environment for your project from the Lean version down to the editor and Lean extension.
+However, it is still experimental and subject to change; in particular, it is heavily based on an unreleased version of Nix enabling [Nix Flakes](https://www.tweag.io/blog/2020-05-25-flakes/). The setup has been tested on NixOS, other Linux distributions, and macOS.
+
+After installing (any version of) Nix (<https://nixos.org/download.html>), you can easily open a shell with the particular pre-release version of Nix needed by and tested with our setup (called the "Lean shell" from here on):
+```bash
+$ nix-shell https://github.com/leanprover/lean4/archive/master.tar.gz -A nix
+```
+While this shell is sufficient for executing the steps below, it is recommended to also set the following options in `/etc/nix/nix.conf` (`nix.extraOptions` in NixOS):
+```
+max-jobs = auto  # Allow building multiple derivations in parallel
+keep-outputs = true  # Do not garbage-collect build time-only dependencies (e.g. clang)
+# Allow fetching build results from the Lean Cachix cache
+trusted-substituters = https://lean4.cachix.org/
+trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= lean4.cachix.org-1:mawtxSxcaiWE24xCXXgh3qnvlTkyU7evRRnGeAhD4Wk=
+```
+On a multi-user installation of Nix (the default), you need to restart the Nix daemon afterwards:
+```bash
+sudo pkill nix-daemon
+```
+
+The [Cachix](https://cachix.org/) integration will magically beam any build steps already executed by the CI right onto your machine when calling Nix commands in the shell opened above.
+It can be set up analogously as a cache for your own project.
+
+Note: Your system Nix might print warnings about not knowing some of the settings used by the Lean shell Nix, which can be ignored.
+
+## Basic Commands
+
+From a Lean shell, run
+```bash
+$ 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 standard setup, 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)
+$ nix run .#emacs-dev  # open a pinned version of Emacs with lean4-mode fully set up
+$ nix run .#emacs-dev MyPackage.lean  # arguments can be passed as well, e.g. the file to open
+$ nix run .#vscode-dev MyPackage.lean  # ditto, using VS Code
+```
+Note that if you rename `MyPackage.lean`, you also have to adjust the `name` attribute in `flake.nix` accordingly.
+Also note that if you turn the package into a Git repository, only tracked files will be visible to Nix.
+
+As in the standard setup, changes need to be saved to be visible in other files, which have then to be invalidated via an editor command.
+
+If you don't want to or cannot start the pinned editor from Nix, e.g. because you're running Lean inside WSL/a container/on a different machine, you can manually point your editor at the `lean` wrapper script the commands above use internally:
+```bash
+$ nix build .#lean-dev -o result-lean-dev
+```
+The resulting `./result-lean-dev/bin/lean` script essentially runs `nix run .#lean` in the current project's root directory when you open a Lean file or use the "refresh dependencies" command such that the correct Lean version for that project is executed.
+This includes selecting the correct stage of Lean (which it will compile on the fly, though without progress output) if you are [working on Lean itself](./make/nix.md#editor-integration).
+
+Package dependencies can be added as further input flakes and passed to the `deps` list of `buildLeanPackage`. Example: <https://github.com/Kha/testpkg2/blob/master/flake.nix#L5>
+
+For hacking, it can be useful to temporarily override an input with a local checkout/different version of a dependency:
+```bash
+$ nix build --override-input somedep path/to/somedep
+```
+
+On a build error, Nix will show the last 10 lines of the output by default. You can pass `-L` to `nix build` to show all lines, or pass the shown `*.drv` path to `nix log` to show the full log after the fact.
+
+Keeping all outputs ever built on a machine alive can accumulate to quite impressive amounts of disk space, so you might want to trigger the Nix GC when `/nix/store/` has grown too large:
+```bash
+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 `lakefile.lean` used in the standard setup.
+Unifying the two formats is TBD.

nix/bootstrap.nix

@@ -1,5 +1,5 @@
 { src, debug ? false, stage0debug ? false, extraCMakeFlags ? [],
-  stdenv, lib, cmake, gmp, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir, perl, gnused, darwin, llvmPackages, linkFarmFromDrvs,
+  stdenv, lib, cmake, gmp, git, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir, perl, gnused, darwin, llvmPackages, linkFarmFromDrvs,
   ... } @ args:
 with builtins;
 rec {
@@ -88,7 +88,7 @@ rec {
         src = src + "/src";
         roots = [ { mod = args.name; glob = "andSubmodules"; } ];
         fullSrc = src;
-        srcPrefix = "src";
+        srcPath = "$PWD/src:$PWD/src/lake";
         inherit debug;
       } // args);
       Init' = build { name = "Init"; deps = []; };
@@ -101,13 +101,25 @@ rec {
       inherit (Lean) emacs-dev emacs-package vscode-dev vscode-package;
       Init = attachSharedLib leanshared Init';
       Lean = attachSharedLib leanshared Lean' // { allExternalDeps = [ Init ]; };
-      stdlib = [ Init Lean ];
+      Lake = build {
+        name = "Lake";
+        src = src + "/src/lake";
+        deps = [ Init Lean ];
+      };
+      Lake-Main = build {
+        name = "Lake.Main";
+        roots = [ "Lake.Main" ];
+        executableName = "lake";
+        deps = [ Lake ];
+        linkFlags = lib.optional stdenv.isLinux "-rdynamic";
+        src = src + "/src/lake";
+      };
+      stdlib = [ Init 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; };
-      extlib = stdlib;  # TODO: add Lake
       Leanc = build { name = "Leanc"; src = lean-bin-tools-unwrapped.leanc_src; deps = stdlib; roots = [ "Leanc" ]; };
-      stdlibLinkFlags = "-L${Init.staticLib} -L${Lean.staticLib} -L${leancpp}/lib/lean";
+      stdlibLinkFlags = "-L${Init.staticLib} -L${Lean.staticLib} -L${Lake.staticLib} -L${leancpp}/lib/lean";
       leanshared = runCommand "leanshared" { buildInputs = [ stdenv.cc ]; libName = "libleanshared${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
         mkdir $out
         LEAN_CC=${stdenv.cc}/bin/cc ${lean-bin-tools-unwrapped}/bin/leanc -shared ${lib.optionalString stdenv.isLinux "-Wl,-Bsymbolic"} \
@@ -116,7 +128,8 @@ rec {
           $(${llvmPackages.libllvm.dev}/bin/llvm-config --ldflags --libs) \
           -o $out/$libName
       '';
-      mods = Init.mods // Lean.mods;
+      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${leanshared} "$@"
       '';
@@ -129,9 +142,9 @@ rec {
         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/
+          ln -sf ${leancpp}/lib/lean/* ${lib.concatMapStringsSep " " (l: "${l.modRoot}/* ${l.staticLib}/*") (lib.reverseList stdlib)} ${leanshared}/* $out/lib/lean/
           # put everything in a single final derivation so `IO.appDir` references work
-          cp ${lean}/bin/lean ${leanc}/bin/leanc $out/bin
+          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
         '';
@@ -140,30 +153,30 @@ rec {
       cacheRoots = linkFarmFromDrvs "cacheRoots" [
         stage0 lean leanc lean-all iTree modDepsFiles depRoots Leanc.src
         # .o files are not a runtime dependency on macOS because of lack of thin archives
-        Lean.oTree
+        Lean.oTree Lake.oTree
       ];
       test = buildCMake {
         name = "lean-test-${desc}";
         realSrc = lib.sourceByRegex src [ "src.*" "tests.*" ];
-        buildInputs = [ gmp perl ];
+        buildInputs = [ gmp perl git ];
         preConfigure = ''
           cd src
         '';
         extraCMakeFlags = [ "-DLLVM=OFF" ];
         postConfigure = ''
-          patchShebangs ../../tests
+          patchShebangs ../../tests ../lake
           rm -r bin lib include share
           ln -sf ${lean-all}/* .
         '';
         buildPhase = ''
-          ctest --output-on-failure -E 'leancomptest_(doc_example|foreign)|laketest|leanpkgtest' -j$NIX_BUILD_CORES
+          ctest --output-on-failure -E 'leancomptest_(doc_example|foreign)' -j$NIX_BUILD_CORES
         '';
         installPhase = ''
           touch $out
         '';
       };
       update-stage0 =
-        let cTree = symlinkJoin { name = "cs"; paths = map (l: l.cTree) stdlib; }; in
+        let cTree = symlinkJoin { name = "cs"; paths = [ Init.cTree Lean.cTree ]; }; in
         writeShellScriptBin "update-stage0" ''
           CSRCS=${cTree} CP_C_PARAMS="--dereference --no-preserve=all" ${src + "/script/update-stage0"}
         '';

nix/buildLeanPackage.nix

@@ -3,7 +3,7 @@
   runCommand, darwin, mkShell, ... }:
 let lean-final' = lean-final; in
 lib.makeOverridable (
-{ name, src, fullSrc ? src, srcPrefix ? "",
+{ name, src, fullSrc ? src, srcPrefix ? "", srcPath ? "$PWD/${srcPrefix}",
   # Lean dependencies. Each entry should be an output of buildLeanPackage.
   deps ? [ lean.Lean ],
   # Static library dependencies. Each derivation `static` should contain a static library in the directory `${static}`.
@@ -210,7 +210,6 @@ with builtins; let
       loadDynlibPaths = map pathOfSharedLib (loadDynlibsOfDeps deps);
     }}'
   '';
-  makePrintPathsFor = deps: mods: printPaths deps // mapAttrs (_: mod: makePrintPathsFor (deps ++ [mod]) mods) mods;
   expandGlob = g:
     if typeOf g == "string" then [g]
     else if g.glob == "one" then [g.mod]
@@ -270,6 +269,7 @@ in rec {
     ln -sf ${iTree}/* $dest/build/lib
   '';
 
+  makePrintPathsFor = deps: mods: printPaths deps // mapAttrs (_: mod: makePrintPathsFor (deps ++ [mod]) mods) mods;
   print-paths = makePrintPathsFor [] (mods' // externalModMap);
   # `lean` wrapper that dynamically runs Nix for the actual `lean` executable so the same editor can be
   # used for multiple projects/after upgrading the `lean` input/for editing both stage 1 and the tests
@@ -297,7 +297,7 @@ in rec {
   devShell = mkShell {
     buildInputs = [ nix ];
     shellHook = ''
-      export LEAN_SRC_PATH="$PWD/${srcPrefix}"
+      export LEAN_SRC_PATH="${srcPath}"
     '';
   };
 })

script/prepare-llvm-macos.sh

@@ -34,8 +34,11 @@ $CP llvm/lib/clang/*/include/{std*,__std*,limits}.h stage1/include/clang
 (cd llvm; $CP --parents lib/clang/*/lib/*/libclang_rt.osx.a ../stage1)
 # libSystem stub, includes libc
 cp $SDK/usr/lib/libSystem.tbd stage1/lib/libc
-# use for linking, use system libs for running
-gcp llvm/lib/lib{c++,c++abi,unwind}.dylib stage1/lib/libc
+# use for linking, use system lib for running
+gcp llvm/lib/libc++.dylib stage1/lib/libc
+# make sure we search for the library in /usr/lib instead of the rpath, which should not contain `/usr/lib`
+# and apparently since Sonoma does not do so implicitly either
+install_name_tool -id /usr/lib/libc++.dylib stage1/lib/libc/libc++.dylib
 echo -n " -DLLVM=ON -DLLVM_CONFIG=$PWD/llvm-host/bin/llvm-config" # manually point to `llvm-config` location
 echo -n " -DLEAN_STANDALONE=ON"
 # do not change C++ compiler; libc++ etc. being system libraries means there's no danger of conflicts,

script/update-stage0

@@ -3,8 +3,8 @@ set -euo pipefail
 
 rm -r stage0 || true
 # don't copy untracked files
-for f in $(git ls-files src); do
-    [[ $f != src/lake && $f != src/Leanc.lean ]] || continue
+# `:!` is git glob flavor for exclude patterns
+for f in $(git ls-files src ':!:src/lake/*' ':!:src/Leanc.lean'); do
     if [[ $f == *.lean ]]; then
         f=${f#src/}
         f=${f%.lean}.c

src/CMakeLists.txt

@@ -293,7 +293,7 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
     find_package(ZLIB REQUIRED)
     message(STATUS "ZLIB_LIBRARY: ${ZLIB_LIBRARY}")
     cmake_path(GET ZLIB_LIBRARY PARENT_PATH ZLIB_LIBRARY_PARENT_PATH)
-    string(APPEND LEAN_EXTRA_LINKER_FLAGS " -L ${ZLIB_LIBRARY_PARENT_PATH}")
+    string(APPEND LEANSHARED_LINKER_FLAGS " -L ${ZLIB_LIBRARY_PARENT_PATH}")
   endif()
   string(APPEND LEANC_STATIC_LINKER_FLAGS " -lleancpp -lInit -lLean -lleanrt")
 elseif(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
@@ -301,6 +301,7 @@ elseif(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
 else()
   string(APPEND LEANC_STATIC_LINKER_FLAGS " -Wl,--start-group -lleancpp -lLean -Wl,--end-group -Wl,--start-group -lInit -lleanrt -Wl,--end-group")
 endif()
+string(APPEND LEANC_STATIC_LINKER_FLAGS " -lLake")
 
 set(LEAN_CXX_STDLIB "-lstdc++" CACHE STRING "C++ stdlib linker flags")
 

src/Init/Core.lean

@@ -1480,7 +1480,7 @@ end
 
 section Exact
 
-variable   {α : Sort u}
+variable {α : Sort u}
 
 private def rel {s : Setoid α} (q₁ q₂ : Quotient s) : Prop :=
   Quotient.liftOn₂ q₁ q₂

src/Init/Data/Array/Basic.lean

@@ -269,7 +269,15 @@ unsafe def mapMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad
 /-- Reference implementation for `mapM` -/
 @[implemented_by mapMUnsafe]
 def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (as : Array α) : m (Array β) :=
-  as.foldlM (fun bs a => do let b ← f a; pure (bs.push b)) (mkEmpty as.size)
+  -- Note: we cannot use `foldlM` here for the reference implementation because this calls
+  -- `bind` and `pure` too many times. (We are not assuming `m` is a `LawfulMonad`)
+  let rec map (i : Nat) (r : Array β) : m (Array β) := do
+    if hlt : i < as.size then
+      map (i+1) (r.push (← f as[i]))
+    else
+      pure r
+  map 0 (mkEmpty as.size)
+termination_by map => as.size - i
 
 @[inline]
 def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : Fin as.size → α → m β) : m (Array β) :=

src/Init/Data/Hashable.lean

@@ -58,3 +58,7 @@ instance : Hashable Int where
 
 instance (P : Prop) : Hashable P where
   hash _ := 0
+
+/-- An opaque (low-level) hash operation used to implement hashing for pointers. -/
+@[always_inline, inline] def hash64 (u : UInt64) : UInt64 :=
+  mixHash u 11

src/Init/Data/Int/Basic.lean

@@ -269,8 +269,8 @@ def natAbs (m : @& Int) : Nat :=
 
   #eval (12 : Int) / (7 : Int) -- 1
   #eval (12 : Int) / (-7 : Int) -- -1
-  #eval (-12 : Int) / (7 : Int) -- -2
-  #eval (-12 : Int) / (-7 : Int) -- 2
+  #eval (-12 : Int) / (7 : Int) -- -1
+  #eval (-12 : Int) / (-7 : Int) -- 1
   ```
 
   Implemented by efficient native code. -/

src/Init/Data/String/Basic.lean

@@ -247,7 +247,7 @@ termination_by _ => s.endPos.1 - i.1
 
 def splitOnAux (s sep : String) (b : Pos) (i : Pos) (j : Pos) (r : List String) : List String :=
   if h : s.atEnd i then
-    let r := if sep.atEnd j then ""::(s.extract b (i - j))::r else (s.extract b i)::r
+    let r := (s.extract b i)::r
     r.reverse
   else
     have := Nat.sub_lt_sub_left (Nat.gt_of_not_le (mt decide_eq_true h)) (lt_next s _)

src/Init/NotationExtra.lean

@@ -65,7 +65,7 @@ syntax unifConstraint := term patternIgnore(" =?= " <|> " ≟ ") term
 syntax unifConstraintElem := colGe unifConstraint ", "?
 
 syntax (docComment)? attrKind "unif_hint" (ppSpace ident)? (ppSpace bracketedBinder)*
-  " where " withPosition(unifConstraintElem*) patternIgnore("|-" <|> "⊢ ") unifConstraint : command
+  " where " withPosition(unifConstraintElem*) patternIgnore(atomic("|" noWs "-") <|> "⊢") unifConstraint : command
 
 macro_rules
   | `($[$doc?:docComment]? $kind:attrKind unif_hint $(n)? $bs* where $[$cs₁ ≟ $cs₂]* |- $t₁ ≟ $t₂) => do

src/Init/Prelude.lean

@@ -608,7 +608,7 @@ parameter.
 
 For example, the `Coe` class is defined as:
 ```
-class Coe (α : semiOutParam (Type u)) (β : Type v)
+class Coe (α : semiOutParam (Sort u)) (β : Sort v)
 ```
 This means that all `Coe` instances should provide a concrete value for `α`
 (i.e., not an assignable metavariable). An instance like `Coe Nat Int` or `Coe
@@ -1471,7 +1471,7 @@ set_option bootstrap.genMatcherCode false in
 /--
 The power operation on natural numbers.
 
-This definition is overridden in the compiler to efficiently
+This definition is overridden in both the kernel and the compiler to efficiently
 evaluate using the "bignum" representation (see `Nat`). The definition provided
 here is the logical model.
 -/

src/Init/SimpLemmas.lean

@@ -156,3 +156,6 @@ theorem Bool.or_assoc (a b c : Bool) : (a || b || c) = (a || (b || c)) := by
 
 @[simp] theorem decide_False : decide False = false := rfl
 @[simp] theorem decide_True : decide True = true := rfl
+
+@[simp] theorem bne_iff_ne [BEq α] [LawfulBEq α] (a b : α) : a != b ↔ a ≠ b := by
+  simp [bne]; rw [← beq_iff_eq a b]; simp [-beq_iff_eq]

src/Init/SizeOfLemmas.lean

@@ -8,26 +8,26 @@ import Init.Meta
 import Init.SizeOf
 import Init.Data.Nat.Linear
 
-@[simp] theorem Fin.sizeOf (a : Fin n) : sizeOf a = a.val + 1 := by
+@[simp] protected theorem Fin.sizeOf (a : Fin n) : sizeOf a = a.val + 1 := by
   cases a; simp_arith
 
-@[simp] theorem UInt8.sizeOf (a : UInt8) : sizeOf a = a.toNat + 2 := by
+@[simp] protected theorem UInt8.sizeOf (a : UInt8) : sizeOf a = a.toNat + 2 := by
   cases a; simp_arith [UInt8.toNat]
 
-@[simp] theorem UInt16.sizeOf (a : UInt16) : sizeOf a = a.toNat + 2 := by
+@[simp] protected theorem UInt16.sizeOf (a : UInt16) : sizeOf a = a.toNat + 2 := by
   cases a; simp_arith [UInt16.toNat]
 
-@[simp] theorem UInt32.sizeOf (a : UInt32) : sizeOf a = a.toNat + 2 := by
+@[simp] protected theorem UInt32.sizeOf (a : UInt32) : sizeOf a = a.toNat + 2 := by
   cases a; simp_arith [UInt32.toNat]
 
-@[simp] theorem UInt64.sizeOf (a : UInt64) : sizeOf a = a.toNat + 2 := by
+@[simp] protected theorem UInt64.sizeOf (a : UInt64) : sizeOf a = a.toNat + 2 := by
   cases a; simp_arith [UInt64.toNat]
 
-@[simp] theorem USize.sizeOf (a : USize) : sizeOf a = a.toNat + 2 := by
+@[simp] protected theorem USize.sizeOf (a : USize) : sizeOf a = a.toNat + 2 := by
   cases a; simp_arith [USize.toNat]
 
-@[simp] theorem Char.sizeOf (a : Char) : sizeOf a = a.toNat + 3 := by
+@[simp] protected theorem Char.sizeOf (a : Char) : sizeOf a = a.toNat + 3 := by
   cases a; simp_arith [Char.toNat]
 
-@[simp] theorem Subtype.sizeOf {α : Sort u_1} {p : α → Prop} (s : Subtype p) : sizeOf s = sizeOf s.val + 1 := by
+@[simp] protected theorem Subtype.sizeOf {α : Sort u_1} {p : α → Prop} (s : Subtype p) : sizeOf s = sizeOf s.val + 1 := by
   cases s; simp_arith

src/Init/System/IO.lean

@@ -294,6 +294,14 @@ end Handle
 @[extern "lean_io_remove_dir"] opaque removeDir : @& FilePath → IO Unit
 @[extern "lean_io_create_dir"] opaque createDir : @& FilePath → IO Unit
 
+/--
+Moves a file or directory `old` to the new location `new`.
+
+This function coincides with the [POSIX `rename` function](https://pubs.opengroup.org/onlinepubs/9699919799/functions/rename.html),
+see there for more information.
+-/
+@[extern "lean_io_rename"] opaque rename (old new : @& FilePath) : IO Unit
+
 end FS
 
 @[extern "lean_io_getenv"] opaque getEnv (var : @& String) : BaseIO (Option String)
@@ -536,6 +544,8 @@ structure SpawnArgs extends StdioConfig where
   cwd : Option FilePath := none
   /-- Add or remove environment variables for the process. -/
   env : Array (String × Option String) := #[]
+  /-- Start process in new session and process group using `setsid`. Currently a no-op on non-POSIX platforms. -/
+  setsid : Bool := false
 
 -- TODO(Sebastian): constructor must be private
 structure Child (cfg : StdioConfig) where
@@ -547,6 +557,10 @@ structure Child (cfg : StdioConfig) where
 
 @[extern "lean_io_process_child_wait"] opaque Child.wait {cfg : @& StdioConfig} : @& Child cfg → IO UInt32
 
+/-- Terminates the child process using the SIGTERM signal or a platform analogue.
+    If the process was started using `SpawnArgs.setsid`, terminates the entire process group instead. -/
+@[extern "lean_io_process_child_kill"] opaque Child.kill {cfg : @& StdioConfig} : @& Child cfg → IO Unit
+
 /--
 Extract the `stdin` field from a `Child` object, allowing them to be freed independently.
 This operation is necessary for closing the child process' stdin while still holding on to a process handle,

src/Init/Tactics.lean

@@ -304,7 +304,7 @@ syntax locationWildcard := " *"
 A hypothesis location specification consists of 1 or more hypothesis references
 and optionally `⊢` denoting the goal.
 -/
-syntax locationHyp := (ppSpace colGt term:max)+ ppSpace patternIgnore("⊢" <|> "|-")?
+syntax locationHyp := (ppSpace colGt term:max)+ ppSpace patternIgnore( atomic("|" noWs "-") <|> "⊢")?
 
 /--
 Location specifications are used by many tactics that can operate on either the

src/Init/WF.lean

@@ -184,15 +184,9 @@ protected theorem caseStrongInductionOn
 
 end Nat
 
-def Measure {α : Sort u} : (α → Nat) → α → α → Prop :=
-  InvImage (fun a b => a < b)
-
 abbrev measure {α : Sort u} (f : α → Nat) : WellFoundedRelation α :=
   invImage f Nat.lt_wfRel
 
-def SizeOfRef (α : Sort u) [SizeOf α] : α → α → Prop :=
-  Measure sizeOf
-
 abbrev sizeOfWFRel {α : Sort u} [SizeOf α] : WellFoundedRelation α :=
   measure sizeOf
 

src/Lean/Compiler/IR/Checker.lean

@@ -16,6 +16,10 @@ def maxCtorFields := getMaxCtorFields ()
 opaque getMaxCtorScalarsSize : Unit → Nat
 def maxCtorScalarsSize := getMaxCtorScalarsSize ()
 
+@[extern c inline "lean_box(LeanMaxCtorTag)"]
+opaque getMaxCtorTag : Unit → Nat
+def maxCtorTag := getMaxCtorTag ()
+
 @[extern c inline "lean_box(sizeof(size_t))"]
 opaque getUSizeSize : Unit → Nat
 def usizeSize := getUSizeSize ()
@@ -113,6 +117,8 @@ def checkExpr (ty : IRType) : Expr → M Unit
   | Expr.ap x ys            => checkObjVar x *> checkArgs ys
   | Expr.fap f ys           => checkFullApp f ys
   | Expr.ctor c ys          => do
+    if c.cidx > maxCtorTag && (c.size > 0 || c.usize > 0 || c.ssize > 0) then
+      throw s!"tag for constructor '{c.name}' is too big, this is a limitation of the current runtime"
     if c.size > maxCtorFields then
       throw s!"constructor '{c.name}' has too many fields"
     if c.ssize + c.usize * usizeSize > maxCtorScalarsSize then
@@ -175,7 +181,7 @@ end Checker
 def checkDecl (decls : Array Decl) (decl : Decl) : CompilerM Unit := do
   let env ← getEnv
   match (Checker.checkDecl decl { env := env, decls := decls }).run' {} with
-  | .error msg => throw s!"IR check failed at '{decl.name}', error: {msg}"
+  | .error msg => throw s!"compiler IR check failed at '{decl.name}', error: {msg}"
   | _ => pure ()
 
 def checkDecls (decls : Array Decl) : CompilerM Unit :=

src/Lean/Compiler/IR/EmitC.lean

@@ -687,9 +687,13 @@ def emitDeclInit (d : Decl) : M Unit := do
   let env ← getEnv
   let n := d.name
   if isIOUnitInitFn env n then
+    if isIOUnitBuiltinInitFn env n then
+      emit "if (builtin) {"
     emit "res = "; emitCName n; emitLn "(lean_io_mk_world());"
     emitLn "if (lean_io_result_is_error(res)) return res;"
     emitLn "lean_dec_ref(res);"
+    if isIOUnitBuiltinInitFn env n then
+      emit "}"
   else if d.params.size == 0 then
     match getInitFnNameFor? env d.name with
     | some initFn =>

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -415,24 +415,38 @@ def emitFnDeclAux (mod : LLVM.Module llvmctx)
   let env ← getEnv
   -- bollu: if we have a declaration with no parameters, then we emit it as a global pointer.
   -- bollu: Otherwise, we emit it as a function
+  let global ←
+    if ps.isEmpty then
+        let retty ← (toLLVMType decl.resultType)
+        let global ← LLVM.getOrAddGlobal mod cppBaseName retty
+        if !isExternal then
+          LLVM.setInitializer global (← LLVM.getUndef retty)
+        pure global
+    else
+        let retty ← (toLLVMType decl.resultType)
+        let mut argtys := #[]
+        for p in ps do
+          -- if it is extern, then we must not add irrelevant args
+          if !(isExternC env decl.name) || !p.ty.isIrrelevant then
+            argtys := argtys.push (← toLLVMType p.ty)
+        -- TODO (bollu): simplify this API, this code of `closureMaxArgs` is duplicated in multiple places.
+        if argtys.size > closureMaxArgs && isBoxedName decl.name then
+          argtys := #[← LLVM.pointerType (← LLVM.voidPtrType llvmctx)]
+        let fnty ← LLVM.functionType retty argtys (isVarArg := false)
+        LLVM.getOrAddFunction mod cppBaseName fnty
+  -- we must now set symbol visibility for global.
   if ps.isEmpty then
-      let retty ← (toLLVMType decl.resultType)
-      let global ← LLVM.getOrAddGlobal mod cppBaseName retty
-      if !isExternal then
-        LLVM.setInitializer global (← LLVM.getUndef retty)
-      return global
-  else
-      let retty ← (toLLVMType decl.resultType)
-      let mut argtys := #[]
-      for p in ps do
-        -- if it is extern, then we must not add irrelevant args
-        if !(isExternC env decl.name) || !p.ty.isIrrelevant then
-          argtys := argtys.push (← toLLVMType p.ty)
-      -- TODO (bollu): simplify this API, this code of `closureMaxArgs` is duplicated in multiple places.
-      if argtys.size > closureMaxArgs && isBoxedName decl.name then
-        argtys := #[← LLVM.pointerType (← LLVM.voidPtrType llvmctx)]
-      let fnty ← LLVM.functionType retty argtys (isVarArg := false)
-      LLVM.getOrAddFunction mod cppBaseName fnty
+    if isClosedTermName env decl.name then LLVM.setVisibility global LLVM.Visibility.hidden -- static
+    else if isExternal then pure () -- extern (Recall that C/LLVM funcs are extern linkage by default.)
+    else LLVM.setDLLStorageClass global LLVM.DLLStorageClass.export  -- LEAN_EXPORT
+  else if !isExternal
+    -- An extern decl might be linked in from a different translation unit.
+    -- Thus, we cannot export an external declaration as we do not define it,
+    -- only declare its presence.
+    -- So, we only export non-external definitions.
+    then LLVM.setDLLStorageClass global LLVM.DLLStorageClass.export
+  return global
+
 
 def emitFnDecl (decl : Decl) (isExternal : Bool) : M llvmctx Unit := do
   let cppBaseName ← toCName decl.name
@@ -1137,6 +1151,14 @@ def emitDeclAux (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) (d
           argtys := argtys.push (← toLLVMType x.ty)
       let fnty ← LLVM.functionType retty argtys (isVarArg := false)
       let llvmfn ← LLVM.getOrAddFunction mod name fnty
+      -- set linkage and visibility
+      -- TODO: consider refactoring these into a separate concept (e.g. 'setLinkageAndVisibility')
+      --       Find the spots where this refactor needs to happen by grepping for 'LEAN_EXPORT'
+      --       in the C backend
+      if xs.size == 0 then
+        LLVM.setVisibility llvmfn LLVM.Visibility.hidden -- "static "
+      else
+        LLVM.setDLLStorageClass llvmfn LLVM.DLLStorageClass.export  -- LEAN_EXPORT: make symbol visible to the interpreter
       withReader (fun llvmctx => { llvmctx with mainFn := f, mainParams := xs }) do
         set { var2val := default, jp2bb := default : EmitLLVM.State llvmctx } -- flush variable map
         let bb ← LLVM.appendBasicBlockInContext llvmctx llvmfn "entry"
@@ -1247,10 +1269,12 @@ def emitInitFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M
 
   let initFnTy ← LLVM.functionType (← LLVM.voidPtrType llvmctx) #[ (← LLVM.i8Type llvmctx), (← LLVM.voidPtrType llvmctx)] (isVarArg := false)
   let initFn ← LLVM.getOrAddFunction mod (mkModuleInitializationFunctionName modName) initFnTy
+  LLVM.setDLLStorageClass initFn LLVM.DLLStorageClass.export  -- LEAN_EXPORT
   let entryBB ← LLVM.appendBasicBlockInContext llvmctx initFn "entry"
   LLVM.positionBuilderAtEnd builder entryBB
   let ginit?ty := ← LLVM.i1Type llvmctx
   let ginit?slot ← LLVM.getOrAddGlobal mod (modName.mangle ++ "_G_initialized") ginit?ty
+  LLVM.setVisibility ginit?slot LLVM.Visibility.hidden -- static
   LLVM.setInitializer ginit?slot (← LLVM.constFalse llvmctx)
   let ginit?v ← LLVM.buildLoad2 builder ginit?ty ginit?slot "init_v"
   buildIfThen_ builder "isGInitialized" ginit?v

src/Lean/Compiler/IR/LLVMBindings.lean

@@ -294,6 +294,28 @@ opaque disposeTargetMachine (tm : TargetMachine ctx) : BaseIO Unit
 opaque disposeModule (m : Module ctx) : BaseIO Unit
 
 
+-- https://github.com/llvm/llvm-project/blob/c3e073bcbdc523b0f758d44a89a6333e38bff863/llvm/include/llvm-c/Core.h#L198
+structure Visibility where
+  private mk :: val : UInt64
+
+def Visibility.default   : Visibility := { val := 0 }
+def Visibility.hidden    : Visibility := { val := 1 }
+def Visibility.protected : Visibility := { val := 2 }
+
+@[extern "lean_llvm_set_visibility"]
+opaque setVisibility {ctx : Context} (value : Value ctx) (visibility : Visibility) : BaseIO Unit
+
+-- https://github.com/llvm/llvm-project/blob/c3e073bcbdc523b0f758d44a89a6333e38bff863/llvm/include/llvm-c/Core.h#L210
+structure DLLStorageClass where
+  private mk :: val : UInt64
+
+def DLLStorageClass.default : DLLStorageClass := { val := 0 }
+def DLLStorageClass.import  : DLLStorageClass := { val := 1 }
+def DLLStorageClass.export  : DLLStorageClass := { val := 2 }
+
+@[extern "lean_llvm_set_dll_storage_class"]
+opaque setDLLStorageClass {ctx : Context} (value : Value ctx) (dllStorageClass : DLLStorageClass) : BaseIO Unit
+
 -- Helper to add a function if it does not exist, and to return the function handle if it does.
 def getOrAddFunction(m : Module ctx) (name : String) (type : LLVMType ctx) : BaseIO (Value ctx) :=  do
   match (← getNamedFunction m name) with

src/Lean/Compiler/Specialize.lean

@@ -79,7 +79,7 @@ inductive SpecArgKind where
 
 structure SpecInfo where
   mutualDecls : List Name
-  argKinds : SpecArgKind
+  argKinds : List SpecArgKind
   deriving Inhabited
 
 structure SpecState where

src/Lean/Data/HashMap.lean

@@ -38,7 +38,7 @@ private def mkIdx {sz : Nat} (hash : UInt64) (h : sz.isPowerOfTwo) : { u : USize
   if h' : u.toNat < sz then
     ⟨u, h'⟩
   else
-    ⟨0, by simp [USize.toNat, OfNat.ofNat, USize.ofNat, Fin.ofNat']; rw [Nat.zero_mod]; apply Nat.pos_of_isPowerOfTwo h⟩
+    ⟨0, by simp [USize.toNat, OfNat.ofNat, USize.ofNat, Fin.ofNat']; apply Nat.pos_of_isPowerOfTwo h⟩
 
 @[inline] def reinsertAux (hashFn : α → UInt64) (data : HashMapBucket α β) (a : α) (b : β) : HashMapBucket α β :=
   let ⟨i, h⟩ := mkIdx (hashFn a) data.property

src/Lean/Data/HashSet.lean

@@ -34,7 +34,7 @@ private def mkIdx {sz : Nat} (hash : UInt64) (h : sz.isPowerOfTwo) : { u : USize
   if h' : u.toNat < sz then
     ⟨u, h'⟩
   else
-    ⟨0, by simp [USize.toNat, OfNat.ofNat, USize.ofNat, Fin.ofNat']; rw [Nat.zero_mod]; apply Nat.pos_of_isPowerOfTwo h⟩
+    ⟨0, by simp [USize.toNat, OfNat.ofNat, USize.ofNat, Fin.ofNat']; apply Nat.pos_of_isPowerOfTwo h⟩
 
 @[inline] def reinsertAux (hashFn : α → UInt64) (data : HashSetBucket α) (a : α) : HashSetBucket α :=
   let ⟨i, h⟩ := mkIdx (hashFn a) data.property

src/Lean/Elab/AutoBound.lean

@@ -11,7 +11,7 @@ namespace Lean.Elab
 
 register_builtin_option autoImplicit : Bool := {
     defValue := true
-    descr    := "Unbound local variables in declaration headers become implicit arguments. In \"relaxed\" mode (default), any atomic identifier is eligible, otherwise only a lower case or greek letter followed by numeric digits are eligible. For example, `def f (x : Vector α n) : Vector α n :=` automatically introduces the implicit variables {α n}."
+    descr    := "Unbound local variables in declaration headers become implicit arguments. In \"relaxed\" mode (default), any atomic identifier is eligible, otherwise only single character followed by numeric digits are eligible. For example, `def f (x : Vector α n) : Vector α n :=` automatically introduces the implicit variables {α n}."
   }
 
 register_builtin_option relaxedAutoImplicit : Bool := {
@@ -39,7 +39,7 @@ Therefore, we do consider identifier with macro scopes anymore.
 
 def isValidAutoBoundImplicitName (n : Name) (relaxed : Bool) : Bool :=
   match n with
-  | .str .anonymous s => s.length > 0 && (relaxed || ((isGreek s.front || s.front.isLower) && isValidAutoBoundSuffix s))
+  | .str .anonymous s => s.length > 0 && (relaxed || isValidAutoBoundSuffix s)
   | _ => false
 
 def isValidAutoBoundLevelName (n : Name) (relaxed : Bool) : Bool :=

src/Lean/Elab/Binders.lean

@@ -182,7 +182,10 @@ register_builtin_option checkBinderAnnotations : Bool := {
 /-- Throw an error if `type` is not a valid local instance. -/
 private partial def checkLocalInstanceParameters (type : Expr) : TermElabM Unit := do
   let .forallE n d b bi ← whnf type | return ()
-  if !b.hasLooseBVar 0 then
+  -- We allow instance arguments so that local instances of the form
+  -- `variable [∀ (a : α) [P a], Q a]`
+  -- are accepted, per https://github.com/leanprover/lean4/issues/2311
+  if bi != .instImplicit && !b.hasLooseBVar 0 then
     throwError "invalid parametric local instance, parameter with type{indentExpr d}\ndoes not have forward dependencies, type class resolution cannot use this kind of local instance because it will not be able to infer a value for this parameter."
   withLocalDecl n bi d fun x => checkLocalInstanceParameters (b.instantiate1 x)
 

src/Lean/Elab/BuiltinCommand.lean

@@ -52,14 +52,19 @@ private def popScopes (numScopes : Nat) : CommandElabM Unit :=
   for _ in [0:numScopes] do
     popScope
 
-private def checkAnonymousScope : List Scope → Bool
-  | { header := "", .. } :: _   => true
-  | _                           => false
+private def checkAnonymousScope : List Scope → Option Name
+  | { header := "", .. } :: _ => none
+  | { header := h, .. }  :: _ => some h
+  | _                         => some .anonymous -- should not happen
 
-private def checkEndHeader : Name → List Scope → Bool
-  | .anonymous, _                             => true
-  | .str p s,   { header := h, .. } :: scopes => h == s && checkEndHeader p scopes
-  | _,          _                             => false
+private def checkEndHeader : Name → List Scope → Option Name
+  | .anonymous, _ => none
+  | .str p s, { header := h, .. } :: scopes =>
+    if h == s then
+      (.str · s) <$> checkEndHeader p scopes
+    else
+      some h
+  | _, _ => some .anonymous -- should not happen
 
 @[builtin_command_elab «namespace»] def elabNamespace : CommandElab := fun stx =>
   match stx with
@@ -94,12 +99,12 @@ private def checkEndHeader : Name → List Scope → Bool
     throwError "invalid 'end', insufficient scopes"
   match header? with
   | none        =>
-    unless checkAnonymousScope scopes do
-      throwError "invalid 'end', name is missing"
+    if let some name := checkAnonymousScope scopes then
+      throwError "invalid 'end', name is missing (expected {name})"
   | some header =>
-    unless checkEndHeader header scopes do
+    if let some name := checkEndHeader header scopes then
       addCompletionInfo <| CompletionInfo.endSection stx (scopes.map fun scope => scope.header)
-      throwError "invalid 'end', name mismatch"
+      throwError "invalid 'end', name mismatch (expected {if name == `«» then `nothing else name})"
 
 private partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM Unit :=
   if h : i < cmds.size then

src/Lean/Elab/Command.lean

@@ -304,7 +304,7 @@ builtin_initialize registerTraceClass `Elab.input
 `elabCommand` wrapper that should be used for the initial invocation, not for recursive calls after
 macro expansion etc.
 -/
-def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do
+def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do profileitM Exception "elaboration" (← getOptions) do
   let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
   let initInfoTrees ← getResetInfoTrees
   -- We should *not* factor out `elabCommand`'s `withLogging` to here since it would make its error

src/Lean/Elab/Extra.lean

@@ -209,11 +209,11 @@ private structure AnalyzeResult where
   max?            : Option Expr := none
   hasUncomparable : Bool := false -- `true` if there are two types `α` and `β` where we don't have coercions in any direction.
 
-private def isUnknow : Expr → Bool
+private def isUnknown : Expr → Bool
   | .mvar ..        => true
-  | .app f _        => isUnknow f
-  | .letE _ _ _ b _ => isUnknow b
-  | .mdata _ b      => isUnknow b
+  | .app f _        => isUnknown f
+  | .letE _ _ _ b _ => isUnknown b
+  | .mdata _ b      => isUnknown b
   | _               => false
 
 private def analyze (t : Tree) (expectedType? : Option Expr) : TermElabM AnalyzeResult := do
@@ -222,7 +222,7 @@ private def analyze (t : Tree) (expectedType? : Option Expr) : TermElabM Analyze
     | none => pure none
     | some expectedType =>
       let expectedType ← instantiateMVars expectedType
-      if isUnknow expectedType then pure none else pure (some expectedType)
+      if isUnknown expectedType then pure none else pure (some expectedType)
   (go t *> get).run' { max? }
 where
    go (t : Tree) : StateRefT AnalyzeResult TermElabM Unit := do
@@ -233,7 +233,7 @@ where
        | .unop _ _ arg => go arg
        | .term _ _ val =>
          let type ← instantiateMVars (← inferType val)
-         unless isUnknow type do
+         unless isUnknown type do
            match (← get).max? with
            | none     => modify fun s => { s with max? := type }
            | some max =>
@@ -246,7 +246,10 @@ where
                  trace[Elab.binop] "uncomparable types: {max}, {type}"
                  modify fun s => { s with hasUncomparable := true }
 
-private def mkBinOp (f : Expr) (lhs rhs : Expr) : TermElabM Expr := do
+private def mkBinOp (lazy : Bool) (f : Expr) (lhs rhs : Expr) : TermElabM Expr := do
+  let mut rhs := rhs
+  if lazy then
+    rhs ← mkFunUnit rhs
   elabAppArgs f #[] #[Arg.expr lhs, Arg.expr rhs] (expectedType? := none) (explicit := false) (ellipsis := false) (resultIsOutParamSupport := false)
 
 private def mkUnOp (f : Expr) (arg : Expr) : TermElabM Expr := do
@@ -258,11 +261,7 @@ private def toExprCore (t : Tree) : TermElabM Expr := do
     modifyInfoState (fun s => { s with trees := s.trees ++ trees }); return e
   | .binop ref lazy f lhs rhs =>
     withRef ref <| withInfoContext' ref (mkInfo := mkTermInfo .anonymous ref) do
-      let lhs ← toExprCore lhs
-      let mut rhs ← toExprCore rhs
-      if lazy then
-        rhs ← mkFunUnit rhs
-      mkBinOp f lhs rhs
+      mkBinOp lazy f (← toExprCore lhs) (← toExprCore rhs)
   | .unop ref f arg =>
     withRef ref <| withInfoContext' ref (mkInfo := mkTermInfo .anonymous ref) do
       mkUnOp f (← toExprCore arg)
@@ -359,7 +358,7 @@ mutual
           return .binop ref lazy f (← go lhs f true false) (← go rhs f false false)
         else
           let r ← withRef ref do
-            mkBinOp f (← toExpr lhs none) (← toExpr rhs none)
+            mkBinOp lazy f (← toExpr lhs none) (← toExpr rhs none)
           let infoTrees ← getResetInfoTrees
           return .term ref infoTrees r
       | .unop ref f arg =>
@@ -367,7 +366,7 @@ mutual
       | .term ref trees e =>
         let type ← instantiateMVars (← inferType e)
         trace[Elab.binop] "visiting {e} : {type} =?= {maxType}"
-        if isUnknow type then
+        if isUnknown type then
           if let some f := f? then
             if (← hasHeterogeneousDefaultInstances f maxType lhs) then
               -- See comment at `hasHeterogeneousDefaultInstances`

src/Lean/Elab/Frontend.lean

@@ -62,7 +62,7 @@ def processCommand : FrontendM Bool := do
     modify fun s => { s with commands := s.commands.push cmd }
     setParserState ps
     setMessages messages
-    profileitM IO.Error "elaboration" scope.opts <| elabCommandAtFrontend cmd
+    elabCommandAtFrontend cmd
     pure (Parser.isTerminalCommand cmd)
 
 partial def processCommands : FrontendM Unit := do

src/Lean/Elab/PreDefinition/Basic.lean

@@ -120,8 +120,7 @@ private def addNonRecAux (preDef : PreDefinition) (compile : Bool) (all : List N
     if preDef.modifiers.isNoncomputable then
       modifyEnv fun env => addNoncomputable env preDef.declName
     if compile && shouldGenCodeFor preDef then
-      unless (← compileDecl decl) do
-        return ()
+      discard <| compileDecl decl
     if applyAttrAfterCompilation then
       applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
 
@@ -157,8 +156,7 @@ def addAndCompileUnsafe (preDefs : Array PreDefinition) (safety := DefinitionSaf
       for preDef in preDefs do
         addTermInfo' preDef.ref (← mkConstWithLevelParams preDef.declName) (isBinder := true)
     applyAttributesOf preDefs AttributeApplicationTime.afterTypeChecking
-    unless (← compileDecl decl) do
-      return ()
+    discard <| compileDecl decl
     applyAttributesOf preDefs AttributeApplicationTime.afterCompilation
     return ()
 

src/Lean/Elab/PreDefinition/Main.lean

@@ -73,7 +73,7 @@ private def ensureNoUnassignedMVarsAtPreDef (preDef : PreDefinition) : TermElabM
   This method beta-reduces them to make sure they can be eliminated by the well-founded recursion module. -/
 private def betaReduceLetRecApps (preDefs : Array PreDefinition) : MetaM (Array PreDefinition) :=
   preDefs.mapM fun preDef => do
-    let value ← transform preDef.value fun e => do
+    let value ← Core.transform preDef.value fun e => do
       if e.isApp && e.getAppFn.isLambda && e.getAppArgs.all fun arg => arg.getAppFn.isConst && preDefs.any fun preDef => preDef.declName == arg.getAppFn.constName! then
         return .visit e.headBeta
       else
@@ -106,7 +106,12 @@ def addPreDefinitions (preDefs : Array PreDefinition) (hints : TerminationHints)
   for preDefs in cliques do
     trace[Elab.definition.scc] "{preDefs.map (·.declName)}"
     if preDefs.size == 1 && isNonRecursive preDefs[0]! then
-      let preDef := preDefs[0]!
+      /-
+      We must erase `recApp` annotations even when `preDef` is not recursive
+      because it may use another recursive declaration in the same mutual block.
+      See issue #2321
+      -/
+      let preDef ← eraseRecAppSyntax preDefs[0]!
       if preDef.modifiers.isNoncomputable then
         addNonRec preDef
       else

src/Lean/Elab/PreDefinition/Structural/Main.lean

@@ -85,7 +85,14 @@ def structuralRecursion (preDefs : Array PreDefinition) : TermElabM Unit :=
     let preDefNonRec ← eraseRecAppSyntax preDefNonRec
     let preDef ← eraseRecAppSyntax preDefs[0]!
     state.addMatchers.forM liftM
-    registerEqnsInfo preDef recArgPos
+    unless preDef.kind.isTheorem do
+      unless (← isProp preDef.type) do
+        /-
+        Don't save predefinition info for equation generator
+        for theorems and definitions that are propositions.
+        See issue #2327
+        -/
+        registerEqnsInfo preDef recArgPos
     mapError (addNonRec preDefNonRec (applyAttrAfterCompilation := false)) fun msg =>
       m!"structural recursion failed, produced type incorrect term{indentD msg}"
     addAndCompilePartialRec #[preDef]

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -208,11 +208,18 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
 
 builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension
 
-def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedPrefixSize : Nat) : CoreM Unit := do
-  let declNames := preDefs.map (·.declName)
-  modifyEnv fun env =>
-    preDefs.foldl (init := env) fun env preDef =>
-      eqnInfoExt.insert env preDef.declName { preDef with declNames, declNameNonRec, fixedPrefixSize }
+def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedPrefixSize : Nat) : MetaM Unit := do
+  /-
+  See issue #2327.
+  Remark: we could do better for mutual declarations that mix theorems and definitions. However, this is a rare
+  combination, and we would have add support for it in the equation generator. I did not check which assumptions are made there.
+  -/
+  unless preDefs.all fun p => p.kind.isTheorem do
+    unless (← preDefs.allM fun p => isProp p.type) do
+      let declNames := preDefs.map (·.declName)
+      modifyEnv fun env =>
+        preDefs.foldl (init := env) fun env preDef =>
+          eqnInfoExt.insert env preDef.declName { preDef with declNames, declNameNonRec, fixedPrefixSize }
 
 def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
   if let some info := eqnInfoExt.find? (← getEnv) declName then

src/Lean/Elab/Tactic/Generalize.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 import Lean.Meta.Tactic.Generalize
 import Lean.Meta.Check
 import Lean.Meta.Tactic.Intro
+import Lean.Elab.Binders
 import Lean.Elab.Tactic.ElabTerm
 import Lean.Elab.Tactic.Location
 
@@ -14,15 +15,27 @@ open Meta
 
 @[builtin_tactic Lean.Parser.Tactic.generalize] def evalGeneralize : Tactic := fun stx =>
   withMainContext do
-    let args ← stx[1].getSepArgs.mapM fun arg => do
-      let hName? := if arg[0].isNone then none else some arg[0][0].getId
+    let mut xIdents := #[]
+    let mut hIdents := #[]
+    let mut args := #[]
+    for arg in stx[1].getSepArgs do
+      let hName? ← if arg[0].isNone then
+        pure none
+      else
+        hIdents := hIdents.push arg[0][0]
+        pure (some arg[0][0].getId)
       let expr ← elabTerm arg[1] none
-      return { hName?, expr, xName? := arg[3].getId : GeneralizeArg }
+      xIdents := xIdents.push arg[3]
+      args := args.push { hName?, expr, xName? := arg[3].getId : GeneralizeArg }
     let hyps ← match expandOptLocation stx[2] with
     | .targets hyps _ => getFVarIds hyps
     | .wildcard => pure (← getLCtx).getFVarIds
-    liftMetaTactic fun mvarId => do
-      let (_, _, mvarId) ← mvarId.generalizeHyp args hyps
-      return [mvarId]
+    let mvarId ← getMainGoal
+    mvarId.withContext do
+      let (_, newVars, mvarId) ← mvarId.generalizeHyp args hyps
+      mvarId.withContext do
+        for v in newVars, id in xIdents ++ hIdents do
+          Term.addLocalVarInfo id (.fvar v)
+        replaceMainGoal [mvarId]
 
 end Lean.Elab.Tactic

src/Lean/Elab/Tactic/Rewrite.lean

@@ -11,20 +11,16 @@ import Lean.Elab.Tactic.Config
 namespace Lean.Elab.Tactic
 open Meta
 
-def rewriteTarget (stx : Syntax) (symm : Bool) (config : Rewrite.Config) : TacticM Unit := do
-  Term.withSynthesize <| withMainContext do
-    let e ← elabTerm stx none true
-    let r ← (← getMainGoal).rewrite (← getMainTarget) e symm (config := config)
-    let mvarId' ← (← getMainGoal).replaceTargetEq r.eNew r.eqProof
-    replaceMainGoal (mvarId' :: r.mvarIds)
+def rewriteTarget (e : Expr) (symm : Bool) (config : Rewrite.Config) : TacticM Unit := do
+  let r ← (← getMainGoal).rewrite (← getMainTarget) e symm (config := config)
+  let mvarId' ← (← getMainGoal).replaceTargetEq r.eNew r.eqProof
+  replaceMainGoal (mvarId' :: r.mvarIds)
 
-def rewriteLocalDecl (stx : Syntax) (symm : Bool) (fvarId : FVarId) (config : Rewrite.Config) : TacticM Unit := do
-  Term.withSynthesize <| withMainContext do
-    let e ← elabTerm stx none true
-    let localDecl ← fvarId.getDecl
-    let rwResult ← (← getMainGoal).rewrite localDecl.type e symm (config := config)
-    let replaceResult ← (← getMainGoal).replaceLocalDecl fvarId rwResult.eNew rwResult.eqProof
-    replaceMainGoal (replaceResult.mvarId :: rwResult.mvarIds)
+def rewriteLocalDecl (e : Expr) (symm : Bool) (fvarId : FVarId) (config : Rewrite.Config) : TacticM Unit := do
+  let localDecl ← fvarId.getDecl
+  let rwResult ← (← getMainGoal).rewrite localDecl.type e symm (config := config)
+  let replaceResult ← (← getMainGoal).replaceLocalDecl fvarId rwResult.eNew rwResult.eqProof
+  replaceMainGoal (replaceResult.mvarId :: rwResult.mvarIds)
 
 def withRWRulesSeq (token : Syntax) (rwRulesSeqStx : Syntax) (x : (symm : Bool) → (term : Syntax) → TacticM Unit) : TacticM Unit := do
   let lbrak := rwRulesSeqStx[0]
@@ -62,9 +58,11 @@ declare_config_elab elabRewriteConfig Rewrite.Config
   let cfg ← elabRewriteConfig stx[1]
   let loc   := expandOptLocation stx[3]
   withRWRulesSeq stx[0] stx[2] fun symm term => do
-    withLocation loc
-      (rewriteLocalDecl term symm · cfg)
-      (rewriteTarget term symm cfg)
-      (throwTacticEx `rewrite · "did not find instance of the pattern in the current goal")
+    Term.withSynthesize <| withMainContext do
+      let e ← elabTerm term none true
+      withLocation loc
+        (rewriteLocalDecl e symm · cfg)
+        (rewriteTarget e symm cfg)
+        (throwTacticEx `rewrite · "did not find instance of the pattern in the current goal")
 
 end Lean.Elab.Tactic

src/Lean/Meta/AbstractNestedProofs.lean

@@ -8,11 +8,18 @@ import Lean.Meta.Closure
 namespace Lean.Meta
 namespace AbstractNestedProofs
 
+def getLambdaBody (e : Expr) : Expr :=
+  match e with
+  | .lam _ _ b _ => getLambdaBody b
+  | _ => e
+
 def isNonTrivialProof (e : Expr) : MetaM Bool := do
   if !(← isProof e) then
     pure false
   else
-    e.withApp fun f args =>
+    -- We consider proofs such as `fun x => f x a` as trivial.
+    -- For example, we don't want to abstract the body of `def rfl`
+    (getLambdaBody e).withApp fun f args =>
       pure $ !f.isAtomic || args.any fun arg => !arg.isAtomic
 
 structure Context where
@@ -31,7 +38,7 @@ private def mkAuxLemma (e : Expr) : M Expr := do
   /- We turn on zeta-expansion to make sure we don't need to perform an expensive `check` step to
      identify which let-decls can be abstracted. If we design a more efficient test, we can avoid the eager zeta expasion step.
      It a benchmark created by @selsam, The extra `check` step was a bottleneck. -/
-  mkAuxDefinitionFor lemmaName e (zeta := true)
+  mkAuxTheoremFor lemmaName e (zeta := true)
 
 partial def visit (e : Expr) : M Expr := do
   if e.isAtomic then

src/Lean/Meta/Closure.lean

@@ -366,4 +366,39 @@ def mkAuxDefinitionFor (name : Name) (value : Expr) (zeta : Bool := false) : Met
   let type := type.headBeta
   mkAuxDefinition name type value (zeta := zeta)
 
+/--
+  Create an auxiliary theorem with the given name, type and value. It is similar to `mkAuxDefinition`.
+-/
+def mkAuxTheorem (name : Name) (type : Expr) (value : Expr) (zeta : Bool := false) : MetaM Expr := do
+  let result ← Closure.mkValueTypeClosure type value zeta
+  let env ← getEnv
+  let decl :=
+    if env.hasUnsafe result.type || env.hasUnsafe result.value then
+      -- `result` contains unsafe code, thus we cannot use a theorem.
+      Declaration.defnDecl {
+        name
+        levelParams := result.levelParams.toList
+        type        := result.type
+        value       := result.value
+        hints       := ReducibilityHints.opaque
+        safety      := DefinitionSafety.unsafe
+      }
+    else
+      Declaration.thmDecl {
+        name
+        levelParams := result.levelParams.toList
+        type        := result.type
+        value       := result.value
+      }
+  addDecl decl
+  return mkAppN (mkConst name result.levelArgs.toList) result.exprArgs
+
+/--
+  Similar to `mkAuxTheorem`, but infers the type of `value`.
+-/
+def mkAuxTheoremFor (name : Name) (value : Expr) (zeta : Bool := false) : MetaM Expr := do
+  let type ← inferType value
+  let type := type.headBeta
+  mkAuxTheorem name type value zeta
+
 end Lean.Meta

src/Lean/Meta/DiscrTree.lean

@@ -182,6 +182,31 @@ private partial def isNumeral (e : Expr) : Bool :=
       else if fName == ``Nat.zero && e.getAppNumArgs == 0 then true
       else false
 
+private partial def toNatLit? (e : Expr) : Option Literal :=
+  if isNumeral e then
+    if let some n := loop e then
+      some (.natVal n)
+    else
+      none
+  else
+    none
+where
+  loop (e : Expr) : OptionT Id Nat := do
+    let f := e.getAppFn
+    match f with
+    | .lit (.natVal n) => return n
+    | .const fName .. =>
+      if fName == ``Nat.succ && e.getAppNumArgs == 1 then
+        let r ← loop e.appArg!
+        return r+1
+      else if fName == ``OfNat.ofNat && e.getAppNumArgs == 3 then
+        loop (e.getArg! 1)
+      else if fName == ``Nat.zero && e.getAppNumArgs == 0 then
+        return 0
+      else
+        failure
+    | _ => failure
+
 private def isNatType (e : Expr) : MetaM Bool :=
   return (← whnf e).isConstOf ``Nat
 
@@ -207,16 +232,14 @@ private def isOffset (fName : Name) (e : Expr) : MetaM Bool := do
   TODO: add hook for users adding their own functions for controlling `shouldAddAsStar`
   Different `DiscrTree` users may populate this set using, for example, attributes.
 
-  Remark: we currently tag `Nat.zero` and "offset" terms to avoid having to add special
-  support for `Expr.lit` and offset terms.
+  Remark: we currently tag "offset" terms as star to avoid having to add special
+  support for offset terms.
   Example, suppose the discrimination tree contains the entry
   `Nat.succ ?m |-> v`, and we are trying to retrieve the matches for `Expr.lit (Literal.natVal 1) _`.
-  In this scenario, we want to retrieve `Nat.succ ?m |-> v` -/
+  In this scenario, we want to retrieve `Nat.succ ?m |-> v`
+-/
 private def shouldAddAsStar (fName : Name) (e : Expr) : MetaM Bool := do
-  if fName == ``Nat.zero then
-    return true
-  else
-    isOffset fName e
+  isOffset fName e
 
 def mkNoindexAnnotation (e : Expr) : Expr :=
   mkAnnotation `noindex e
@@ -313,9 +336,12 @@ private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) : MetaM (Key s
       let todo ← pushArgsAux info.paramInfo (nargs-1) e todo
       return (k, todo)
     match fn with
-    | .lit v         => return (.lit v, todo)
-    | .const c _     =>
+    | .lit v     =>
+      return (.lit v, todo)
+    | .const c _ =>
       unless root do
+        if let some v := toNatLit? e then
+          return (.lit v, todo)
         if (← shouldAddAsStar c e) then
           return (.star, todo)
       let nargs := e.getAppNumArgs
@@ -376,8 +402,24 @@ private partial def createNodes (keys : Array (Key s)) (v : α) (i : Nat) : Trie
   else
     .node #[v] #[]
 
+/--
+If `vs` contains an element `v'` such that `v == v'`, then replace `v'` with `v`.
+Otherwise, push `v`.
+See issue #2155
+Recall that `BEq α` may not be Lawful.
+-/
 private def insertVal [BEq α] (vs : Array α) (v : α) : Array α :=
-  if vs.contains v then vs else vs.push v
+  loop 0
+where
+  loop (i : Nat) : Array α :=
+    if h : i < vs.size then
+      if v == vs[i] then
+        vs.set ⟨i,h⟩ v
+      else
+        loop (i+1)
+    else
+      vs.push v
+termination_by loop i => vs.size - i
 
 private partial def insertAux [BEq α] (keys : Array (Key s)) (v : α) : Nat → Trie α s → Trie α s
   | i, .node vs cs =>
@@ -410,6 +452,10 @@ def insert [BEq α] (d : DiscrTree α s) (e : Expr) (v : α) : MetaM (DiscrTree
 
 private def getKeyArgs (e : Expr) (isMatch root : Bool) : MetaM (Key s × Array Expr) := do
   let e ← reduceDT e root (simpleReduce := s)
+  unless root do
+    -- See pushArgs
+    if let some v := toNatLit? e then
+      return (.lit v, #[])
   match e.getAppFn with
   | .lit v         => return (.lit v, #[])
   | .const c _     =>

src/Lean/Meta/Injective.lean

@@ -158,9 +158,13 @@ def mkInjectiveTheorems (declName : Name) : MetaM Unit := do
       -- See https://github.com/leanprover/lean4/issues/2188
       withLCtx {} {} do
       for ctor in info.ctors do
-        let ctorVal ← getConstInfoCtor ctor
-        if ctorVal.numFields > 0 then
-          mkInjectiveTheorem ctorVal
-          mkInjectiveEqTheorem ctorVal
+        withTraceNode `Meta.injective (fun _ => return m!"{ctor}") do
+          let ctorVal ← getConstInfoCtor ctor
+          if ctorVal.numFields > 0 then
+            mkInjectiveTheorem ctorVal
+            mkInjectiveEqTheorem ctorVal
+
+builtin_initialize
+  registerTraceClass `Meta.injective
 
 end Lean.Meta

src/Lean/Meta/Instances.lean

@@ -73,7 +73,7 @@ structure Instances where
 
 def addInstanceEntry (d : Instances) (e : InstanceEntry) : Instances :=
   match e.globalName? with
-  | some n => { d with discrTree := d.discrTree.insertCore e.keys e, instanceNames := d.instanceNames.insert n e }
+  | some n => { d with discrTree := d.discrTree.insertCore e.keys e, instanceNames := d.instanceNames.insert n e, erased := d.erased.erase n }
   | none   => { d with discrTree := d.discrTree.insertCore e.keys e }
 
 def Instances.eraseCore (d : Instances) (declName : Name) : Instances :=

src/Lean/Meta/SizeOf.lean

@@ -471,42 +471,43 @@ register_builtin_option genSizeOf : Bool := {
 
 register_builtin_option genSizeOfSpec : Bool := {
   defValue := true
-  descr    := "generate `SizeOf` specificiation theorems for automatically generated instances"
+  descr    := "generate `SizeOf` specification theorems for automatically generated instances"
 }
 
 def mkSizeOfInstances (typeName : Name) : MetaM Unit := do
   if (← getEnv).contains ``SizeOf && genSizeOf.get (← getOptions) && !(← isInductivePredicate typeName) then
-    let indInfo ← getConstInfoInduct typeName
-    unless indInfo.isUnsafe do
-      let (fns, recMap) ← mkSizeOfFns typeName
-      for indTypeName in indInfo.all, fn in fns do
-        let indInfo ← getConstInfoInduct indTypeName
-        forallTelescopeReducing indInfo.type fun xs _ =>
-          let params := xs[:indInfo.numParams]
-          withInstImplicitAsImplict params do
-            let indices := xs[indInfo.numParams:]
-            mkLocalInstances params fun localInsts => do
-              let us := indInfo.levelParams.map mkLevelParam
-              let indType := mkAppN (mkConst indTypeName us) xs
-              let sizeOfIndType ← mkAppM ``SizeOf #[indType]
-              withLocalDeclD `m indType fun m => do
-                let v ← mkLambdaFVars #[m] <| mkAppN (mkConst fn us) (params ++ localInsts ++ indices ++ #[m])
-                let sizeOfMk ← mkAppM ``SizeOf.mk #[v]
-                let instDeclName := indTypeName ++ `_sizeOf_inst
-                let instDeclType ← mkForallFVars (xs ++ localInsts) sizeOfIndType
-                let instDeclValue ← mkLambdaFVars (xs ++ localInsts) sizeOfMk
-                trace[Meta.sizeOf] ">> {instDeclName} : {instDeclType}"
-                addDecl <| Declaration.defnDecl {
-                  name        := instDeclName
-                  levelParams := indInfo.levelParams
-                  type        := instDeclType
-                  value       := instDeclValue
-                  safety      := .safe
-                  hints       := .abbrev
-                }
-                addInstance instDeclName AttributeKind.global (eval_prio default)
-      if genSizeOfSpec.get (← getOptions) then
-        mkSizeOfSpecTheorems indInfo.all.toArray fns recMap
+    withTraceNode `Meta.sizeOf (fun _ => return m!"{typeName}") do
+      let indInfo ← getConstInfoInduct typeName
+      unless indInfo.isUnsafe do
+        let (fns, recMap) ← mkSizeOfFns typeName
+        for indTypeName in indInfo.all, fn in fns do
+          let indInfo ← getConstInfoInduct indTypeName
+          forallTelescopeReducing indInfo.type fun xs _ =>
+            let params := xs[:indInfo.numParams]
+            withInstImplicitAsImplict params do
+              let indices := xs[indInfo.numParams:]
+              mkLocalInstances params fun localInsts => do
+                let us := indInfo.levelParams.map mkLevelParam
+                let indType := mkAppN (mkConst indTypeName us) xs
+                let sizeOfIndType ← mkAppM ``SizeOf #[indType]
+                withLocalDeclD `m indType fun m => do
+                  let v ← mkLambdaFVars #[m] <| mkAppN (mkConst fn us) (params ++ localInsts ++ indices ++ #[m])
+                  let sizeOfMk ← mkAppM ``SizeOf.mk #[v]
+                  let instDeclName := indTypeName ++ `_sizeOf_inst
+                  let instDeclType ← mkForallFVars (xs ++ localInsts) sizeOfIndType
+                  let instDeclValue ← mkLambdaFVars (xs ++ localInsts) sizeOfMk
+                  trace[Meta.sizeOf] ">> {instDeclName} : {instDeclType}"
+                  addDecl <| Declaration.defnDecl {
+                    name        := instDeclName
+                    levelParams := indInfo.levelParams
+                    type        := instDeclType
+                    value       := instDeclValue
+                    safety      := .safe
+                    hints       := .abbrev
+                  }
+                  addInstance instDeclName AttributeKind.global (eval_prio default)
+        if genSizeOfSpec.get (← getOptions) then
+          mkSizeOfSpecTheorems indInfo.all.toArray fns recMap
 
 builtin_initialize
   registerTraceClass `Meta.sizeOf

src/Lean/Meta/Tactic/Apply.lean

@@ -27,6 +27,11 @@ structure ApplyConfig where
   -/
   synthAssignedInstances := true
   /--
+  If `allowSynthFailures` is `true`, then `apply` will return instance implicit arguments
+  for which typeclass search failed as new goals.
+  -/
+  allowSynthFailures := false
+  /--
   If `approx := true`, then we turn on `isDefEq` approximations. That is, we use
   the `approxDefEq` combinator.
   -/
@@ -47,15 +52,18 @@ def getExpectedNumArgs (e : Expr) : MetaM Nat := do
 private def throwApplyError {α} (mvarId : MVarId) (eType : Expr) (targetType : Expr) : MetaM α :=
   throwTacticEx `apply mvarId m!"failed to unify{indentExpr eType}\nwith{indentExpr targetType}"
 
-def synthAppInstances (tacticName : Name) (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Array BinderInfo) (synthAssignedInstances : Bool) : MetaM Unit :=
+def synthAppInstances (tacticName : Name) (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Array BinderInfo)
+    (synthAssignedInstances : Bool) (allowSynthFailures : Bool) : MetaM Unit :=
   newMVars.size.forM fun i => do
     if binderInfos[i]!.isInstImplicit then
       let mvar := newMVars[i]!
       if synthAssignedInstances || !(← mvar.mvarId!.isAssigned) then
         let mvarType ← inferType mvar
-        let mvarVal  ← synthInstance mvarType
-        unless (← isDefEq mvar mvarVal) do
-          throwTacticEx tacticName mvarId "failed to assign synthesized instance"
+        try
+          let mvarVal  ← synthInstance mvarType
+          unless (← isDefEq mvar mvarVal) do
+            throwTacticEx tacticName mvarId "failed to assign synthesized instance"
+        catch e => unless allowSynthFailures do throw e
 
 def appendParentTag (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Array BinderInfo) : MetaM Unit := do
   let parentTag ← mvarId.getTag
@@ -76,8 +84,9 @@ If `synthAssignedInstances` is `true`, then `apply` will synthesize instance imp
 even if they have assigned by `isDefEq`, and then check whether the synthesized value matches the
 one inferred. The `congr` tactic sets this flag to false.
 -/
-def postprocessAppMVars (tacticName : Name) (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Array BinderInfo) (synthAssignedInstances := true) : MetaM Unit := do
-  synthAppInstances tacticName mvarId newMVars binderInfos synthAssignedInstances
+def postprocessAppMVars (tacticName : Name) (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Array BinderInfo)
+    (synthAssignedInstances := true) (allowSynthFailures := false) : MetaM Unit := do
+  synthAppInstances tacticName mvarId newMVars binderInfos synthAssignedInstances allowSynthFailures
   -- TODO: default and auto params
   appendParentTag mvarId newMVars binderInfos
 
@@ -163,7 +172,7 @@ def _root_.Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig :=
         let (_, _, eType) ← forallMetaTelescopeReducing eType (some rangeNumArgs.start)
         throwApplyError mvarId eType targetType
     let (newMVars, binderInfos) ← go rangeNumArgs.start
-    postprocessAppMVars `apply mvarId newMVars binderInfos cfg.synthAssignedInstances
+    postprocessAppMVars `apply mvarId newMVars binderInfos cfg.synthAssignedInstances cfg.allowSynthFailures
     let e ← instantiateMVars e
     mvarId.assign (mkAppN e newMVars)
     let newMVars ← newMVars.filterM fun mvar => not <$> mvar.mvarId!.isAssigned

src/Lean/Meta/WHNF.lean

@@ -155,12 +155,24 @@ private def toCtorWhenStructure (inductName : Name) (major : Expr) : MetaM Expr
         return result
     | _ => return major
 
+
+-- Helper predicate that returns `true` for inductive predicates used to define functions by well-founded recursion.
+private def isWFRec (declName : Name) : Bool :=
+  declName == ``Acc.rec || declName == ``WellFounded.rec
+
 /-- Auxiliary function for reducing recursor applications. -/
 private def reduceRec (recVal : RecursorVal) (recLvls : List Level) (recArgs : Array Expr) (failK : Unit → MetaM α) (successK : Expr → MetaM α) : MetaM α :=
   let majorIdx := recVal.getMajorIdx
   if h : majorIdx < recArgs.size then do
     let major := recArgs.get ⟨majorIdx, h⟩
-    let mut major ← whnf major
+    let mut major ← if isWFRec recVal.name && (← getTransparency) == TransparencyMode.default then
+      -- If recursor is `Acc.rec` or `WellFounded.rec` and transparency is default,
+      -- then we bump transparency to .all to make sure we can unfold defs defined by WellFounded recursion.
+      -- We use this trick because we abstract nested proofs occurring in definitions.
+      -- Alternative design: do not abstract nested proofs used to justify well-founded recursion.
+      withTransparency .all <| whnf major
+    else
+      whnf major
     if recVal.k then
       major ← toCtorWhenK recVal major
     major := major.toCtorIfLit
@@ -302,7 +314,7 @@ end
   | .lam ..        => return e
   | .sort ..       => return e
   | .lit ..        => return e
-  | .bvar ..       => unreachable!
+  | .bvar ..       => panic! "loose bvar in expression"
   | .letE ..       => k e
   | .const ..      => k e
   | .app ..        => k e
@@ -708,7 +720,8 @@ mutual
       if smartUnfolding.get (← getOptions) && (← getEnv).contains (mkSmartUnfoldingNameFor declName) then
         return none
       else
-        let (some (cinfo@(ConstantInfo.defnInfo _))) ← getConstNoEx? declName | pure none
+        let some cinfo ← getConstNoEx? declName | pure none
+        unless cinfo.hasValue do return none
         deltaDefinition cinfo lvls
           (fun _ => pure none)
           (fun e => pure (some e))

src/Lean/Parser/Basic.lean

@@ -750,18 +750,18 @@ partial def identFnAux (startPos : String.Pos) (tk : Option Token) (r : Name) :
             parse r c s
           else
             mkIdResult startPos tk r c s
-    else if isIdFirst curr then
-      let startPart := i
-      let s         := takeWhileFn isIdRest c (s.next input i)
-      let stopPart  := s.pos
-      let r := .str r (input.extract startPart stopPart)
-      if isIdCont input s then
-        let s := s.next input s.pos
-        parse r c s
+      else if isIdFirst curr then
+        let startPart := i
+        let s         := takeWhileFn isIdRest c (s.next input i)
+        let stopPart  := s.pos
+        let r := .str r (input.extract startPart stopPart)
+        if isIdCont input s then
+          let s := s.next input s.pos
+          parse r c s
+        else
+          mkIdResult startPos tk r c s
       else
-        mkIdResult startPos tk r c s
-    else
-      mkTokenAndFixPos startPos tk c s
+        mkTokenAndFixPos startPos tk c s
   parse r
 
 private def isIdFirstOrBeginEscape (c : Char) : Bool :=

src/Lean/Parser/Extension.lean

@@ -177,7 +177,7 @@ inductive AliasValue (α : Type) where
 abbrev AliasTable (α) := NameMap (AliasValue α)
 
 def registerAliasCore {α} (mapRef : IO.Ref (AliasTable α)) (aliasName : Name) (value : AliasValue α) : IO Unit := do
-  unless (← IO.initializing) do throw ↑"aliases can only be registered during initialization"
+  unless (← initializing) do throw ↑"aliases can only be registered during initialization"
   if (← mapRef.get).contains aliasName then
     throw ↑s!"alias '{aliasName}' has already been declared"
   mapRef.modify (·.insert aliasName value)

src/Lean/Server/FileWorker/WidgetRequests.lean

@@ -49,7 +49,7 @@ def makePopup : WithRpcRef InfoWithCtx → RequestM (RequestTask InfoPopup)
   | ⟨i⟩ => RequestM.asTask do
     i.ctx.runMetaM i.info.lctx do
       let type? ← match (← i.info.type?) with
-        | some type => some <$> ppExprTagged type
+        | some type => some <$> (ppExprTagged =<< instantiateMVars type)
         | none => pure none
       let exprExplicit? ← match i.info with
         | Elab.Info.ofTermInfo ti =>

src/Lean/Server/Rpc/RequestHandling.lean

@@ -93,7 +93,7 @@ def registerBuiltinRpcProcedure (method : Name) paramType respType
     [RpcEncodable paramType] [RpcEncodable respType]
     (handler : paramType → RequestM (RequestTask respType)) : IO Unit := do
   let errMsg := s!"Failed to register builtin RPC call handler for '{method}'"
-  unless (← IO.initializing) do
+  unless (← initializing) do
     throw <| IO.userError s!"{errMsg}: only possible during initialization"
   if (←builtinRpcProcedures.get).contains method then
     throw <| IO.userError s!"{errMsg}: already registered"

src/Lean/Server/Watchdog.lean

@@ -210,6 +210,9 @@ section ServerM
         -- If writeLspMessage from above errors we will block here, but the main task will
         -- quit eventually anyways if that happens
         let exitCode ← fw.proc.wait
+        -- Remove surviving descendant processes, if any, such as from nested builds.
+        -- On Windows, we instead rely on elan doing this.
+        try fw.proc.kill catch _ => pure ()
         match exitCode with
         | 0 =>
           -- Worker was terminated
@@ -241,6 +244,8 @@ section ServerM
       toStdioConfig := workerCfg
       cmd           := st.workerPath.toString
       args          := #["--worker"] ++ st.args.toArray ++ #[m.uri]
+      -- open session for `kill` above
+      setsid        := true
     }
     let pendingRequestsRef ← IO.mkRef (RBMap.empty : PendingRequestMap)
     -- The task will never access itself, so this is fine

src/Lean/SubExpr.lean

@@ -11,7 +11,13 @@ namespace Lean
 
 /-- A position of a subexpression in an expression.
 
-See docstring of `SubExpr` for more detail.-/
+We use a simple encoding scheme for expression positions `Pos`:
+every `Expr` constructor has at most 3 direct expression children. Considering an expression's type
+to be one extra child as well, we can injectively map a path of `childIdxs` to a natural number
+by computing the value of the 4-ary representation `1 :: childIdxs`, since n-ary representations
+without leading zeros are unique. Note that `pos` is initialized to `1` (case `childIdxs == []`).
+
+See also `SubExpr`. -/
 def SubExpr.Pos := Nat
 
 namespace SubExpr.Pos
@@ -145,18 +151,12 @@ instance : FromJson Pos := ⟨fun j => fromJson? j >>= Pos.fromString?⟩
 
 end SubExpr.Pos
 
-/-- An expression and the position of a subexpression within this expression.
-
-Subexpressions are encoded as the current subexpression `e` and a
-position `p : Pos` denoting `e`'s position with respect to the root expression.
-
-We use a simple encoding scheme for expression positions `Pos`:
-every `Expr` constructor has at most 3 direct expression children. Considering an expression's type
-to be one extra child as well, we can injectively map a path of `childIdxs` to a natural number
-by computing the value of the 4-ary representation `1 :: childIdxs`, since n-ary representations
-without leading zeros are unique. Note that `pos` is initialized to `1` (case `childIdxs == []`).-/
+/-- A subexpression of some root expression. Both its value and its position
+within the root are stored. -/
 structure SubExpr where
+  /-- The subexpression. -/
   expr : Expr
+  /-- The position of the subexpression within the root expression. -/
   pos  : SubExpr.Pos
   deriving Inhabited
 
@@ -164,7 +164,7 @@ namespace SubExpr
 
 def mkRoot (e : Expr) : SubExpr := ⟨e, Pos.root⟩
 
-/-- Returns true if the selected subexpression is the topmost one.-/
+/-- Returns true if the selected subexpression is the topmost one. -/
 def isRoot (s : SubExpr) : Bool := s.pos.isRoot
 
 /-- Map from subexpr positions to values. -/

src/Lean/Syntax.lean

@@ -198,26 +198,29 @@ If `nFields` is set, we take that many fields from the end and keep the remainin
 as one name. For example, `` `foo.bla.boo `` with `(nFields := 1)` ↦ `` [`foo.bla, `boo] ``. -/
 def identComponents (stx : Syntax) (nFields? : Option Nat := none) : List Syntax :=
   match stx with
-  | ident (SourceInfo.original lead pos trail _) rawStr val _ =>
+  | ident si@(SourceInfo.original lead pos trail _) rawStr val _ => Id.run do
     let val := val.eraseMacroScopes
     -- With original info, we assume that `rawStr` represents `val`.
     let nameComps := nameComps val nFields?
     let rawComps := splitNameLit rawStr
-    let rawComps :=
-      if let some nFields := nFields? then
-        let nPrefix := rawComps.length - nFields
-        let prefixSz := rawComps.take nPrefix |>.foldl (init := 0) fun acc (ss : Substring) => acc + ss.bsize + 1
-        let prefixSz := prefixSz - 1 -- The last component has no dot
-        rawStr.extract 0 ⟨prefixSz⟩ :: rawComps.drop nPrefix
-      else
-        rawComps
-    assert! nameComps.length == rawComps.length
-    nameComps.zip rawComps |>.map fun (id, ss) =>
-      let off := ss.startPos - rawStr.startPos
-      let lead := if off == 0 then lead else "".toSubstring
-      let trail := if ss.stopPos == rawStr.stopPos then trail else "".toSubstring
-      let info := original lead (pos + off) trail (pos + off + ⟨ss.bsize⟩)
-      ident info ss id []
+    if !rawComps.isEmpty then
+      let rawComps :=
+        if let some nFields := nFields? then
+          let nPrefix := rawComps.length - nFields
+          let prefixSz := rawComps.take nPrefix |>.foldl (init := 0) fun acc (ss : Substring) => acc + ss.bsize + 1
+          let prefixSz := prefixSz - 1 -- The last component has no dot
+          rawStr.extract 0 ⟨prefixSz⟩ :: rawComps.drop nPrefix
+        else
+          rawComps
+      if nameComps.length == rawComps.length then
+        return nameComps.zip rawComps |>.map fun (id, ss) =>
+          let off := ss.startPos - rawStr.startPos
+          let lead := if off == 0 then lead else "".toSubstring
+          let trail := if ss.stopPos == rawStr.stopPos then trail else "".toSubstring
+          let info := original lead (pos + off) trail (pos + off + ⟨ss.bsize⟩)
+          ident info ss id []
+    -- if re-parsing failed, just give them all the same span
+    nameComps.map fun n => ident si n.toString.toSubstring n []
   | ident si _ val _ =>
     let val := val.eraseMacroScopes
     /- With non-original info:

src/Lean/Util/FindExpr.lean

@@ -4,52 +4,36 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Expr
+import Lean.Util.PtrSet
 
 namespace Lean
 namespace Expr
-
 namespace FindImpl
 
-abbrev cacheSize : USize := 8192 - 1
+unsafe abbrev FindM := StateT (PtrSet Expr) Id
 
-structure State where
-  keys : Array Expr -- Remark: our "unsafe" implementation relies on the fact that `()` is not a valid Expr
+@[inline] unsafe def checkVisited (e : Expr) : OptionT FindM Unit := do
+  if (← get).contains e then
+    failure
+  modify fun s => s.insert e
 
-abbrev FindM := StateT State Id
-
-unsafe def visited (e : Expr) (size : USize) : FindM Bool := do
-  let s ← get
-  let h := ptrAddrUnsafe e
-  let i := h % size
-  let k := s.keys.uget i lcProof
-  if ptrAddrUnsafe k == h then
-    pure true
-  else
-    modify fun s => { keys := s.keys.uset i e lcProof }
-    pure false
-
-unsafe def findM? (p : Expr → Bool) (size : USize) (e : Expr) : OptionT FindM Expr :=
+unsafe def findM? (p : Expr → Bool) (e : Expr) : OptionT FindM Expr :=
   let rec visit (e : Expr) := do
-    if (← visited e size)  then
-      failure
-    else if p e then
+    checkVisited e
+    if p e then
       pure e
     else match e with
-      | Expr.forallE _ d b _   => visit d <|> visit b
-      | Expr.lam _ d b _       => visit d <|> visit b
-      | Expr.mdata _ b         => visit b
-      | Expr.letE _ t v b _    => visit t <|> visit v <|> visit b
-      | Expr.app f a           => visit f <|> visit a
-      | Expr.proj _ _ b        => visit b
-      | _                      => failure
+      | .forallE _ d b _ => visit d <|> visit b
+      | .lam _ d b _     => visit d <|> visit b
+      | .mdata _ b       => visit b
+      | .letE _ t v b _  => visit t <|> visit v <|> visit b
+      | .app f a         => visit f <|> visit a
+      | .proj _ _ b      => visit b
+      | _                => failure
   visit e
 
-
-unsafe def initCache : State :=
-  { keys    := mkArray cacheSize.toNat (cast lcProof ()) }
-
 unsafe def findUnsafe? (p : Expr → Bool) (e : Expr) : Option Expr :=
-  Id.run <| findM? p cacheSize e |>.run' initCache
+  Id.run <| findM? p e |>.run' mkPtrSet
 
 end FindImpl
 
@@ -59,13 +43,13 @@ def find? (p : Expr → Bool) (e : Expr) : Option Expr :=
   if p e then
     some e
   else match e with
-    | Expr.forallE _ d b _   => find? p d <|> find? p b
-    | Expr.lam _ d b _       => find? p d <|> find? p b
-    | Expr.mdata _ b         => find? p b
-    | Expr.letE _ t v b _    => find? p t <|> find? p v <|> find? p b
-    | Expr.app f a           => find? p f <|> find? p a
-    | Expr.proj _ _ b        => find? p b
-    | _                      => none
+    | .forallE _ d b _ => find? p d <|> find? p b
+    | .lam _ d b _     => find? p d <|> find? p b
+    | .mdata _ b       => find? p b
+    | .letE _ t v b _  => find? p t <|> find? p v <|> find? p b
+    | .app f a         => find? p f <|> find? p a
+    | .proj _ _ b      => find? p b
+    | _                => none
 
 /-- Return true if `e` occurs in `t` -/
 def occurs (e : Expr) (t : Expr) : Bool :=
@@ -81,32 +65,31 @@ inductive FindStep where
 
 namespace FindExtImpl
 
-unsafe def findM? (p : Expr → FindStep) (size : USize) (e : Expr) : OptionT FindImpl.FindM Expr :=
+unsafe def findM? (p : Expr → FindStep) (e : Expr) : OptionT FindImpl.FindM Expr :=
   visit e
 where
   visitApp (e : Expr) :=
     match e with
-    | Expr.app f a .. => visitApp f <|> visit a
+    | .app f a .. => visitApp f <|> visit a
     | e => visit e
 
   visit (e : Expr) := do
-    if (← FindImpl.visited e size)  then
-      failure
-    else match p e with
-      | FindStep.done  => failure
-      | FindStep.found => pure e
-      | FindStep.visit =>
+    FindImpl.checkVisited e
+    match p e with
+      | .done  => failure
+      | .found => pure e
+      | .visit =>
         match e with
-        | Expr.forallE _ d b _   => visit d <|> visit b
-        | Expr.lam _ d b _       => visit d <|> visit b
-        | Expr.mdata _ b         => visit b
-        | Expr.letE _ t v b _    => visit t <|> visit v <|> visit b
-        | Expr.app ..            => visitApp e
-        | Expr.proj _ _ b        => visit b
-        | _                      => failure
+        | .forallE _ d b _ => visit d <|> visit b
+        | .lam _ d b _     => visit d <|> visit b
+        | .mdata _ b       => visit b
+        | .letE _ t v b _  => visit t <|> visit v <|> visit b
+        | .app ..          => visitApp e
+        | .proj _ _ b      => visit b
+        | _                => failure
 
 unsafe def findUnsafe? (p : Expr → FindStep) (e : Expr) : Option Expr :=
-  Id.run <| findM? p FindImpl.cacheSize e |>.run' FindImpl.initCache
+  Id.run <| findM? p e |>.run' mkPtrSet
 
 end FindExtImpl
 

src/Lean/Util/PtrSet.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2023 Leonardo de Moura. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Data.HashSet
+
+namespace Lean
+
+structure Ptr (α : Type u) where
+  value : α
+
+unsafe instance : Hashable (Ptr α) where
+  hash a := hash64 (ptrAddrUnsafe a).toUInt64
+
+unsafe instance : BEq (Ptr α) where
+  beq a b := ptrAddrUnsafe a == ptrAddrUnsafe b
+
+/--
+Set of pointers. It is a low-level auxiliary datastructure used for traversing DAGs.
+-/
+unsafe def PtrSet (α : Type) :=
+  HashSet (Ptr α)
+
+unsafe def mkPtrSet {α : Type} (capacity : Nat := 64) : PtrSet α :=
+  mkHashSet capacity
+
+unsafe abbrev PtrSet.insert (s : PtrSet α) (a : α) : PtrSet α :=
+  HashSet.insert s { value := a }
+
+unsafe abbrev PtrSet.contains (s : PtrSet α) (a : α) : Bool :=
+  HashSet.contains s { value := a }
+
+end Lean

src/Lean/Util/Trace.lean

@@ -193,7 +193,7 @@ def withTraceNode [MonadExcept ε m] [MonadLiftT BaseIO m] (cls : Name) (msg : E
     modifyTraces (oldTraces ++ ·)
     return (← MonadExcept.ofExcept res)
   let ref ← getRef
-  let mut m ← msg res
+  let mut m ← try msg res catch _ => pure m!"<exception thrown while producing trace node message>"
   if profiler.get opts || aboveThresh then
     m := m!"[{secs}s] {m}"
   addTraceNode oldTraces cls ref m collapsed

src/initialize/init.cpp

@@ -17,8 +17,8 @@ Author: Leonardo de Moura
 #include "initialize/init.h"
 
 namespace lean {
-extern "C" object* initialize_Init(object* w);
-extern "C" object* initialize_Lean(object* w);
+extern "C" object* initialize_Init(uint8_t, object* w);
+extern "C" object* initialize_Lean(uint8_t, object* w);
 
 /* Initializes the Lean runtime. Before executing any code which uses the Lean package,
 you must first call this function, and then `lean::io_mark_end_initialization`. Inbetween
@@ -26,8 +26,9 @@ these two calls, you may also have to run additional initializers for your own m
 extern "C" LEAN_EXPORT void lean_initialize() {
     save_stack_info();
     initialize_util_module();
-    consume_io_result(initialize_Init(io_mk_world()));
-    consume_io_result(initialize_Lean(io_mk_world()));
+    uint8_t builtin = 1;
+    consume_io_result(initialize_Init(builtin, io_mk_world()));
+    consume_io_result(initialize_Lean(builtin, io_mk_world()));
     initialize_kernel_module();
     init_default_print_fn();
     initialize_library_core_module();

src/kernel/type_checker.cpp

@@ -29,6 +29,7 @@ static expr * g_nat_succ     = nullptr;
 static expr * g_nat_add      = nullptr;
 static expr * g_nat_sub      = nullptr;
 static expr * g_nat_mul      = nullptr;
+static expr * g_nat_pow      = nullptr;
 static expr * g_nat_mod      = nullptr;
 static expr * g_nat_div      = nullptr;
 static expr * g_nat_beq      = nullptr;
@@ -601,6 +602,7 @@ optional<expr> type_checker::reduce_nat(expr const & e) {
         if (f == *g_nat_add) return reduce_bin_nat_op(nat_add, e);
         if (f == *g_nat_sub) return reduce_bin_nat_op(nat_sub, e);
         if (f == *g_nat_mul) return reduce_bin_nat_op(nat_mul, e);
+        if (f == *g_nat_pow) return reduce_bin_nat_op(nat_pow, e);
         if (f == *g_nat_mod) return reduce_bin_nat_op(nat_mod, e);
         if (f == *g_nat_div) return reduce_bin_nat_op(nat_div, e);
         if (f == *g_nat_beq) return reduce_bin_nat_pred(nat_eq, e);
@@ -1146,6 +1148,8 @@ void initialize_type_checker() {
     mark_persistent(g_nat_sub->raw());
     g_nat_mul      = new expr(mk_constant(name{"Nat", "mul"}));
     mark_persistent(g_nat_mul->raw());
+    g_nat_pow      = new expr(mk_constant(name{"Nat", "pow"}));
+    mark_persistent(g_nat_pow->raw());
     g_nat_div      = new expr(mk_constant(name{"Nat", "div"}));
     mark_persistent(g_nat_div->raw());
     g_nat_mod      = new expr(mk_constant(name{"Nat", "mod"}));
@@ -1171,6 +1175,7 @@ void finalize_type_checker() {
     delete g_nat_add;
     delete g_nat_sub;
     delete g_nat_mul;
+    delete g_nat_pow;
     delete g_nat_div;
     delete g_nat_mod;
     delete g_nat_beq;

src/lake/.gitattributes

@@ -0,0 +1 @@
+*.sh text eol=lf

src/lake/.github/workflows/ci.yml

@@ -0,0 +1,72 @@
+name: CI
+
+on: [ push, pull_request ]
+
+jobs:
+  skip_check:
+    name: Skip Check
+    continue-on-error: true
+    runs-on: ubuntu-latest
+    outputs:
+      should_skip: ${{ steps.skip_check.outputs.should_skip }}
+    steps:
+      - id: skip_check
+        uses: fkirc/skip-duplicate-actions@v4
+        with:
+          concurrent_skipping: 'same_content_newer'
+          paths_ignore: '["README.md", "LICENSE"]'
+
+  build:
+    needs: skip_check
+    name: ${{ matrix.name || 'Build' }}
+    if: ${{ needs.skip_check.outputs.should_skip != 'true' }}
+    runs-on: ${{ matrix.os }}
+    defaults:
+      run:
+        shell: ${{ matrix.shell || 'sh' }}
+    strategy:
+      matrix:
+        include:
+        - name: Ubuntu
+          os: ubuntu-latest
+        - name: MacOS
+          os: macos-latest
+        - name: Windows
+          os: windows-latest
+          shell: msys2 {0}
+      # complete all jobs
+      fail-fast: false
+    steps:
+    - name: Install MSYS2 (Windows)
+      if: matrix.os == 'windows-latest'
+      uses: msys2/setup-msys2@v2
+      with:
+        path-type: inherit
+        install: curl unzip make diffutils mingw-w64-x86_64-gcc mingw-w64-x86_64-gmp
+    - name: Install Elan
+      shell: bash -euo pipefail {0}
+      run: |
+        curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none
+        echo "$HOME/.elan/bin" >> $GITHUB_PATH
+    - name: Checkout
+      uses: actions/checkout@v2
+    - name: Check Lean
+      run: lean --version
+    - name: Build & Time
+      run: ./time.sh -j4
+    - name: Upload Build
+      continue-on-error: true
+      uses: actions/upload-artifact@v2
+      with:
+        name: ${{ matrix.os }}
+        path: build
+    - name: Check Lake
+      run: make check-lake
+    - name: Test Lake
+      run: make test-ci
+    - name: Time Bootstrap
+      run: make time-bootstrap
+    - name: Check Bootstrap
+      run: make check-bootstrap
+    - name: Test Bootstrapped Lake
+      run: make test-bootstrapped -j4

src/lake/.gitignore

@@ -0,0 +1,5 @@
+/build
+produced.out
+result*
+# Do not commit the flake lockfile to avoid having to maintain it
+flake.lock

src/lake/LICENSE

@@ -0,0 +1,70 @@
+Apache License 2.0 (Apache)
+Apache License
+Version 2.0, January 2004
+http://www.apache.org/licenses/
+
+TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
+
+1. Definitions.
+
+"License" shall mean the terms and conditions for use, reproduction, and distribution as defined by Sections 1 through 9 of this document.
+
+"Licensor" shall mean the copyright owner or entity authorized by the copyright owner that is granting the License.
+
+"Legal Entity" shall mean the union of the acting entity and all other entities that control, are controlled by, or are under common control with that entity. For the purposes of this definition, "control" means (i) the power, direct or indirect, to cause the direction or management of such entity, whether by contract or otherwise, or (ii) ownership of fifty percent (50%) or more of the outstanding shares, or (iii) beneficial ownership of such entity.
+
+"You" (or "Your") shall mean an individual or Legal Entity exercising permissions granted by this License.
+
+"Source" form shall mean the preferred form for making modifications, including but not limited to software source code, documentation source, and configuration files.
+
+"Object" form shall mean any form resulting from mechanical transformation or translation of a Source form, including but not limited to compiled object code, generated documentation, and conversions to other media types.
+
+"Work" shall mean the work of authorship, whether in Source or Object form, made available under the License, as indicated by a copyright notice that is included in or attached to the work (an example is provided in the Appendix below).
+
+"Derivative Works" shall mean any work, whether in Source or Object form, that is based on (or derived from) the Work and for which the editorial revisions, annotations, elaborations, or other modifications represent, as a whole, an original work of authorship. For the purposes of this License, Derivative Works shall not include works that remain separable from, or merely link (or bind by name) to the interfaces of, the Work and Derivative Works thereof.
+
+"Contribution" shall mean any work of authorship, including the original version of the Work and any modifications or additions to that Work or Derivative Works thereof, that is intentionally submitted to Licensor for inclusion in the Work by the copyright owner or by an individual or Legal Entity authorized to submit on behalf of the copyright owner. For the purposes of this definition, "submitted" means any form of electronic, verbal, or written communication sent to the Licensor or its representatives, including but not limited to communication on electronic mailing lists, source code control systems, and issue tracking systems that are managed by, or on behalf of, the Licensor for the purpose of discussing and improving the Work, but excluding communication that is conspicuously marked or otherwise designated in writing by the copyright owner as "Not a Contribution."
+
+"Contributor" shall mean Licensor and any individual or Legal Entity on behalf of whom a Contribution has been received by Licensor and subsequently incorporated within the Work.
+
+2. Grant of Copyright License.
+
+Subject to the terms and conditions of this License, each Contributor hereby grants to You a perpetual, worldwide, non-exclusive, no-charge, royalty-free, irrevocable copyright license to reproduce, prepare Derivative Works of, publicly display, publicly perform, sublicense, and distribute the Work and such Derivative Works in Source or Object form.
+
+3. Grant of Patent License.
+
+Subject to the terms and conditions of this License, each Contributor hereby grants to You a perpetual, worldwide, non-exclusive, no-charge, royalty-free, irrevocable (except as stated in this section) patent license to make, have made, use, offer to sell, sell, import, and otherwise transfer the Work, where such license applies only to those patent claims licensable by such Contributor that are necessarily infringed by their Contribution(s) alone or by combination of their Contribution(s) with the Work to which such Contribution(s) was submitted. If You institute patent litigation against any entity (including a cross-claim or counterclaim in a lawsuit) alleging that the Work or a Contribution incorporated within the Work constitutes direct or contributory patent infringement, then any patent licenses granted to You under this License for that Work shall terminate as of the date such litigation is filed.
+
+4. Redistribution.
+
+You may reproduce and distribute copies of the Work or Derivative Works thereof in any medium, with or without modifications, and in Source or Object form, provided that You meet the following conditions:
+
+1. You must give any other recipients of the Work or Derivative Works a copy of this License; and
+
+2. You must cause any modified files to carry prominent notices stating that You changed the files; and
+
+3. You must retain, in the Source form of any Derivative Works that You distribute, all copyright, patent, trademark, and attribution notices from the Source form of the Work, excluding those notices that do not pertain to any part of the Derivative Works; and
+
+4. If the Work includes a "NOTICE" text file as part of its distribution, then any Derivative Works that You distribute must include a readable copy of the attribution notices contained within such NOTICE file, excluding those notices that do not pertain to any part of the Derivative Works, in at least one of the following places: within a NOTICE text file distributed as part of the Derivative Works; within the Source form or documentation, if provided along with the Derivative Works; or, within a display generated by the Derivative Works, if and wherever such third-party notices normally appear. The contents of the NOTICE file are for informational purposes only and do not modify the License. You may add Your own attribution notices within Derivative Works that You distribute, alongside or as an addendum to the NOTICE text from the Work, provided that such additional attribution notices cannot be construed as modifying the License.
+
+You may add Your own copyright statement to Your modifications and may provide additional or different license terms and conditions for use, reproduction, or distribution of Your modifications, or for any such Derivative Works as a whole, provided Your use, reproduction, and distribution of the Work otherwise complies with the conditions stated in this License.
+
+5. Submission of Contributions.
+
+Unless You explicitly state otherwise, any Contribution intentionally submitted for inclusion in the Work by You to the Licensor shall be under the terms and conditions of this License, without any additional terms or conditions. Notwithstanding the above, nothing herein shall supersede or modify the terms of any separate license agreement you may have executed with Licensor regarding such Contributions.
+
+6. Trademarks.
+
+This License does not grant permission to use the trade names, trademarks, service marks, or product names of the Licensor, except as required for reasonable and customary use in describing the origin of the Work and reproducing the content of the NOTICE file.
+
+7. Disclaimer of Warranty.
+
+Unless required by applicable law or agreed to in writing, Licensor provides the Work (and each Contributor provides its Contributions) on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied, including, without limitation, any warranties or conditions of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A PARTICULAR PURPOSE. You are solely responsible for determining the appropriateness of using or redistributing the Work and assume any risks associated with Your exercise of permissions under this License.
+
+8. Limitation of Liability.
+
+In no event and under no legal theory, whether in tort (including negligence), contract, or otherwise, unless required by applicable law (such as deliberate and grossly negligent acts) or agreed to in writing, shall any Contributor be liable to You for damages, including any direct, indirect, special, incidental, or consequential damages of any character arising as a result of this License or out of the use or inability to use the Work (including but not limited to damages for loss of goodwill, work stoppage, computer failure or malfunction, or any and all other commercial damages or losses), even if such Contributor has been advised of the possibility of such damages.
+
+9. Accepting Warranty or Additional Liability.
+
+While redistributing the Work or Derivative Works thereof, You may choose to offer, and charge a fee for, acceptance of support, warranty, indemnity, or other liability obligations and/or rights consistent with this License. However, in accepting such obligations, You may act only on Your own behalf and on Your sole responsibility, not on behalf of any other Contributor, and only if You agree to indemnify, defend, and hold each Contributor harmless for any liability incurred by, or claims asserted against, such Contributor by reason of your accepting any such warranty or additional liability.

src/lake/Lake.lean

@@ -0,0 +1,10 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Build
+import Lake.Config
+import Lake.DSL
+import Lake.Version
+import Lake.CLI.Actions

src/lake/Lake/Build.lean

@@ -0,0 +1,12 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Build.Monad
+import Lake.Build.Actions
+import Lake.Build.Index
+import Lake.Build.Module
+import Lake.Build.Package
+import Lake.Build.Library
+import Lake.Build.Imports

src/lake/Lake/Build/Actions.lean

@@ -0,0 +1,123 @@
+/-
+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, Mac Malone
+-/
+import Lake.Util.Proc
+import Lake.Util.NativeLib
+import Lake.Build.Context
+
+namespace Lake
+open System
+
+def createParentDirs (path : FilePath) : IO Unit := do
+  if let some dir := path.parent then IO.FS.createDirAll dir
+
+def compileLeanModule (name : String) (leanFile : FilePath)
+(oleanFile? ileanFile? cFile? : Option FilePath)
+(leanPath : SearchPath := []) (rootDir : FilePath := ".")
+(dynlibs : Array FilePath := #[]) (dynlibPath : SearchPath := {})
+(leanArgs : Array String := #[]) (lean : FilePath := "lean")
+: BuildM Unit := do
+  logStep s!"Building {name}"
+  let mut args := leanArgs ++
+    #[leanFile.toString, "-R", rootDir.toString]
+  if let some oleanFile := oleanFile? then
+    createParentDirs oleanFile
+    args := args ++ #["-o", oleanFile.toString]
+  if let some ileanFile := ileanFile? then
+    createParentDirs ileanFile
+    args := args ++ #["-i", ileanFile.toString]
+  if let some cFile := cFile? then
+    createParentDirs cFile
+    args := args ++ #["-c", cFile.toString]
+  for dynlib in dynlibs do
+    args := args.push s!"--load-dynlib={dynlib}"
+  proc {
+    args
+    cmd := lean.toString
+    env := #[
+      ("LEAN_PATH", leanPath.toString),
+      (sharedLibPathEnvVar, (← getSearchPath sharedLibPathEnvVar) ++ dynlibPath |>.toString)
+    ]
+  }
+
+def compileO (name : String) (oFile srcFile : FilePath)
+(moreArgs : Array String := #[]) (compiler : FilePath := "cc") : BuildM Unit := do
+  logStep s!"Compiling {name}"
+  createParentDirs oFile
+  proc {
+    cmd := compiler.toString
+    args := #["-c", "-o", oFile.toString, srcFile.toString] ++ moreArgs
+  }
+
+def compileStaticLib (name : String) (libFile : FilePath)
+(oFiles : Array FilePath) (ar : FilePath := "ar") : BuildM Unit := do
+  logStep s!"Creating {name}"
+  createParentDirs libFile
+  proc {
+    cmd := ar.toString
+    args := #["rcs", libFile.toString] ++ oFiles.map toString
+  }
+
+def compileSharedLib (name : String) (libFile : FilePath)
+(linkArgs : Array String) (linker : FilePath := "cc") : BuildM Unit := do
+  logStep s!"Linking {name}"
+  createParentDirs libFile
+  proc {
+    cmd := linker.toString
+    args := #["-shared", "-o", libFile.toString] ++ linkArgs
+  }
+
+def compileExe (name : String) (binFile : FilePath) (linkFiles : Array FilePath)
+(linkArgs : Array String := #[]) (linker : FilePath := "cc") : BuildM Unit := do
+  logStep s!"Linking {name}"
+  createParentDirs binFile
+  proc {
+    cmd := linker.toString
+    args := #["-o", binFile.toString] ++ linkFiles.map toString ++ linkArgs
+  }
+
+/-- Download a file using `curl`, clobbering any existing file. -/
+def download (name : String) (url : String) (file : FilePath) : LogIO PUnit := do
+  logInfo s!"Downloading {name}"
+  if (← file.pathExists) then
+    IO.FS.removeFile file
+  else
+    createParentDirs file
+  let args :=
+    if (← getIsVerbose) then #[] else #["-s"]
+  proc (quiet := true) {
+    cmd := "curl"
+    args := args ++ #["-f", "-o", file.toString, "-L", url]
+  }
+
+/-- Unpack an archive `file` using `tar` into the directory `dir`. -/
+def untar (name : String) (file : FilePath) (dir : FilePath) (gzip := true) : LogIO PUnit := do
+  logInfo s!"Unpacking {name}"
+  let mut opts := "-x"
+  if (← getIsVerbose) then
+    opts := opts.push 'v'
+  if gzip then
+    opts := opts.push 'z'
+  proc {
+    cmd := "tar",
+    args := #[opts, "-f", file.toString, "-C", dir.toString]
+  }
+
+/-- Pack a directory `dir` using `tar` into the archive `file`. -/
+def tar (name : String) (dir : FilePath) (file : FilePath)
+(gzip := true) (excludePaths : Array FilePath := #[]) : LogIO PUnit := do
+  logInfo s!"Packing {name}"
+  createParentDirs file
+  let mut args := #["-c"]
+  if gzip then
+    args := args.push "-z"
+  if (← getIsVerbose) then
+    args := args.push "-v"
+  for path in excludePaths do
+    args := args.push s!"--exclude={path}"
+  proc {
+    cmd := "tar"
+    args := args ++ #["-f", file.toString, "-C", dir.toString, "."]
+  }

src/lake/Lake/Build/Common.lean

@@ -0,0 +1,118 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Build.Job
+import Lake.Build.Actions
+import Lake.Build.Monad
+
+open System
+namespace Lake
+
+/-! # General Utilities -/
+
+@[inline] def inputFile (path : FilePath) : SchedulerM (BuildJob FilePath) :=
+  Job.async <| (path, ·) <$> computeTrace path
+
+@[inline] def buildUnlessUpToDate [CheckExists ι] [GetMTime ι] (info : ι)
+(depTrace : BuildTrace) (traceFile : FilePath) (build : JobM PUnit) : JobM PUnit := do
+  let isOldMode ← getIsOldMode
+  let upToDate ←
+    if isOldMode then
+      depTrace.checkAgainstTime info
+    else
+      depTrace.checkAgainstFile info traceFile
+  unless upToDate do
+    build
+    unless isOldMode do
+      depTrace.writeToFile traceFile
+
+@[inline] def buildFileUnlessUpToDate (file : FilePath)
+(depTrace : BuildTrace) (build : BuildM PUnit) : BuildM BuildTrace := do
+  let traceFile := FilePath.mk <| file.toString ++ ".trace"
+  buildUnlessUpToDate file depTrace traceFile build
+  computeTrace file
+
+@[inline] def buildFileAfterDep
+(file : FilePath) (dep : BuildJob α) (build : α → BuildM PUnit)
+(extraDepTrace : BuildM _ := pure BuildTrace.nil) : SchedulerM (BuildJob FilePath) :=
+  dep.bindSync fun depInfo depTrace => do
+    let depTrace := depTrace.mix (← extraDepTrace)
+    let trace ← buildFileUnlessUpToDate file depTrace <| build depInfo
+    return (file, trace)
+
+@[inline] def buildFileAfterDepList
+(file : FilePath) (deps : List (BuildJob α)) (build : List α → BuildM PUnit)
+(extraDepTrace : BuildM _ := pure BuildTrace.nil) : SchedulerM (BuildJob FilePath) := do
+  buildFileAfterDep file (← BuildJob.collectList deps) build extraDepTrace
+
+@[inline] def buildFileAfterDepArray
+(file : FilePath) (deps : Array (BuildJob α)) (build : Array α → BuildM PUnit)
+(extraDepTrace : BuildM _ := pure BuildTrace.nil) : SchedulerM (BuildJob FilePath) := do
+  buildFileAfterDep file (← BuildJob.collectArray deps) build extraDepTrace
+
+/-! # Common Builds -/
+
+def buildO (name : String)
+(oFile : FilePath) (srcJob : BuildJob FilePath)
+(args : Array String := #[]) (compiler : FilePath := "cc") : SchedulerM (BuildJob FilePath) :=
+  buildFileAfterDep oFile srcJob (extraDepTrace := computeHash args) fun srcFile => do
+     compileO name oFile srcFile args compiler
+
+def buildLeanO (name : String)
+(oFile : FilePath) (srcJob : BuildJob FilePath)
+(args : Array String := #[]) : SchedulerM (BuildJob FilePath) :=
+  buildFileAfterDep oFile srcJob (extraDepTrace := computeHash args) fun srcFile => do
+     compileO name oFile srcFile args (← getLeanc)
+
+def buildStaticLib (libFile : FilePath)
+(oFileJobs : Array (BuildJob FilePath)) : SchedulerM (BuildJob FilePath) :=
+  let name := libFile.fileName.getD libFile.toString
+  buildFileAfterDepArray libFile oFileJobs fun oFiles => do
+    compileStaticLib name libFile oFiles (← getLeanAr)
+
+def buildLeanSharedLib
+(libFile : FilePath) (linkJobs : Array (BuildJob FilePath))
+(linkArgs : Array String := #[]) : SchedulerM (BuildJob FilePath) :=
+  let name := libFile.fileName.getD libFile.toString
+  buildFileAfterDepArray libFile linkJobs
+  (extraDepTrace := computeHash linkArgs) fun links => do
+    compileSharedLib name libFile (links.map toString ++ linkArgs) (← getLeanc)
+
+def buildLeanExe
+(exeFile : FilePath) (linkJobs : Array (BuildJob FilePath))
+(linkArgs : Array String := #[]) : SchedulerM (BuildJob FilePath) :=
+  let name := exeFile.fileName.getD exeFile.toString
+  buildFileAfterDepArray exeFile linkJobs
+  (extraDepTrace := computeHash linkArgs) fun links => do
+    compileExe name exeFile links linkArgs (← getLeanc)
+
+def buildLeanSharedLibOfStatic (staticLibJob : BuildJob FilePath)
+(linkArgs : Array String := #[]) : SchedulerM (BuildJob FilePath) :=
+  staticLibJob.bindSync fun staticLib staticTrace => do
+    let dynlib := staticLib.withExtension sharedLibExt
+    let baseArgs :=
+      if System.Platform.isOSX then
+        #[s!"-Wl,-force_load,{staticLib}"]
+      else
+        #["-Wl,--whole-archive", staticLib.toString, "-Wl,--no-whole-archive"]
+    let args := baseArgs ++ linkArgs
+    let depTrace := staticTrace.mix (← computeHash args)
+    let trace ← buildFileUnlessUpToDate dynlib depTrace do
+      let name := dynlib.fileName.getD dynlib.toString
+      compileSharedLib name dynlib args (← getLeanc)
+    return (dynlib, trace)
+
+def computeDynlibOfShared
+(sharedLibTarget : BuildJob FilePath) : SchedulerM (BuildJob Dynlib) :=
+  sharedLibTarget.bindSync fun sharedLib trace => do
+    if let some stem := sharedLib.fileStem then
+      if Platform.isWindows then
+        return ({path := sharedLib, name := stem}, trace)
+      else if stem.startsWith "lib" then
+        return ({path := sharedLib, name := stem.drop 3}, trace)
+      else
+        error s!"shared library `{sharedLib}` does not start with `lib`; this is not supported on Unix"
+    else
+      error s!"shared library `{sharedLib}` has no file name"

src/lake/Lake/Build/Context.lean

@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Util.Log
+import Lake.Util.Task
+import Lake.Util.Error
+import Lake.Util.OptionIO
+import Lake.Config.Context
+import Lake.Build.Trace
+import Lake.Build.Store
+import Lake.Build.Topological
+
+open System
+namespace Lake
+
+/-- A Lake context with some additional caching for builds. -/
+structure BuildContext extends Context where
+  leanTrace : BuildTrace
+  oldMode : Bool := false
+  startedBuilds : IO.Ref Nat
+  finishedBuilds : IO.Ref Nat
+
+/-- A transformer to equip a monad with a `BuildContext`. -/
+abbrev BuildT := ReaderT BuildContext
+
+/-- The monad for the Lake build manager. -/
+abbrev SchedulerM := BuildT <| LogT BaseIO
+
+/-- The core monad for Lake builds. -/
+abbrev BuildM := BuildT LogIO
+
+/-- A transformer to equip a monad with a Lake build store. -/
+abbrev BuildStoreT := StateT BuildStore
+
+/-- A Lake build cycle. -/
+abbrev BuildCycle := Cycle BuildKey
+
+/-- A transformer for monads that may encounter a build cycle. -/
+abbrev BuildCycleT := CycleT BuildKey
+
+/-- A recursive build of a Lake build store that may encounter a cycle. -/
+abbrev RecBuildM := BuildCycleT <| BuildStoreT BuildM
+
+instance [Pure m] : MonadLift LakeM (BuildT m) where
+  monadLift x := fun ctx => pure <| x.run ctx.toContext
+
+@[inline] def BuildM.run (ctx : BuildContext) (self : BuildM α) : LogIO α :=
+  self ctx
+
+def BuildM.catchFailure (f : Unit → BaseIO α) (self : BuildM α) : SchedulerM α :=
+  fun ctx logMethods => self ctx logMethods |>.catchFailure f
+
+def logStep (message : String) : BuildM Unit := do
+  let done ← (← read).finishedBuilds.get
+  let started ← (← read).startedBuilds.get
+  logInfo s!"[{done}/{started}] {message}"

src/lake/Lake/Build/Data.lean

@@ -0,0 +1,131 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Build.Key
+import Lake.Util.Family
+
+open Lean
+namespace Lake
+
+--------------------------------------------------------------------------------
+/-! ## Build Data Subtypes                                                    -/
+--------------------------------------------------------------------------------
+
+/--
+The open type family which maps a module facet's name to its build data
+in the Lake build store. For example, a transitive × direct import pair
+for the `lean.imports` facet or an active build target for `lean.c`.
+
+It is an open type, meaning additional mappings can be add lazily
+as needed (via `module_data`).
+-/
+opaque ModuleData (facet : Name) : Type
+
+/--
+The open type family which maps a package facet's name to its build data
+in the Lake build store. For example, a transitive dependencies of the package
+for the facet `deps`.
+
+It is an open type, meaning additional mappings can be add lazily
+as needed (via `package_data`).
+-/
+opaque PackageData (facet : Name) : Type
+
+/--
+The open type family which maps a (builtin) Lake target's (e.g., `extern_lib`)
+facet to its associated build data. For example, an active build target for
+the `externLib.static` facet.
+
+It is an open type, meaning additional mappings can be add lazily
+as needed (via `target_data`).
+-/
+opaque TargetData (facet : Name) : Type
+
+/-
+The open type family which maps a library facet's name to its build data
+in the Lake build store. For example, an active build target for the `static`
+facet.
+
+It is an open type, meaning additional mappings can be add lazily
+as needed (via `library_data`).
+-/
+abbrev LibraryData (facet : Name) := TargetData (`leanLib ++ facet)
+
+instance [h : FamilyOut LibraryData facet α] : FamilyDef TargetData (`leanLib ++ facet) α :=
+  ⟨by simp [h.family_key_eq_type]⟩
+
+instance [h : FamilyOut TargetData (`leanLib ++ facet) α] : FamilyDef LibraryData facet α :=
+  ⟨h.family_key_eq_type⟩
+
+/--
+The open type family which maps a custom target (package × target name) to
+its build data in the Lake build store.
+
+It is an open type, meaning additional mappings can be add lazily
+as needed (via `custom_data`).
+-/
+opaque CustomData (target : Name × Name) : Type
+
+--------------------------------------------------------------------------------
+/-! ## Build Data                                                             -/
+--------------------------------------------------------------------------------
+
+/--
+A mapping between a build key and its associated build data in the store.
+It is a simple type function composed of the separate open type families for
+modules facets, package facets, Lake target facets, and custom targets.
+-/
+abbrev BuildData : BuildKey → Type
+| .moduleFacet _ f => ModuleData f
+| .packageFacet _ f => PackageData f
+| .targetFacet _ _ f => TargetData f
+| .customTarget p t => CustomData (p, t)
+
+instance (priority := low) : FamilyDef BuildData (.moduleFacet m f) (ModuleData f) := ⟨rfl⟩
+instance (priority := low) : FamilyDef BuildData (.packageFacet p f) (PackageData f) := ⟨rfl⟩
+instance (priority := low) : FamilyDef BuildData (.targetFacet p t f) (TargetData f) := ⟨rfl⟩
+instance (priority := low)  : FamilyDef BuildData (.customTarget p t) (CustomData (p,t)) := ⟨rfl⟩
+
+--------------------------------------------------------------------------------
+/-! ## Macros for Declaring Build Data                                        -/
+--------------------------------------------------------------------------------
+
+/-- Macro for declaring new `PackageData`. -/
+scoped macro (name := packageDataDecl) doc?:optional(Parser.Command.docComment)
+"package_data " id:ident " : " ty:term : command => do
+  let dty := mkCIdentFrom (← getRef) ``PackageData
+  let key := Name.quoteFrom id id.getId
+  `($[$doc?]? family_def $id : $dty $key := $ty)
+
+/-- Macro for declaring new `ModuleData`. -/
+scoped macro (name := moduleDataDecl) doc?:optional(Parser.Command.docComment)
+"module_data " id:ident " : " ty:term : command => do
+  let dty := mkCIdentFrom (← getRef) ``ModuleData
+  let key := Name.quoteFrom id id.getId
+  `($[$doc?]? family_def $id : $dty $key := $ty)
+
+/-- Macro for declaring new `TargetData` for libraries. -/
+scoped macro (name := libraryDataDecl) doc?:optional(Parser.Command.docComment)
+"library_data " id:ident " : " ty:term : command => do
+  let dty := mkCIdentFrom (← getRef) ``TargetData
+  let key := Name.quoteFrom id id.getId
+  let id := mkIdentFrom id <| id.getId.modifyBase (`leanLib ++ ·)
+  `($[$doc?]? family_def $id : $dty (`leanLib ++ $key) := $ty)
+
+/-- Macro for declaring new `TargetData`. -/
+scoped macro (name := targetDataDecl) doc?:optional(Parser.Command.docComment)
+"target_data " id:ident " : " ty:term : command => do
+  let dty := mkCIdentFrom (← getRef) ``TargetData
+  let key := Name.quoteFrom id id.getId
+  `($[$doc?]? family_def $id : $dty $key := $ty)
+
+/-- Macro for declaring new `CustomData`. -/
+scoped macro (name := customDataDecl) doc?:optional(Parser.Command.docComment)
+"custom_data " pkg:ident tgt:ident " : " ty:term : command => do
+  let dty := mkCIdentFrom (← getRef) ``CustomData
+  let id := mkIdentFrom tgt (pkg.getId ++ tgt.getId)
+  let pkg := Name.quoteFrom pkg pkg.getId
+  let tgt := Name.quoteFrom pkg tgt.getId
+  `($[$doc?]? family_def $id : $dty ($pkg, $tgt) := $ty)

src/lake/Lake/Build/Executable.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Build.Common
+
+namespace Lake
+
+/-- Get the Lean executable in the workspace with the configuration's name. -/
+@[inline] def LeanExeConfig.get (self : LeanExeConfig)
+[Monad m] [MonadError m] [MonadLake m] : m LeanExe := do
+  let some exe ← findLeanExe? self.name
+    | error "Lean executable '{self.name}' does not exist in the workspace"
+  return exe
+
+
+/-- Fetch the build of the Lean executable. -/
+@[inline] def LeanExeConfig.fetch
+(self : LeanExeConfig) : IndexBuildM (BuildJob FilePath) := do
+  (← self.get).exe.fetch
+
+/-! # Build Executable -/
+
+protected def LeanExe.recBuildExe
+(self : LeanExe) : IndexBuildM (BuildJob FilePath) := do
+  let imports ← self.root.transImports.fetch
+  let mut linkJobs := #[← self.root.o.fetch]
+  for mod in imports do for facet in mod.nativeFacets do
+    linkJobs := linkJobs.push <| ← fetch <| mod.facet facet.name
+  let deps := (← fetch <| self.pkg.facet `deps).push self.pkg
+  for dep in deps do for lib in dep.externLibs do
+    linkJobs := linkJobs.push <| ← lib.static.fetch
+  buildLeanExe self.file linkJobs self.linkArgs

src/lake/Lake/Build/Facets.lean

@@ -0,0 +1,126 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Build.Job
+import Lake.Build.Data
+
+/-!
+# Simple Builtin Facet Declarations
+
+This module contains the definitions of most of the builtin facets.
+The others are defined `Build.Info`. The facets there require configuration
+definitions (e.g., `Module`), and some of the facets here are used in said
+definitions.
+-/
+
+namespace Lake
+export System (SearchPath FilePath)
+
+/-- A dynamic/shared library for linking. -/
+structure Dynlib where
+  /-- Library file path. -/
+  path : FilePath
+  /-- Library name without platform-specific prefix/suffix (for `-l`). -/
+  name : String
+
+/-- Optional library directory (for `-L`). -/
+def Dynlib.dir? (self : Dynlib) : Option FilePath :=
+  self.path.parent
+
+/-! ## Module Facets -/
+
+/-- A module facet name along with proof of its data type. -/
+structure ModuleFacet (α) where
+  /-- The name of the module facet. -/
+  name : Name
+  /-- Proof that module's facet build result is of type α. -/
+  data_eq : ModuleData name = α
+  deriving Repr
+
+instance (facet : ModuleFacet α) : FamilyDef ModuleData facet.name α :=
+  ⟨facet.data_eq⟩
+
+instance [FamilyOut ModuleData facet α] : CoeDep Name facet (ModuleFacet α) :=
+  ⟨facet, FamilyOut.family_key_eq_type⟩
+
+/--
+The facet which builds all of a module's dependencies
+(i.e., transitive local imports and `--load-dynlib` shared libraries).
+Returns the list of shared libraries to load along with their search path.
+-/
+abbrev Module.depsFacet := `deps
+module_data deps : BuildJob (SearchPath × Array FilePath)
+
+/--
+The core compilation / elaboration of the Lean file via `lean`,
+which produce the Lean binaries of the module (i.e., `olean`, `ilean`, `c`).
+Its trace just includes its dependencies.
+-/
+abbrev Module.leanBinFacet := `bin
+module_data bin : BuildJob Unit
+
+/--
+The `leanBinFacet` combined with the module's trace
+(i.e., the trace of its `olean` and `ilean`).
+It is the facet used for building a Lean import of a module.
+-/
+abbrev Module.importBinFacet := `importBin
+module_data importBin : BuildJob Unit
+
+/-- The `olean` file produced by `lean`  -/
+abbrev Module.oleanFacet := `olean
+module_data olean : BuildJob FilePath
+
+/-- The `ilean` file produced by `lean` -/
+abbrev Module.ileanFacet := `ilean
+module_data ilean : BuildJob FilePath
+
+/-- The C file built from the Lean file via `lean` -/
+abbrev Module.cFacet := `c
+module_data c : BuildJob FilePath
+
+/-- The object file built from `lean.c` -/
+abbrev Module.oFacet := `o
+module_data o : BuildJob FilePath
+
+/-! ## Package Facets -/
+
+/-- The package's cloud build release. -/
+abbrev Package.releaseFacet := `release
+package_data release : BuildJob Unit
+
+/-- The package's `extraDepTarget` mixed with its transitive dependencies'. -/
+abbrev Package.extraDepFacet := `extraDep
+package_data extraDep : BuildJob Unit
+
+/-! ## Target Facets -/
+
+/-- A Lean library's Lean libraries. -/
+abbrev LeanLib.leanFacet := `lean
+library_data lean : BuildJob Unit
+
+/-- A Lean library's static binary. -/
+abbrev LeanLib.staticFacet := `static
+library_data static : BuildJob FilePath
+
+/-- A Lean library's shared binary. -/
+abbrev LeanLib.sharedFacet := `shared
+library_data shared : BuildJob FilePath
+
+/-- A Lean binary executable. -/
+abbrev LeanExe.exeFacet := `leanExe
+target_data leanExe : BuildJob FilePath
+
+/-- A external library's static binary. -/
+abbrev ExternLib.staticFacet := `externLib.static
+target_data externLib.static : BuildJob FilePath
+
+/-- A external library's shared binary. -/
+abbrev ExternLib.sharedFacet := `externLib.shared
+target_data externLib.shared : BuildJob FilePath
+
+/-- A external library's dynlib. -/
+abbrev ExternLib.dynlibFacet := `externLib.dynlib
+target_data externLib.dynlib : BuildJob Dynlib

src/lake/Lake/Build/Imports.lean

@@ -0,0 +1,70 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Build.Index
+
+/-!
+Definitions to support `lake print-paths` builds.
+-/
+
+open System
+namespace Lake
+
+/--
+Construct an `Array` of `Module`s for the workspace-local modules of
+a `List` of import strings.
+-/
+def Workspace.processImportList
+(imports : List String) (self : Workspace) : Array Module := Id.run do
+  let mut localImports := #[]
+  for imp in imports do
+    if let some mod := self.findModule? imp.toName then
+      localImports := localImports.push mod
+  return localImports
+
+/--
+Recursively build a set of imported modules and return their build jobs,
+the build jobs of their precompiled modules and the build jobs of said modules'
+external libraries.
+-/
+def recBuildImports (imports : Array Module)
+: IndexBuildM (Array (BuildJob Unit) × Array (BuildJob Dynlib) × Array (BuildJob Dynlib)) := do
+  let mut modJobs := #[]
+  let mut precompileImports := OrdModuleSet.empty
+  for mod in imports do
+    if mod.shouldPrecompile then
+      precompileImports := precompileImports.appendArray (← mod.transImports.fetch) |>.insert mod
+    else
+      precompileImports := precompileImports.appendArray (← mod.precompileImports.fetch)
+    modJobs := modJobs.push <| ← mod.leanBin.fetch
+  let pkgs := precompileImports.foldl (·.insert ·.pkg) OrdPackageSet.empty |>.toArray
+  let externJobs ← pkgs.concatMapM (·.externLibs.mapM (·.dynlib.fetch))
+  let precompileJobs ← precompileImports.toArray.mapM (·.dynlib.fetch)
+  return (modJobs, precompileJobs, externJobs)
+
+/--
+Builds the workspace-local modules of list of imports.
+Used by `lake print-paths` to build modules for the Lean server.
+Returns the set of module dynlibs built (so they can be loaded by the server).
+
+Builds only module `.olean` and `.ilean` files if the package is configured
+as "Lean-only". Otherwise, also builds `.c` files.
+-/
+def buildImportsAndDeps (imports : List String) : BuildM (Array FilePath) := do
+  let ws ← getWorkspace
+  if imports.isEmpty then
+    -- build the package's (and its dependencies') `extraDepTarget`
+    ws.root.extraDep.build >>= (·.materialize)
+    return #[]
+  else
+    -- build local imports from list
+    let mods := ws.processImportList imports
+    let (modJobs, precompileJobs, externLibJobs) ←
+      recBuildImports mods |>.run.run
+    modJobs.forM (·.await)
+    let modLibs ← precompileJobs.mapM (·.await <&> (·.path))
+    let externLibs ← externLibJobs.mapM (·.await <&> (·.path))
+    -- NOTE: Lean wants the external library symbols before module symbols
+    return externLibs ++ modLibs

src/lake/Lake/Build/Index.lean

@@ -0,0 +1,108 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Build.Executable
+import Lake.Build.Topological
+
+/-!
+# The Lake Build Index
+
+The Lake build index is the complete map of Lake build keys to
+Lake build functions, which is used by Lake to build any Lake build info.
+
+This module leverages the index to perform topologically-based recursive builds.
+-/
+
+open Lean
+namespace Lake
+
+/--
+Converts a conveniently typed target facet build function into its
+dynamically typed equivalent.
+-/
+@[macro_inline] def mkTargetFacetBuild (facet : Name) (build : IndexBuildM α)
+[h : FamilyOut TargetData facet α] : IndexBuildM (TargetData facet) :=
+  cast (by rw [← h.family_key_eq_type]) build
+
+def ExternLib.recBuildStatic (lib : ExternLib) : IndexBuildM (BuildJob FilePath) := do
+  lib.config.getJob <$> fetch (lib.pkg.target lib.staticTargetName)
+
+def ExternLib.recBuildShared (lib : ExternLib) : IndexBuildM (BuildJob FilePath) := do
+  buildLeanSharedLibOfStatic (← lib.static.fetch) lib.linkArgs
+
+def ExternLib.recComputeDynlib (lib : ExternLib) : IndexBuildM (BuildJob Dynlib) := do
+  computeDynlibOfShared (← lib.shared.fetch)
+
+/-!
+## Topologically-based Recursive Build Using the Index
+-/
+
+/-- Recursive build function for anything in the Lake build index. -/
+def recBuildWithIndex : (info : BuildInfo) → IndexBuildM (BuildData info.key)
+| .moduleFacet mod facet => do
+  if let some config := (← getWorkspace).findModuleFacetConfig? facet then
+    config.build mod
+  else
+    error s!"do not know how to build module facet `{facet}`"
+| .packageFacet pkg facet => do
+  if let some config := (← getWorkspace).findPackageFacetConfig? facet then
+    config.build pkg
+  else
+    error s!"do not know how to build package facet `{facet}`"
+| .target pkg target =>
+  if let some config := pkg.findTargetConfig? target then
+    config.build pkg
+  else
+    error s!"could not build `{target}` of `{pkg.name}` -- target not found"
+| .libraryFacet lib facet => do
+  if let some config := (← getWorkspace).findLibraryFacetConfig? facet then
+    config.build lib
+  else
+    error s!"do not know how to build library facet `{facet}`"
+| .leanExe exe =>
+  mkTargetFacetBuild LeanExe.exeFacet exe.recBuildExe
+| .staticExternLib lib =>
+  mkTargetFacetBuild ExternLib.staticFacet lib.recBuildStatic
+| .sharedExternLib lib =>
+  mkTargetFacetBuild ExternLib.sharedFacet lib.recBuildShared
+| .dynlibExternLib lib =>
+  mkTargetFacetBuild ExternLib.dynlibFacet lib.recComputeDynlib
+
+/--
+Run the given recursive build using the Lake build index
+and a topological / suspending scheduler.
+-/
+def IndexBuildM.run (build : IndexBuildM α) : RecBuildM α :=
+  build <| recFetchMemoize BuildInfo.key recBuildWithIndex
+
+/--
+Recursively build the given info using the Lake build index
+and a topological / suspending scheduler.
+-/
+def buildIndexTop' (info : BuildInfo) : RecBuildM (BuildData info.key) :=
+  recFetchMemoize BuildInfo.key recBuildWithIndex info
+
+/--
+Recursively build the given info using the Lake build index
+and a topological / suspending scheduler and return the dynamic result.
+-/
+@[macro_inline] def buildIndexTop (info : BuildInfo)
+[FamilyOut BuildData info.key α] : RecBuildM α := do
+  cast (by simp) <| buildIndexTop' info
+
+/-- Build the given Lake target in a fresh build store. -/
+@[inline] def BuildInfo.build
+(self : BuildInfo) [FamilyOut BuildData self.key α] : BuildM α :=
+  buildIndexTop self |>.run
+
+export BuildInfo (build)
+
+/-! ### Lean Executable Builds -/
+
+@[inline] protected def LeanExe.build (self : LeanExe) : BuildM (BuildJob FilePath) :=
+  self.exe.build
+
+@[inline] protected def LeanExe.fetch (self : LeanExe) : IndexBuildM (BuildJob FilePath) :=
+  self.exe.fetch

src/lake/Lake/Build/Info.lean

@@ -0,0 +1,269 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Config.LeanExe
+import Lake.Config.ExternLib
+import Lake.Build.Facets
+import Lake.Util.EquipT
+
+/-!
+# Build Info
+
+This module defines the Lake build info type and related utilities.
+Build info is what is the data passed to a Lake build function to facilitate
+the build.
+-/
+
+namespace Lake
+
+/-- The type of Lake's build info. -/
+inductive BuildInfo
+| moduleFacet (module : Module) (facet : Name)
+| packageFacet (package : Package) (facet : Name)
+| libraryFacet (lib : LeanLib) (facet : Name)
+| leanExe (exe : LeanExe)
+| staticExternLib (lib : ExternLib)
+| sharedExternLib (lib : ExternLib)
+| dynlibExternLib (lib : ExternLib)
+| target (package : Package) (target : Name)
+
+--------------------------------------------------------------------------------
+/-! ## Build Info & Keys                                                      -/
+--------------------------------------------------------------------------------
+
+/-! ### Build Key Helper Constructors -/
+
+abbrev Module.facetBuildKey (facet : Name) (self : Module) : BuildKey :=
+  .moduleFacet self.keyName facet
+
+abbrev Package.facetBuildKey (facet : Name) (self : Package) : BuildKey :=
+  .packageFacet self.name facet
+
+abbrev Package.targetBuildKey (target : Name) (self : Package) : BuildKey :=
+  .customTarget self.name target
+
+abbrev LeanLib.facetBuildKey (self : LeanLib) (facet : Name) : BuildKey :=
+  .targetFacet self.pkg.name self.name (`leanLib ++ facet)
+
+abbrev LeanExe.buildKey (self : LeanExe) : BuildKey :=
+  .targetFacet self.pkg.name self.name exeFacet
+
+abbrev ExternLib.staticBuildKey (self : ExternLib) : BuildKey :=
+  .targetFacet self.pkg.name self.name staticFacet
+
+abbrev ExternLib.sharedBuildKey (self : ExternLib) : BuildKey :=
+  .targetFacet self.pkg.name self.name sharedFacet
+
+abbrev ExternLib.dynlibBuildKey (self : ExternLib) : BuildKey :=
+  .targetFacet self.pkg.name self.name dynlibFacet
+
+/-! ### Build Info to Key -/
+
+/-- The key that identifies the build in the Lake build store. -/
+abbrev BuildInfo.key : (self : BuildInfo) → BuildKey
+| moduleFacet m f => m.facetBuildKey f
+| packageFacet p f => p.facetBuildKey f
+| libraryFacet l f => l.facetBuildKey f
+| leanExe x => x.buildKey
+| staticExternLib l => l.staticBuildKey
+| sharedExternLib l => l.sharedBuildKey
+| dynlibExternLib l => l.dynlibBuildKey
+| target p t => p.targetBuildKey t
+
+/-! ### Instances for deducing data types of `BuildInfo` keys -/
+
+instance [FamilyOut ModuleData f α]
+: FamilyDef BuildData (BuildInfo.key (.moduleFacet m f)) α where
+  family_key_eq_type := by unfold BuildData; simp
+
+instance [FamilyOut PackageData f α]
+: FamilyDef BuildData (BuildInfo.key (.packageFacet p f)) α where
+  family_key_eq_type := by unfold BuildData; simp
+
+instance (priority := low) {p : NPackage n} : FamilyDef BuildData
+  (.customTarget p.toPackage.name t) (CustomData (n,t)) := ⟨by simp⟩
+
+instance {p : NPackage n} [FamilyOut CustomData (n, t) α]
+: FamilyDef BuildData (BuildInfo.key (.target p.toPackage t)) α where
+  family_key_eq_type := by unfold BuildData; simp
+
+instance [FamilyOut TargetData (`leanLib ++ f) α]
+: FamilyDef BuildData (BuildInfo.key (.libraryFacet l f)) α where
+  family_key_eq_type := by unfold BuildData; simp
+
+instance [FamilyOut TargetData LeanExe.exeFacet α]
+: FamilyDef BuildData (BuildInfo.key (.leanExe x)) α where
+  family_key_eq_type := by unfold BuildData; simp
+
+instance [FamilyOut TargetData ExternLib.staticFacet α]
+: FamilyDef BuildData (BuildInfo.key (.staticExternLib l)) α where
+  family_key_eq_type := by unfold BuildData; simp
+
+instance [FamilyOut TargetData ExternLib.sharedFacet α]
+: FamilyDef BuildData (BuildInfo.key (.sharedExternLib l)) α where
+  family_key_eq_type := by unfold BuildData; simp
+
+instance [FamilyOut TargetData ExternLib.dynlibFacet α]
+: FamilyDef BuildData (BuildInfo.key (.dynlibExternLib l)) α where
+  family_key_eq_type := by unfold BuildData; simp
+
+--------------------------------------------------------------------------------
+/-! ## Recursive Building                                                     -/
+--------------------------------------------------------------------------------
+
+/-- A build function for any element of the Lake build index. -/
+abbrev IndexBuildFn (m : Type → Type v) :=
+  -- `DBuildFn BuildInfo (BuildData ·.key) m` with less imports
+  (info : BuildInfo) → m (BuildData info.key)
+
+/-- A transformer to equip a monad with a build function for the Lake index. -/
+abbrev IndexT (m : Type → Type v) := EquipT (IndexBuildFn m) m
+
+/-- The monad for build functions that are part of the index. -/
+abbrev IndexBuildM := IndexT RecBuildM
+
+/-- Fetch the result associated with the info using the Lake build index. -/
+@[inline] def BuildInfo.fetch (self : BuildInfo) [FamilyOut BuildData self.key α] : IndexBuildM α :=
+  fun build => cast (by simp) <| build self
+
+export BuildInfo (fetch)
+
+--------------------------------------------------------------------------------
+/-! ## Build Info & Facets                                                    -/
+--------------------------------------------------------------------------------
+
+/-!
+### Complex Builtin Facet Declarations
+
+Additional builtin facets missing from `Build.Facets`.
+These are defined here because they need configuration definitions
+(e.g., `Module`), whereas the facets there are needed by the configuration
+definitions.
+-/
+
+/-- The direct local imports of the Lean module. -/
+abbrev Module.importsFacet := `lean.imports
+module_data lean.imports : Array Module
+
+/-- The transitive local imports of the Lean module. -/
+abbrev Module.transImportsFacet := `lean.transImports
+module_data lean.transImports : Array Module
+
+/-- The transitive local imports of the Lean module. -/
+abbrev Module.precompileImportsFacet := `lean.precompileImports
+module_data lean.precompileImports : Array Module
+
+/-- Shared library for `--load-dynlib`. -/
+abbrev Module.dynlibFacet := `dynlib
+module_data dynlib : BuildJob Dynlib
+
+/-- A Lean library's Lean modules. -/
+abbrev LeanLib.modulesFacet := `modules
+library_data modules : Array Module
+
+/-- The package's complete array of transitive dependencies. -/
+abbrev Package.depsFacet := `deps
+package_data deps : Array Package
+
+
+/-!
+### Facet Build Info Helper Constructors
+
+Definitions to easily construct `BuildInfo` values for module, package,
+and target facets.
+-/
+
+namespace Module
+
+/-- Build info for the module's specified facet. -/
+abbrev facet (facet : Name) (self : Module) : BuildInfo :=
+  .moduleFacet self facet
+
+@[inherit_doc importsFacet] abbrev imports (self : Module) :=
+  self.facet importsFacet
+
+@[inherit_doc transImportsFacet] abbrev transImports (self : Module) :=
+  self.facet transImportsFacet
+
+@[inherit_doc precompileImportsFacet] abbrev precompileImports (self : Module) :=
+  self.facet precompileImportsFacet
+
+@[inherit_doc depsFacet] abbrev deps  (self : Module) :=
+  self.facet depsFacet
+
+@[inherit_doc leanBinFacet] abbrev leanBin  (self : Module) :=
+  self.facet leanBinFacet
+
+@[inherit_doc importBinFacet] abbrev importBin (self : Module) :=
+  self.facet importBinFacet
+
+@[inherit_doc oleanFacet] abbrev olean (self : Module) :=
+  self.facet oleanFacet
+
+@[inherit_doc ileanFacet] abbrev ilean (self : Module)  :=
+  self.facet ileanFacet
+
+@[inherit_doc cFacet] abbrev c (self : Module) :=
+  self.facet cFacet
+
+@[inherit_doc oFacet] abbrev o (self : Module) :=
+  self.facet oFacet
+
+@[inherit_doc dynlibFacet] abbrev dynlib (self : Module) :=
+  self.facet dynlibFacet
+
+end Module
+
+/-- Build info for the package's specified facet. -/
+abbrev Package.facet (facet : Name) (self : Package) : BuildInfo :=
+  .packageFacet self facet
+
+@[inherit_doc releaseFacet]
+abbrev Package.release (self : Package) : BuildInfo :=
+  self.facet releaseFacet
+
+@[inherit_doc extraDepFacet]
+abbrev Package.extraDep (self : Package) : BuildInfo :=
+  self.facet extraDepFacet
+
+/-- Build info for a custom package target. -/
+abbrev Package.target (target : Name) (self : Package) : BuildInfo :=
+  .target self target
+
+/-- Build info of the Lean library's Lean binaries. -/
+abbrev LeanLib.facet (self : LeanLib) (facet : Name) : BuildInfo :=
+  .libraryFacet self facet
+
+@[inherit_doc modulesFacet]
+abbrev LeanLib.modules (self : LeanLib) : BuildInfo :=
+  self.facet modulesFacet
+
+@[inherit_doc leanFacet]
+abbrev LeanLib.lean (self : LeanLib) : BuildInfo :=
+  self.facet leanFacet
+
+@[inherit_doc staticFacet]
+abbrev LeanLib.static (self : LeanLib) : BuildInfo :=
+  self.facet staticFacet
+
+@[inherit_doc sharedFacet]
+abbrev LeanLib.shared (self : LeanLib) : BuildInfo :=
+  self.facet sharedFacet
+
+/-- Build info of the Lean executable. -/
+abbrev LeanExe.exe (self : LeanExe) : BuildInfo :=
+  .leanExe self
+
+/-- Build info of the external library's static binary. -/
+abbrev ExternLib.static (self : ExternLib) : BuildInfo :=
+  .staticExternLib self
+
+/-- Build info of the external library's shared binary. -/
+abbrev ExternLib.shared (self : ExternLib) : BuildInfo :=
+  .sharedExternLib self
+
+/-- Build info of the external library's dynlib. -/
+abbrev ExternLib.dynlib (self : ExternLib) : BuildInfo :=
+  .dynlibExternLib self

src/lake/Lake/Build/Job.lean

@@ -0,0 +1,112 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Util.Async
+import Lake.Build.Trace
+import Lake.Build.Context
+
+open System
+namespace Lake
+
+/-- A Lake job. -/
+abbrev Job α := OptionIOTask α
+
+/-- The monad of Lake jobs. -/
+abbrev JobM := BuildM
+
+/-- The monad of a finished Lake job. -/
+abbrev ResultM := OptionIO
+
+namespace Job
+
+@[inline] def nil : Job Unit :=
+ pure ()
+
+@[inline] protected def async (act : JobM α) : SchedulerM (Job α) :=
+  async act
+
+@[inline] protected def await (self : Job α) : ResultM α :=
+  await self
+
+@[inline] protected def bindSync
+(self : Job α) (f : α → JobM β) (prio := Task.Priority.default) : SchedulerM (Job β) :=
+  bindSync prio self f
+
+@[inline] protected def bindAsync
+(self : Job α) (f : α → SchedulerM (Job β)) : SchedulerM (Job β)  :=
+  bindAsync self f
+
+end Job
+
+/-- A Lake build job. -/
+abbrev BuildJob α := Job (α × BuildTrace)
+
+namespace BuildJob
+
+@[inline] def mk (job : Job (α × BuildTrace)) : BuildJob α :=
+  job
+
+@[inline] def ofJob (self : Job BuildTrace) : BuildJob Unit :=
+  mk <| ((), ·) <$> self
+
+@[inline] def toJob (self : BuildJob α) : Job (α × BuildTrace) :=
+  self
+
+@[inline] def nil : BuildJob Unit :=
+  mk <| pure ((), nilTrace)
+
+@[inline] protected def pure (a : α) : BuildJob α :=
+  mk <| pure (a, nilTrace)
+
+instance : Pure BuildJob := ⟨BuildJob.pure⟩
+
+@[inline] protected def map (f : α → β) (self : BuildJob α) : BuildJob β :=
+  mk <| (fun (a,t) => (f a,t)) <$> self.toJob
+
+instance : Functor BuildJob where
+  map := BuildJob.map
+
+@[inline] def mapWithTrace (f : α → BuildTrace → β × BuildTrace) (self : BuildJob α) : BuildJob β :=
+  mk <| (fun (a,t) => f a t) <$> self.toJob
+
+@[inline] protected def bindSync
+(self : BuildJob α) (f : α → BuildTrace → JobM β)
+(prio : Task.Priority := .default) : SchedulerM (Job β) :=
+  self.toJob.bindSync (prio := prio) fun (a, t) => f a t
+
+@[inline] protected def bindAsync
+(self : BuildJob α) (f : α → BuildTrace → SchedulerM (Job β)) : SchedulerM (Job β)  :=
+  self.toJob.bindAsync fun (a, t) => f a t
+
+@[inline] protected def await (self : BuildJob α) : ResultM α :=
+  (·.1) <$> await self.toJob
+
+instance : Await BuildJob ResultM := ⟨BuildJob.await⟩
+
+@[inline] def materialize (self : BuildJob α) : ResultM Unit :=
+  discard <| await self.toJob
+
+def mix (t1 : BuildJob α) (t2 : BuildJob β) : BaseIO (BuildJob Unit) :=
+  mk <$> seqWithAsync (fun (_,t) (_,t') => ((), mixTrace t t')) t1.toJob t2.toJob
+
+def mixList (jobs : List (BuildJob α)) : BaseIO (BuildJob Unit) := ofJob <$> do
+  jobs.foldrM (init := pure nilTrace) fun j a =>
+    seqWithAsync (fun (_,t') t => mixTrace t t') j.toJob a
+
+def mixArray (jobs : Array (BuildJob α)) : BaseIO (BuildJob Unit) := ofJob <$> do
+  jobs.foldlM (init := pure nilTrace) fun a j =>
+    seqWithAsync (fun t (_,t') => mixTrace t t') a j.toJob
+
+protected def seqWithAsync
+(f : α → β → γ) (t1 : BuildJob α) (t2 : BuildJob β) : BaseIO (BuildJob γ) :=
+  mk <$> seqWithAsync (fun (a,t) (b,t') => (f a b, mixTrace t t')) t1.toJob t2.toJob
+
+instance : SeqWithAsync BaseIO BuildJob := ⟨BuildJob.seqWithAsync⟩
+
+def collectList (jobs : List (BuildJob α)) : BaseIO (BuildJob (List α)) :=
+  jobs.foldrM (seqWithAsync List.cons) (pure [])
+
+def collectArray (jobs : Array (BuildJob α)) : BaseIO (BuildJob (Array α)) :=
+  jobs.foldlM (seqWithAsync Array.push) (pure #[])

src/lake/Lake/Build/Key.lean

@@ -0,0 +1,104 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Util.Name
+
+namespace Lake
+
+/-- The type of keys in the Lake build store. -/
+inductive BuildKey
+| moduleFacet (module : Name) (facet : Name)
+| packageFacet (package : Name) (facet : Name)
+| targetFacet (package : Name) (target : Name) (facet : Name)
+| customTarget (package : Name) (target : Name)
+deriving Inhabited, Repr, DecidableEq, Hashable
+
+namespace BuildKey
+
+def toString : (self : BuildKey) → String
+| moduleFacet m f => s!"+{m}:{f}"
+| packageFacet p f => s!"@{p}:{f}"
+| targetFacet p t f => s!"{p}/{t}:{f}"
+| customTarget p t => s!"{p}/{t}"
+
+instance : ToString BuildKey := ⟨(·.toString)⟩
+
+def quickCmp (k k' : BuildKey) : Ordering :=
+  match k with
+  | moduleFacet m f =>
+    match k' with
+    | moduleFacet m' f' =>
+      match m.quickCmp m' with
+      | .eq => f.quickCmp f'
+      | ord => ord
+    | _ => .lt
+  | packageFacet p f =>
+    match k' with
+    | moduleFacet .. => .gt
+    | packageFacet p' f' =>
+      match p.quickCmp p' with
+      | .eq => f.quickCmp f'
+      | ord => ord
+    | _ => .lt
+  | targetFacet p t f =>
+    match k' with
+    | customTarget .. => .lt
+    | targetFacet p' t' f' =>
+      match p.quickCmp p' with
+      | .eq =>
+        match t.quickCmp t' with
+        | .eq => f.quickCmp f'
+        | ord => ord
+      | ord => ord
+    | _=> .gt
+  | customTarget p t =>
+    match k' with
+    | customTarget p' t' =>
+      match p.quickCmp p' with
+      | .eq => t.quickCmp t'
+      | ord => ord
+    | _ => .gt
+
+theorem eq_of_quickCmp {k k' : BuildKey}  :
+quickCmp k k' = Ordering.eq → k = k' := by
+  unfold quickCmp
+  cases k with
+  | moduleFacet m f =>
+    cases k'
+    case moduleFacet m' f' =>
+      dsimp only; split
+      next m_eq => intro f_eq; rw [eq_of_cmp m_eq, eq_of_cmp f_eq]
+      next => intro; contradiction
+    all_goals (intro; contradiction)
+  | packageFacet p f =>
+    cases k'
+    case packageFacet p' f' =>
+      dsimp only; split
+      next p_eq => intro f_eq; rw [eq_of_cmp p_eq, eq_of_cmp f_eq]
+      next => intro; contradiction
+    all_goals (intro; contradiction)
+  | targetFacet p t f =>
+    cases k'
+    case targetFacet p' t' f' =>
+      dsimp only; split
+      next p_eq =>
+        split
+        next t_eq =>
+          intro f_eq
+          rw [eq_of_cmp p_eq, eq_of_cmp t_eq, eq_of_cmp f_eq]
+        next => intro; contradiction
+      next => intro; contradiction
+    all_goals (intro; contradiction)
+  | customTarget p t =>
+    cases k'
+    case customTarget p' t' =>
+      dsimp only; split
+      next p_eq => intro t_eq; rw [eq_of_cmp p_eq, eq_of_cmp t_eq]
+      next => intro; contradiction
+    all_goals (intro; contradiction)
+
+instance : LawfulCmpEq BuildKey quickCmp where
+  eq_of_cmp := eq_of_quickCmp
+  cmp_rfl {k} := by cases k <;> simp [quickCmp]

src/lake/Lake/Build/Library.lean

@@ -0,0 +1,111 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Build.Common
+
+namespace Lake
+
+/-- Get the Lean library in the workspace with the configuration's name. -/
+@[inline] def LeanLibConfig.get (self : LeanLibConfig)
+[Monad m] [MonadError m] [MonadLake m] : m LeanLib := do
+  let some lib ← findLeanLib? self.name
+    | error "Lean library '{self.name}' does not exist in the workspace"
+  return lib
+
+/-- Fetch the build result of a library facet. -/
+@[inline] protected def LibraryFacetDecl.fetch (lib : LeanLib)
+(self : LibraryFacetDecl) [FamilyOut LibraryData self.name α] : IndexBuildM α := do
+  fetch <| lib.facet self.name
+
+/-- Fetch the build job of a library facet. -/
+def LibraryFacetConfig.fetchJob (lib : LeanLib)
+(self : LibraryFacetConfig name) : IndexBuildM (BuildJob Unit) :=  do
+  let some getJob := self.getJob?
+    | error "library facet '{self.name}' has no associated build job"
+  return getJob <| ← fetch <| lib.facet self.name
+
+/-- Fetch the build job of a library facet. -/
+def LeanLib.fetchFacetJob
+(name : Name) (self : LeanLib) : IndexBuildM (BuildJob Unit) :=  do
+  let some config := (← getWorkspace).libraryFacetConfigs.find? name
+    | error "library facet '{name}' does not exist in workspace"
+  inline <| config.fetchJob self
+
+/-! # Build Lean & Static Lib -/
+
+/--
+Collect the local modules of a library.
+That is, the modules from `getModuleArray` plus their local transitive imports.
+-/
+partial def LeanLib.recCollectLocalModules (self : LeanLib) : IndexBuildM (Array Module) := do
+  let mut mods := #[]
+  let mut modSet := ModuleSet.empty
+  for mod in (← self.getModuleArray) do
+    (mods, modSet) ← go mod mods modSet
+  return mods
+where
+  go root mods modSet := do
+    let mut mods := mods
+    let mut modSet := modSet
+    unless modSet.contains root do
+      modSet := modSet.insert root
+      let imps ← root.imports.fetch
+      for mod in imps do
+        if self.isLocalModule mod.name then
+          (mods, modSet) ← go mod mods modSet
+      mods := mods.push root
+    return (mods, modSet)
+
+/-- The `LibraryFacetConfig` for the builtin `modulesFacet`. -/
+def LeanLib.modulesFacetConfig : LibraryFacetConfig modulesFacet :=
+  mkFacetConfig LeanLib.recCollectLocalModules
+
+protected def LeanLib.recBuildLean
+(self : LeanLib) : IndexBuildM (BuildJob Unit) := do
+  let mods ← self.modules.fetch
+  mods.foldlM (init := BuildJob.nil) fun job mod => do
+    job.mix <| ← mod.leanBin.fetch
+
+/-- The `LibraryFacetConfig` for the builtin `leanFacet`. -/
+def LeanLib.leanFacetConfig : LibraryFacetConfig leanFacet :=
+  mkFacetJobConfigSmall LeanLib.recBuildLean
+
+protected def LeanLib.recBuildStatic
+(self : LeanLib) : IndexBuildM (BuildJob FilePath) := do
+  let mods ← self.modules.fetch
+  let oJobs ← mods.concatMapM fun mod =>
+    mod.nativeFacets.mapM fun facet => fetch <| mod.facet facet.name
+  buildStaticLib self.staticLibFile oJobs
+
+/-- The `LibraryFacetConfig` for the builtin `staticFacet`. -/
+def LeanLib.staticFacetConfig : LibraryFacetConfig staticFacet :=
+  mkFacetJobConfig LeanLib.recBuildStatic
+
+/-! # Build Shared Lib -/
+
+protected def LeanLib.recBuildShared
+(self : LeanLib) : IndexBuildM (BuildJob FilePath) := do
+  let mods ← self.modules.fetch
+  let oJobs ← mods.concatMapM fun mod =>
+    mod.nativeFacets.mapM fun facet => fetch <| mod.facet facet.name
+  let pkgs := mods.foldl (·.insert ·.pkg) OrdPackageSet.empty |>.toArray
+  let externJobs ← pkgs.concatMapM (·.externLibs.mapM (·.shared.fetch))
+  buildLeanSharedLib self.sharedLibFile (oJobs ++ externJobs) self.linkArgs
+
+/-- The `LibraryFacetConfig` for the builtin `sharedFacet`. -/
+def LeanLib.sharedFacetConfig : LibraryFacetConfig sharedFacet :=
+  mkFacetJobConfig LeanLib.recBuildShared
+
+open LeanLib in
+/--
+A library facet name to build function map that contains builders for
+the initial set of Lake library facets (e.g., `lean`, `static`, and `shared`).
+-/
+def initLibraryFacetConfigs : DNameMap LibraryFacetConfig :=
+  DNameMap.empty
+  |>.insert modulesFacet modulesFacetConfig
+  |>.insert leanFacet leanFacetConfig
+  |>.insert staticFacet staticFacetConfig
+  |>.insert sharedFacet sharedFacetConfig

src/lake/Lake/Build/Module.lean

@@ -0,0 +1,255 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Ullrich, Mac Malone
+-/
+import Lake.Util.OrdHashSet
+import Lean.Elab.ParseImportsFast
+import Lake.Build.Common
+
+open System
+
+namespace Lake
+
+/-- Fetch the build result of a module facet. -/
+@[inline] protected def ModuleFacetDecl.fetch (mod : Module)
+(self : ModuleFacetDecl) [FamilyOut ModuleData self.name α] : IndexBuildM α := do
+  fetch <| mod.facet self.name
+
+/-- Fetch the build job of a module facet. -/
+def ModuleFacetConfig.fetchJob (mod : Module)
+(self : ModuleFacetConfig name) : IndexBuildM (BuildJob Unit) :=  do
+  let some getJob := self.getJob?
+    | error "module facet '{self.name}' has no associated build job"
+  return getJob <| ← fetch <| mod.facet self.name
+
+/-- Fetch the build job of a module facet. -/
+def Module.fetchFacetJob
+(name : Name) (self : Module) : IndexBuildM (BuildJob Unit) :=  do
+  let some config := (← getWorkspace).moduleFacetConfigs.find? name
+    | error "library facet '{name}' does not exist in workspace"
+  inline <| config.fetchJob self
+
+def Module.buildUnlessUpToDate (mod : Module)
+(dynlibPath : SearchPath) (dynlibs : Array FilePath)
+(depTrace : BuildTrace) : BuildM PUnit := do
+  let isOldMode ← getIsOldMode
+  let argTrace : BuildTrace := pureHash mod.leanArgs
+  let srcTrace : BuildTrace ← computeTrace { path := mod.leanFile : TextFilePath }
+  let modTrace := (← getLeanTrace).mix <| argTrace.mix <| srcTrace.mix depTrace
+  let modUpToDate ← do
+    if isOldMode then
+      srcTrace.checkAgainstTime mod
+    else
+      modTrace.checkAgainstFile mod mod.traceFile
+  let name := mod.name.toString
+  unless modUpToDate do
+    compileLeanModule name mod.leanFile mod.oleanFile mod.ileanFile mod.cFile
+      (← getLeanPath) mod.rootDir dynlibs dynlibPath (mod.leanArgs ++ mod.weakLeanArgs) (← getLean)
+  unless isOldMode do
+    modTrace.writeToFile mod.traceFile
+
+/-- Compute library directories and build external library Jobs of the given packages. -/
+def recBuildExternDynlibs (pkgs : Array Package)
+: IndexBuildM (Array (BuildJob Dynlib) × Array FilePath) := do
+  let mut libDirs := #[]
+  let mut jobs : Array (BuildJob Dynlib) := #[]
+  for pkg in pkgs do
+    libDirs := libDirs.push pkg.nativeLibDir
+    jobs := jobs.append <| ← pkg.externLibs.mapM (·.dynlib.fetch)
+  return (jobs, libDirs)
+
+/--
+Build the dynlibs of the transitive imports that want precompilation
+and the dynlibs of *their* imports.
+-/
+partial def recBuildPrecompileDynlibs (imports : Array Module)
+: IndexBuildM (Array (BuildJob Dynlib) × Array (BuildJob Dynlib) × Array FilePath) := do
+  let (pkgs, _, jobs) ←
+    go imports OrdPackageSet.empty ModuleSet.empty #[] false
+  return (jobs, ← recBuildExternDynlibs pkgs.toArray)
+where
+  go imports pkgs modSet jobs shouldPrecompile := do
+    let mut pkgs := pkgs
+    let mut modSet := modSet
+    let mut jobs := jobs
+    for mod in imports do
+      if modSet.contains mod then
+        continue
+      modSet := modSet.insert mod
+      let shouldPrecompile := shouldPrecompile || mod.shouldPrecompile
+      if shouldPrecompile then
+        pkgs := pkgs.insert mod.pkg
+        jobs := jobs.push <| (←  mod.dynlib.fetch)
+      let recImports ← mod.imports.fetch
+      (pkgs, modSet, jobs) ← go recImports pkgs modSet jobs shouldPrecompile
+    return (pkgs, modSet, jobs)
+
+variable [MonadLiftT BuildM m]
+
+/--
+Recursively parse the Lean files of a module and its imports
+building an `Array` product of its direct local imports.
+-/
+def Module.recParseImports (mod : Module) : IndexBuildM (Array Module) := do
+  let contents ← IO.FS.readFile mod.leanFile
+  let imports ← Lean.parseImports' contents mod.leanFile.toString
+  let mods ← imports.foldlM (init := OrdModuleSet.empty) fun set imp =>
+    findModule? imp.module <&> fun | some mod => set.insert mod | none => set
+  return mods.toArray
+
+/-- The `ModuleFacetConfig` for the builtin `importsFacet`. -/
+def Module.importsFacetConfig : ModuleFacetConfig importsFacet :=
+  mkFacetConfig (·.recParseImports)
+
+/-- Recursively compute a module's transitive imports. -/
+def Module.recComputeTransImports (mod : Module) : IndexBuildM (Array Module) := do
+  (·.toArray) <$> (← mod.imports.fetch).foldlM (init := OrdModuleSet.empty) fun set imp => do
+    return set.appendArray (← imp.transImports.fetch) |>.insert imp
+
+/-- The `ModuleFacetConfig` for the builtin `transImportsFacet`. -/
+def Module.transImportsFacetConfig : ModuleFacetConfig transImportsFacet :=
+  mkFacetConfig (·.recComputeTransImports)
+
+/-- Recursively compute a module's precompiled imports. -/
+def Module.recComputePrecompileImports (mod : Module) : IndexBuildM (Array Module) := do
+  (·.toArray) <$> (← mod.imports.fetch).foldlM (init := OrdModuleSet.empty) fun set imp => do
+    if imp.shouldPrecompile then
+      return set.appendArray (← imp.transImports.fetch) |>.insert imp
+    else
+      return set.appendArray (← imp.precompileImports.fetch)
+
+/-- The `ModuleFacetConfig` for the builtin `precompileImportsFacet`. -/
+def Module.precompileImportsFacetConfig : ModuleFacetConfig precompileImportsFacet :=
+  mkFacetConfig (·.recComputePrecompileImports)
+
+/-- Recursively build a module's transitive local imports and shared library dependencies. -/
+def Module.recBuildDeps (mod : Module) : IndexBuildM (BuildJob (SearchPath × Array FilePath)) := do
+  let imports ← mod.imports.fetch
+  let extraDepJob ← mod.pkg.extraDep.fetch
+  let precompileImports ← mod.precompileImports.fetch
+  let modJobs ← precompileImports.mapM (·.dynlib.fetch)
+  let pkgs := precompileImports.foldl (·.insert ·.pkg)
+    OrdPackageSet.empty |>.insert mod.pkg |>.toArray
+  let (externJobs, libDirs) ← recBuildExternDynlibs pkgs
+  let importJob ← BuildJob.mixArray <| ← imports.mapM (·.importBin.fetch)
+  let externDynlibsJob ← BuildJob.collectArray externJobs
+  let modDynlibsJob ← BuildJob.collectArray modJobs
+
+  extraDepJob.bindAsync fun _ _ => do
+  importJob.bindAsync fun _ importTrace => do
+  modDynlibsJob.bindAsync fun modDynlibs modTrace => do
+  return externDynlibsJob.mapWithTrace fun externDynlibs externTrace =>
+    let depTrace := importTrace.mix <| modTrace.mix externTrace
+    /-
+    Requirements:
+    * Lean wants the external library symbols before module symbols.
+    * Unix requires the file extension of the dynlib.
+    * For some reason, building from the Lean server requires full paths.
+      Everything else loads fine with just the augmented library path.
+    * Linux still needs the augmented path to resolve nested dependencies in dynlibs.
+    -/
+    let dynlibPath := libDirs ++ externDynlibs.filterMap (·.dir?) |>.toList
+    let dynlibs := externDynlibs.map (·.path) ++ modDynlibs.map (·.path)
+    ((dynlibPath, dynlibs), depTrace)
+
+/-- The `ModuleFacetConfig` for the builtin `depsFacet`. -/
+def Module.depsFacetConfig : ModuleFacetConfig depsFacet :=
+  mkFacetJobConfigSmall (·.recBuildDeps)
+
+/-- Recursively build a module and its dependencies. -/
+def Module.recBuildLeanCore (mod : Module) : IndexBuildM (BuildJob Unit) := do
+  (← mod.deps.fetch).bindSync fun (dynlibPath, dynlibs) depTrace => do
+    mod.buildUnlessUpToDate dynlibPath dynlibs depTrace
+    return ((), depTrace)
+
+/-- The `ModuleFacetConfig` for the builtin `leanBinFacet`. -/
+def Module.leanBinFacetConfig : ModuleFacetConfig leanBinFacet :=
+  mkFacetJobConfig (·.recBuildLeanCore)
+
+/-- The `ModuleFacetConfig` for the builtin `importBinFacet`. -/
+def Module.importBinFacetConfig : ModuleFacetConfig importBinFacet :=
+  mkFacetJobConfigSmall fun mod => do
+    (← mod.leanBin.fetch).bindSync fun _ depTrace =>
+      return ((), mixTrace (← computeTrace mod) depTrace)
+
+/-- The `ModuleFacetConfig` for the builtin `oleanFacet`. -/
+def Module.oleanFacetConfig : ModuleFacetConfig oleanFacet :=
+  mkFacetJobConfigSmall fun mod => do
+    (← mod.leanBin.fetch).bindSync fun _ depTrace =>
+      return (mod.oleanFile, mixTrace (← computeTrace mod.oleanFile) depTrace)
+
+/-- The `ModuleFacetConfig` for the builtin `ileanFacet`. -/
+def Module.ileanFacetConfig : ModuleFacetConfig ileanFacet :=
+  mkFacetJobConfigSmall fun mod => do
+    (← mod.leanBin.fetch).bindSync fun _ depTrace =>
+      return (mod.ileanFile, mixTrace (← computeTrace mod.ileanFile) depTrace)
+
+/-- The `ModuleFacetConfig` for the builtin `cFacet`. -/
+def Module.cFacetConfig : ModuleFacetConfig cFacet :=
+  mkFacetJobConfigSmall fun mod => do
+    (← mod.leanBin.fetch).bindSync fun _ _ =>
+      -- do content-aware hashing so that we avoid recompiling unchanged C files
+      return (mod.cFile, ← computeTrace mod.cFile)
+
+/-- Recursively build the module's object file from its C file produced by `lean`. -/
+def Module.recBuildLeanO (self : Module) : IndexBuildM (BuildJob FilePath) := do
+  buildLeanO self.name.toString self.oFile (← self.c.fetch) self.leancArgs
+
+/-- The `ModuleFacetConfig` for the builtin `oFacet`. -/
+def Module.oFacetConfig : ModuleFacetConfig oFacet :=
+  mkFacetJobConfig Module.recBuildLeanO
+
+-- TODO: Return `BuildJob OrdModuleSet × OrdPackageSet` or `OrdRBSet Dynlib`
+/-- Recursively build the shared library of a module (e.g., for `--load-dynlib`). -/
+def Module.recBuildDynlib (mod : Module) : IndexBuildM (BuildJob Dynlib) := do
+
+  -- Compute dependencies
+  let transImports ← mod.transImports.fetch
+  let modJobs ← transImports.mapM (·.dynlib.fetch)
+  let pkgs := transImports.foldl (·.insert ·.pkg)
+    OrdPackageSet.empty |>.insert mod.pkg |>.toArray
+  let (externJobs, pkgLibDirs) ← recBuildExternDynlibs pkgs
+  let linkJobs ← mod.nativeFacets.mapM (fetch <| mod.facet ·.name)
+
+  -- Collect Jobs
+  let linksJob ← BuildJob.collectArray linkJobs
+  let modDynlibsJob ← BuildJob.collectArray modJobs
+  let externDynlibsJob ← BuildJob.collectArray externJobs
+
+  -- Build dynlib
+  show SchedulerM _ from do
+    linksJob.bindAsync fun links oTrace => do
+    modDynlibsJob.bindAsync fun modDynlibs libTrace => do
+    externDynlibsJob.bindSync fun externDynlibs externTrace => do
+      let libNames := modDynlibs.map (·.name) ++ externDynlibs.map (·.name)
+      let libDirs := pkgLibDirs ++ externDynlibs.filterMap (·.dir?)
+      let depTrace := oTrace.mix <| libTrace.mix externTrace
+      let trace ← buildFileUnlessUpToDate mod.dynlibFile depTrace do
+        let args := links.map toString ++
+          libDirs.map (s!"-L{·}") ++ libNames.map (s!"-l{·}")
+        compileSharedLib mod.name.toString mod.dynlibFile args (← getLeanc)
+      return (⟨mod.dynlibFile, mod.dynlibName⟩, trace)
+
+/-- The `ModuleFacetConfig` for the builtin `dynlibFacet`. -/
+def Module.dynlibFacetConfig : ModuleFacetConfig dynlibFacet :=
+  mkFacetJobConfig Module.recBuildDynlib
+
+open Module in
+/--
+A name-configuration map for the initial set of
+Lake module facets (e.g., `lean.{imports, c, o, dynlib]`).
+-/
+def initModuleFacetConfigs : DNameMap ModuleFacetConfig :=
+  DNameMap.empty
+  |>.insert importsFacet importsFacetConfig
+  |>.insert transImportsFacet transImportsFacetConfig
+  |>.insert precompileImportsFacet precompileImportsFacetConfig
+  |>.insert depsFacet depsFacetConfig
+  |>.insert leanBinFacet leanBinFacetConfig
+  |>.insert importBinFacet importBinFacetConfig
+  |>.insert oleanFacet oleanFacetConfig
+  |>.insert ileanFacet ileanFacetConfig
+  |>.insert cFacet cFacetConfig
+  |>.insert oFacet oFacetConfig
+  |>.insert dynlibFacet dynlibFacetConfig

src/lake/Lake/Build/Monad.lean

@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Config.Monad
+import Lake.Build.Context
+import Lake.Util.EStateT
+
+open System
+
+namespace Lake
+
+def mkBuildContext (ws : Workspace) (oldMode : Bool) : IO BuildContext := do
+  let lean := ws.lakeEnv.lean
+  let leanTrace := Hash.ofString lean.githash
+  return {
+    opaqueWs := ws, leanTrace, oldMode
+    startedBuilds := ← IO.mkRef 0
+    finishedBuilds := ← IO.mkRef 0
+  }
+
+@[inline] def getLeanTrace : BuildM BuildTrace :=
+  (·.leanTrace) <$> readThe BuildContext
+
+@[inline] def getIsOldMode : BuildM Bool :=
+  (·.oldMode) <$> readThe BuildContext
+
+def failOnBuildCycle [ToString k] : Except (List k) α → BuildM α
+| Except.ok a => pure a
+| Except.error cycle => do
+  let cycle := cycle.map (s!"  {·}")
+  error s!"build cycle detected:\n{"\n".intercalate cycle}"
+
+/--
+Run the recursive build in the given build store.
+If a cycle is encountered, log it and then fail.
+-/
+@[inline] def RecBuildM.runIn (store : BuildStore) (build : RecBuildM α) : BuildM (α × BuildStore) := do
+  let (res, store) ← EStateT.run store <| ReaderT.run build []
+  return (← failOnBuildCycle res, store)
+
+/--
+Run the recursive build in a fresh build store.
+If a cycle is encountered, log it and then fail.
+-/
+@[inline] def RecBuildM.run (build : RecBuildM α) : BuildM α := do
+  (·.1) <$> build.runIn {}
+
+/-- Run the given build function in the Workspace's context. -/
+@[inline] def Workspace.runBuild (ws : Workspace) (build : BuildM α) (oldMode := false) : LogIO α := do
+  let ctx ← mkBuildContext ws oldMode
+  build.run ctx
+
+/-- Run the given build function in the Lake monad's workspace. -/
+@[inline] def runBuild (build : BuildM α) (oldMode := false) : LakeT LogIO α := do
+  (← getWorkspace).runBuild build oldMode

src/lake/Lake/Build/Package.lean

@@ -0,0 +1,122 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Util.Sugar
+import Lake.Build.Common
+
+open System
+namespace Lake
+
+/-- Fetch the build job of the specified package target. -/
+def Package.fetchTargetJob (self : Package)
+(target : Name) : IndexBuildM (Option (BuildJob Unit)) :=  do
+  let some config := self.findTargetConfig? target
+    | error s!"package '{self.name}' has no target '{target}'"
+  return config.getJob (← fetch <| self.target target)
+
+/-- Fetch the build result of a target. -/
+protected def TargetDecl.fetch (self : TargetDecl)
+[FamilyDef CustomData (self.pkg, self.name) α] : IndexBuildM α := do
+  let some pkg ← findPackage? self.pkg
+    | error s!"package '{self.pkg}' of target '{self.name}' does not exist in workspace"
+  fetch <| pkg.target self.name
+
+/-- Fetch the build job of the target. -/
+def TargetDecl.fetchJob (self : TargetDecl) : IndexBuildM (BuildJob Unit) :=  do
+  let some pkg ← findPackage? self.pkg
+    | error s!"package '{self.pkg}' of target '{self.name}' does not exist in workspace"
+  return self.config.getJob (← fetch <| pkg.target self.name)
+
+/-- Fetch the build result of a package facet. -/
+@[inline] protected def PackageFacetDecl.fetch (pkg : Package)
+(self : PackageFacetDecl) [FamilyOut PackageData self.name α] : IndexBuildM α := do
+  fetch <| pkg.facet self.name
+
+/-- Fetch the build job of a package facet. -/
+def PackageFacetConfig.fetchJob (pkg : Package)
+(self : PackageFacetConfig name) : IndexBuildM (BuildJob Unit) :=  do
+  let some getJob := self.getJob?
+    | error "package facet '{pkg.name}' has no associated build job"
+  return getJob <| ← fetch <| pkg.facet self.name
+
+/-- Fetch the build job of a library facet. -/
+def Package.fetchFacetJob
+(name : Name) (self : Package) : IndexBuildM (BuildJob Unit) :=  do
+  let some config := (← getWorkspace).packageFacetConfigs.find? name
+    | error "package facet '{name}' does not exist in workspace"
+  inline <| config.fetchJob self
+
+/-- Compute a topological ordering of the package's transitive dependencies. -/
+def Package.recComputeDeps (self : Package) : IndexBuildM (Array Package) := do
+  let mut deps := #[]
+  let mut depSet := PackageSet.empty
+  for dep in self.deps do
+    for depDep in (← fetch <| dep.facet `deps) do
+      unless depSet.contains depDep do
+        deps := deps.push depDep
+        depSet := depSet.insert depDep
+    unless depSet.contains dep do
+      deps := deps.push dep
+      depSet := depSet.insert dep
+  return deps
+
+/-- The `PackageFacetConfig` for the builtin `depsFacet`. -/
+def Package.depsFacetConfig : PackageFacetConfig depsFacet :=
+  mkFacetConfig Package.recComputeDeps
+
+/--
+Build the `extraDepTarget` for the package and its transitive dependencies.
+Also fetch pre-built releases for the package's' dependencies.
+-/
+def Package.recBuildExtraDepTargets (self : Package) : IndexBuildM (BuildJob Unit) := do
+  let mut job := BuildJob.nil
+  -- Build dependencies' extra dep targets
+  for dep in self.deps do
+    job ← job.mix <| ← dep.extraDep.fetch
+  -- Fetch pre-built release if desired and this package is a dependency
+  if self.name ≠ (← getWorkspace).root.name ∧ self.preferReleaseBuild then
+    job ← job.mix <| ← self.release.fetch
+  -- Build this package's extra dep targets
+  for target in self.extraDepTargets do
+    if let some config := self.findTargetConfig? target then
+      job ← job.mix <| config.getJob <| ← fetch <| self.target target
+    else
+      error s!"unknown target `{target}`"
+  return job
+
+/-- The `PackageFacetConfig` for the builtin `dynlibFacet`. -/
+def Package.extraDepFacetConfig : PackageFacetConfig extraDepFacet :=
+  mkFacetJobConfigSmall Package.recBuildExtraDepTargets
+
+/-- Download and unpack the package's prebuilt release archive (from GitHub). -/
+def Package.fetchRelease (self : Package) : SchedulerM (BuildJob Unit) := Job.async do
+  let some (repoUrl, tag) := self.release? | do
+    logWarning "wanted prebuilt release, but release repository and tag was not known"
+    return ((), .nil)
+  let url := s!"{repoUrl}/releases/download/{tag}/{self.buildArchive}"
+  let logName := s!"{self.name}/{tag}/{self.buildArchive}"
+  try
+    let depTrace := Hash.ofString url
+    let trace ← buildFileUnlessUpToDate self.buildArchiveFile depTrace do
+      download logName url self.buildArchiveFile
+      untar logName self.buildArchiveFile self.buildDir
+    return ((), trace)
+  else
+    return ((), .nil)
+
+/-- The `PackageFacetConfig` for the builtin `releaseFacet`. -/
+def Package.releaseFacetConfig : PackageFacetConfig releaseFacet :=
+  mkFacetJobConfig (·.fetchRelease)
+
+open Package in
+/--
+A package facet name to build function map that contains builders for
+the initial set of Lake package facets (e.g., `extraDep`).
+-/
+def initPackageFacetConfigs : DNameMap PackageFacetConfig :=
+  DNameMap.empty
+  |>.insert depsFacet depsFacetConfig
+  |>.insert extraDepFacet extraDepFacetConfig
+  |>.insert releaseFacet releaseFacetConfig

src/lake/Lake/Build/Store.lean

@@ -0,0 +1,88 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Build.Data
+import Lake.Util.StoreInsts
+
+/-!
+# The Lake Build Store
+
+The Lake build store is the map of Lake build keys to build task and/or
+build results that is slowly filled during a recursive build (e.g., via
+topological-based build of an initial key's dependencies).
+-/
+
+namespace Lake
+
+/-- A monad equipped with a Lake build store. -/
+abbrev MonadBuildStore (m) := MonadDStore BuildKey BuildData m
+
+/-- The type of the Lake build store. -/
+abbrev BuildStore :=
+  DRBMap BuildKey BuildData BuildKey.quickCmp
+
+@[inline] def BuildStore.empty : BuildStore := DRBMap.empty
+
+namespace BuildStore
+
+-- Linter reports false positives on the `v` variables below
+set_option linter.unusedVariables false
+
+/-- Derive an array of built module facets from the store. -/
+def collectModuleFacetArray (self : BuildStore)
+(facet : Name) [FamilyOut ModuleData facet α] : Array α := Id.run do
+  let mut res : Array α := #[]
+  for ⟨k, v⟩ in self do
+    match k with
+    | .moduleFacet m f =>
+      if h : f = facet then
+        have of_data := by unfold BuildData; simp [h]
+        res := res.push <| cast of_data v
+    | _ => pure ()
+  return res
+
+/-- Derive a map of module names to built facets from the store. -/
+def collectModuleFacetMap (self : BuildStore)
+(facet : Name) [FamilyOut ModuleData facet α] : NameMap α := Id.run do
+  let mut res := Lean.mkNameMap α
+  for ⟨k, v⟩ in self do
+    match k with
+    | .moduleFacet m f =>
+      if h : f = facet then
+        have of_data := by unfold BuildData; simp [h]
+        res := res.insert m <| cast of_data v
+    | _ => pure ()
+  return res
+
+/-- Derive an array of built package facets from the store. -/
+def collectPackageFacetArray (self : BuildStore)
+(facet : Name) [FamilyOut PackageData facet α] : Array α := Id.run do
+  let mut res : Array α := #[]
+  for ⟨k, v⟩ in self do
+    match k with
+    | .packageFacet _ f =>
+      if h : f = facet then
+        have of_data := by unfold BuildData; simp [h]
+        res := res.push <| cast of_data v
+    | _ => pure ()
+  return res
+
+/-- Derive an array of built target facets from the store. -/
+def collectTargetFacetArray (self : BuildStore)
+(facet : Name) [FamilyOut TargetData facet α] : Array α := Id.run do
+  let mut res : Array α := #[]
+  for ⟨k, v⟩ in self do
+    match k with
+    | .targetFacet _ _ f =>
+      if h : f = facet then
+        have of_data := by unfold BuildData; simp [h]
+        res := res.push <| cast of_data v
+    | _ => pure ()
+  return res
+
+/-- Derive an array of built external shared libraries from the store. -/
+def collectSharedExternLibs (self : BuildStore)
+[FamilyOut TargetData `externLib.shared α] : Array α :=
+  self.collectTargetFacetArray `externLib.shared

src/lake/Lake/Build/Topological.lean

@@ -0,0 +1,139 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Util.Cycle
+import Lake.Util.Store
+import Lake.Util.EquipT
+
+/-!
+# Topological / Suspending Recursive Builder
+
+This module defines a recursive build function that topologically
+(ι.e., via a depth-first search with memoization) builds the elements of
+a build store.
+
+This is called a suspending scheduler in *Build systems à la carte*.
+-/
+
+namespace Lake
+
+/-!
+## Recursive Fetching
+
+In this section, we define the primitives that make up a builder.
+-/
+
+/--
+A dependently typed monadic *fetch* function.
+
+That is, a function within the monad `m` and takes an input `a : α`
+describing what to fetch and and produces some output `b : β a` (dependently
+typed) or `b : B` (not) describing what was fetched. All build functions are
+fetch functions, but not all fetch functions need build something.
+-/
+abbrev DFetchFn (α : Type u) (β : α → Type v) (m : Type v → Type w) :=
+  (a : α) → m (β a)
+
+/-!
+In order to nest builds / fetches within one another,
+we equip the monad `m` with a fetch function of its own.
+-/
+
+/-- A transformer that equips a monad with a `DFetchFn`. -/
+abbrev DFetchT (α : Type u) (β : α → Type v) (m : Type v → Type w) :=
+  EquipT (DFetchFn α β m) m
+
+/-- A `DFetchT` that is not dependently typed. -/
+abbrev FetchT (α : Type u) (β : Type v) (m : Type v → Type w) :=
+  DFetchT α (fun _ => β) m
+
+/-!
+We can then use the such a monad as the basis for a fetch function itself.
+-/
+
+/-
+A `DFetchFn` that utilizes another `DFetchFn` equipped to the monad to
+fetch values. It is thus usually implemented recursively via some variation
+of the `recFetch` function below, hence the "rec" in both names.
+-/
+abbrev DRecFetchFn (α : Type u) (β : α → Type v) (m : Type v → Type w) :=
+  DFetchFn α β (DFetchT α β m)
+
+/-- A `DRecFetchFn` that is not dependently typed. -/
+abbrev RecFetchFn (α : Type u) (β : Type v) (m : Type v → Type w) :=
+  α → FetchT α β m β
+
+/-- A `DFetchFn` that provides its base `DRecFetchFn` with itself. -/
+@[specialize] partial def recFetch
+[(α : Type u) → Nonempty (m α)] (fetch : DRecFetchFn α β m) : DFetchFn α β m :=
+  fun a => fetch a (recFetch fetch)
+
+/-!
+The basic `recFetch` can fail to terminate in a variety of ways,
+it can even cycle (i.e., `a` fetches `b` which fetches `a`). Thus, we
+define the `acyclicRecFetch` below to guard against such cases.
+-/
+
+/--
+A `recFetch` augmented by a `CycleT` to guard against recursive cycles.
+If the set of visited keys is finite, this function should provably terminate.
+
+We use `keyOf` to the derive the unique key of a fetch from its descriptor
+`a : α`. We do this because descriptors may not be comparable and/or contain
+more information than necessary to determine uniqueness.
+-/
+@[inline] partial def recFetchAcyclic [BEq κ] [Monad m]
+(keyOf : α → κ) (fetch : DRecFetchFn α β (CycleT κ m)) : DFetchFn α β (CycleT κ m) :=
+  recFetch fun a recurse =>
+    /-
+    NOTE: We provide the stack directly to `recurse` rather than
+    get it through `ReaderT` to prevent it being overridden by the `fetch`
+    function (and thereby potentially produce a cycle).
+    -/
+    guardCycle (keyOf a) fun stack => fetch a (recurse · stack) stack
+
+/-!
+When building, we usually do not want to build the same thing twice during
+a single build pass. At the same time, separate builds may both wish to fetch
+the same thing. Thus, we need to store past build results to return them upon
+future fetches. This is what `recFetchMemoize` below does.
+-/
+
+/--
+`recFetchAcyclic` augmented with a `MonadDStore` to
+memoize fetch results and thus avoid computing the same result twice.
+-/
+@[inline] def recFetchMemoize [BEq κ] [Monad m] [MonadDStore κ β m]
+(keyOf : α → κ) (fetch : DRecFetchFn α (fun a => β (keyOf a)) (CycleT κ m))
+: DFetchFn α (fun a => β (keyOf a)) (CycleT κ m) :=
+  recFetchAcyclic keyOf fun a recurse =>
+    fetchOrCreate (keyOf a) do fetch a recurse
+
+/-!
+## Building
+
+In this section, we use the abstractions we have just created to define
+the desired topological recursive build function (a.k.a. a suspending scheduler).
+-/
+
+/-- Recursively builds objects for the keys `κ`, avoiding cycles. -/
+@[inline] def buildAcyclic [BEq κ] [Monad m]
+(keyOf : α → κ) (a : α) (build : RecFetchFn α β (CycleT κ m)) : ExceptT (Cycle κ) m β :=
+  recFetchAcyclic (β := fun _ => β) keyOf build a []
+
+/-- Dependently typed version of `buildTop`. -/
+@[inline] def buildDTop (β) [BEq κ] [Monad m] [MonadDStore κ β m]
+(keyOf : α → κ) (a : α) (build : DRecFetchFn α (fun a => β (keyOf a)) (CycleT κ m))
+: ExceptT (Cycle κ) m (β (keyOf a)) :=
+  recFetchMemoize keyOf build a []
+
+/--
+Recursively fills a `MonadStore` of key-object pairs by
+building objects topologically (ι.e., depth-first with memoization).
+If a cycle is detected, the list of keys traversed is thrown.
+-/
+@[inline] def buildTop [BEq κ] [Monad m] [MonadStore κ β m]
+(keyOf : α → κ) (a : α) (build : RecFetchFn α β (CycleT κ m)) : ExceptT (Cycle κ) m β :=
+  recFetchMemoize (β := fun _ => β) keyOf build a []

src/lake/Lake/Build/Trace.lean

@@ -0,0 +1,273 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+
+open System
+namespace Lake
+
+--------------------------------------------------------------------------------
+/-! # Utilities -/
+--------------------------------------------------------------------------------
+
+class CheckExists.{u} (i : Type u) where
+  /-- Check whether there already exists an artifact for the given target info. -/
+  checkExists : i → BaseIO Bool
+
+export CheckExists (checkExists)
+
+instance : CheckExists FilePath where
+  checkExists := FilePath.pathExists
+
+--------------------------------------------------------------------------------
+/-! # Trace Abstraction -/
+--------------------------------------------------------------------------------
+
+class ComputeTrace.{u,v,w} (i : Type u) (m : outParam $ Type v → Type w) (t : Type v) where
+  /--  Compute the trace of some target info using information from the monadic context. -/
+  computeTrace : i → m t
+
+def computeTrace [ComputeTrace i m t] [MonadLiftT m n] (info : i) : n t :=
+  liftM <| ComputeTrace.computeTrace info
+
+class NilTrace.{u} (t : Type u) where
+  /-- The nil trace. Should not unduly clash with a proper trace. -/
+  nilTrace : t
+
+export NilTrace (nilTrace)
+
+instance [NilTrace t] : Inhabited t := ⟨nilTrace⟩
+
+class MixTrace.{u} (t : Type u) where
+  /-- Combine two traces. The result should be dirty if either of the inputs is dirty. -/
+  mixTrace : t → t → t
+
+export MixTrace (mixTrace)
+
+def mixTraceM [MixTrace t] [Pure m] (t1 t2 : t) : m t :=
+  pure <| mixTrace t1 t2
+
+section
+variable [MixTrace t] [NilTrace t]
+
+def mixTraceList (traces : List t) : t :=
+  traces.foldl mixTrace nilTrace
+
+def mixTraceArray (traces : Array t) : t :=
+  traces.foldl mixTrace nilTrace
+
+variable [ComputeTrace i m t]
+
+def computeListTrace [MonadLiftT m n] [Monad n] (artifacts : List i) : n t :=
+  mixTraceList <$> artifacts.mapM computeTrace
+
+instance [Monad m] : ComputeTrace (List i) m t := ⟨computeListTrace⟩
+
+def computeArrayTrace [MonadLiftT m n] [Monad n] (artifacts : Array i) : n t :=
+  mixTraceArray <$> artifacts.mapM computeTrace
+
+instance [Monad m] : ComputeTrace (Array i) m t := ⟨computeArrayTrace⟩
+end
+
+--------------------------------------------------------------------------------
+/-! # Hash Trace -/
+--------------------------------------------------------------------------------
+
+/--
+A content hash.
+TODO: Use a secure hash rather than the builtin Lean hash function.
+-/
+structure Hash where
+  val : UInt64
+  deriving BEq, DecidableEq, Repr
+
+namespace Hash
+
+def ofNat (n : Nat) :=
+  mk n.toUInt64
+
+def loadFromFile (hashFile : FilePath) : IO (Option Hash) :=
+  return (← IO.FS.readFile hashFile).toNat?.map ofNat
+
+def nil : Hash :=
+  mk <| 1723 -- same as Name.anonymous
+
+instance : NilTrace Hash := ⟨nil⟩
+
+def mix (h1 h2 : Hash) : Hash :=
+  mk <| mixHash h1.val h2.val
+
+instance : MixTrace Hash := ⟨mix⟩
+
+protected def toString (self : Hash) : String :=
+  toString self.val
+
+instance : ToString Hash := ⟨Hash.toString⟩
+
+def ofString (str : String) :=
+  mix nil <| mk <| hash str -- same as Name.mkSimple
+
+def ofByteArray (bytes : ByteArray) : Hash :=
+  ⟨hash bytes⟩
+
+end Hash
+
+class ComputeHash (α : Type u) (m : outParam $ Type → Type v)  where
+  computeHash : α → m Hash
+
+instance [ComputeHash α m] : ComputeTrace α m Hash := ⟨ComputeHash.computeHash⟩
+
+def pureHash [ComputeHash α Id] (a : α) : Hash :=
+  ComputeHash.computeHash a
+
+def computeHash [ComputeHash α m] [MonadLiftT m n] (a : α) : n Hash :=
+  liftM <| ComputeHash.computeHash a
+
+instance : ComputeHash String Id := ⟨Hash.ofString⟩
+
+def computeFileHash (file : FilePath) : IO Hash :=
+  Hash.ofByteArray <$> IO.FS.readBinFile file
+
+instance : ComputeHash FilePath IO := ⟨computeFileHash⟩
+
+/--
+  A wrapper around `FilePath` that adjusts its `ComputeHash` implementation
+  to normalize `\r\n` sequences to `\n` for cross-platform compatibility. -/
+structure TextFilePath where
+  path : FilePath
+
+instance : ComputeHash TextFilePath IO where
+  computeHash file := do
+    let text ← IO.FS.readFile file.path
+    let text := text.replace "\r\n" "\n"
+    return Hash.ofString text
+
+instance [ComputeHash α m] [Monad m] : ComputeHash (Array α) m where
+  computeHash ar := ar.foldlM (fun b a => Hash.mix b <$> computeHash a) Hash.nil
+
+--------------------------------------------------------------------------------
+/-! # Modification Time (MTime) Trace -/
+--------------------------------------------------------------------------------
+
+open IO.FS (SystemTime)
+
+/-- A modification time. -/
+def MTime := SystemTime
+
+namespace MTime
+
+instance : OfNat MTime (nat_lit 0) := ⟨⟨0,0⟩⟩
+
+instance : BEq MTime := inferInstanceAs (BEq SystemTime)
+instance : Repr MTime := inferInstanceAs (Repr SystemTime)
+
+instance : Ord MTime := inferInstanceAs (Ord SystemTime)
+instance : LT MTime := ltOfOrd
+instance : LE MTime := leOfOrd
+instance : Min MTime := minOfLe
+instance : Max MTime := maxOfLe
+
+instance : NilTrace MTime := ⟨0⟩
+instance : MixTrace MTime := ⟨max⟩
+
+end MTime
+
+class GetMTime (α) where
+  getMTime : α → IO MTime
+
+export GetMTime (getMTime)
+instance [GetMTime α] : ComputeTrace α IO MTime := ⟨getMTime⟩
+
+def getFileMTime (file : FilePath) : IO MTime :=
+  return (← file.metadata).modified
+
+instance : GetMTime FilePath := ⟨getFileMTime⟩
+instance : GetMTime TextFilePath := ⟨(getFileMTime ·.path)⟩
+
+/-- Check if the info's `MTIme` is at least `depMTime`. -/
+def checkIfNewer [GetMTime i] (info : i) (depMTime : MTime) : BaseIO Bool :=
+  (do pure ((← getMTime info) >= depMTime : Bool)).catchExceptions fun _ => pure false
+
+--------------------------------------------------------------------------------
+/-! # Lake Build Trace (Hash + MTIme) -/
+--------------------------------------------------------------------------------
+
+/-- Trace used for common Lake targets. Combines `Hash` and `MTime`. -/
+structure BuildTrace where
+  hash : Hash
+  mtime : MTime
+  deriving Repr
+
+namespace BuildTrace
+
+def withHash (hash : Hash) (self : BuildTrace) : BuildTrace :=
+  {self with hash}
+
+def withoutHash (self : BuildTrace) : BuildTrace :=
+  {self with hash := Hash.nil}
+
+def withMTime (mtime : MTime) (self : BuildTrace) : BuildTrace :=
+  {self with mtime}
+
+def withoutMTime (self : BuildTrace) : BuildTrace :=
+  {self with mtime := 0}
+
+def fromHash (hash : Hash) : BuildTrace :=
+  mk hash 0
+
+instance : Coe Hash BuildTrace := ⟨fromHash⟩
+
+def fromMTime (mtime : MTime) : BuildTrace :=
+  mk Hash.nil mtime
+
+instance : Coe MTime BuildTrace := ⟨fromMTime⟩
+
+def nil : BuildTrace :=
+  mk Hash.nil 0
+
+instance : NilTrace BuildTrace := ⟨nil⟩
+
+def compute [ComputeHash i m] [MonadLiftT m IO] [GetMTime i] (info : i) : IO BuildTrace :=
+  return mk (← computeHash info) (← getMTime info)
+
+instance [ComputeHash i m] [MonadLiftT m IO] [GetMTime i] : ComputeTrace i IO BuildTrace := ⟨compute⟩
+
+def mix (t1 t2 : BuildTrace) : BuildTrace :=
+  mk (Hash.mix t1.hash t2.hash) (max t1.mtime t2.mtime)
+
+instance : MixTrace BuildTrace := ⟨mix⟩
+
+/--
+Check the build trace against the given target info and hash
+to see if the target is up-to-date.
+-/
+def checkAgainstHash [CheckExists i]
+(info : i) (hash : Hash) (self : BuildTrace) : BaseIO Bool :=
+  pure (hash == self.hash) <&&> checkExists info
+
+/--
+Check the build trace against the given target info and its modification time
+to see if the target is up-to-date.
+-/
+def checkAgainstTime [CheckExists i] [GetMTime i]
+(info : i) (self : BuildTrace) : BaseIO Bool :=
+  checkIfNewer info self.mtime
+
+/--
+Check the build trace against the given target info and its trace file
+to see if the target is up-to-date.
+-/
+def checkAgainstFile [CheckExists i] [GetMTime i]
+(info : i) (traceFile : FilePath) (self : BuildTrace) : BaseIO Bool := do
+  let act : IO _ := do
+    if let some hash ← Hash.loadFromFile traceFile then
+      self.checkAgainstHash info hash
+    else
+      return self.mtime < (← getMTime info)
+  act.catchExceptions fun _ => pure false
+
+def writeToFile (traceFile : FilePath) (self : BuildTrace) : IO PUnit :=
+  IO.FS.writeFile traceFile self.hash.toString
+
+end BuildTrace

src/lake/Lake/CLI.lean

@@ -0,0 +1,6 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.CLI.Main

src/lake/Lake/CLI/Actions.lean

@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Build.Index
+
+namespace Lake
+
+def env (cmd : String) (args : Array String := #[]) : LakeT IO UInt32 := do
+  IO.Process.spawn {cmd, args, env := ← getAugmentedEnv} >>= (·.wait)
+
+def exe (name : Name) (args  : Array String := #[]) (oldMode := false) : LakeT LogIO UInt32 := do
+  let ws ← getWorkspace
+  if let some exe := ws.findLeanExe? name then
+    let exeFile ← ws.runBuild (exe.build >>= (·.await)) oldMode
+    env exeFile.toString args
+  else
+    error s!"unknown executable `{name}`"
+
+def uploadRelease (pkg : Package) (tag : String) : LogIO Unit := do
+  let mut args :=
+    #["release", "upload", tag, pkg.buildArchiveFile.toString, "--clobber"]
+  if let some repo := pkg.releaseRepo? then
+    args := args.append #["-R", repo]
+  tar pkg.buildArchive pkg.buildDir pkg.buildArchiveFile
+    (excludePaths := #["*.tar.gz", "*.tar.gz.trace"])
+  logInfo s!"Uploading {tag}/{pkg.buildArchive}"
+  proc {cmd := "gh", args}

src/lake/Lake/CLI/Build.lean

@@ -0,0 +1,187 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Build.Index
+import Lake.CLI.Error
+
+namespace Lake
+
+/-! ## Build Target Specifiers -/
+
+structure BuildSpec where
+  info : BuildInfo
+  getBuildJob : BuildData info.key → BuildJob Unit
+
+@[inline] def BuildSpec.getJob (self : BuildSpec) (data : BuildData self.info.key) : Job Unit :=
+  discard <| self.getBuildJob data
+
+@[inline] def BuildData.toBuildJob
+[FamilyOut BuildData k (BuildJob α)] (data : BuildData k) : BuildJob Unit :=
+  discard <| ofFamily data
+
+@[inline] def mkBuildSpec (info : BuildInfo)
+[FamilyOut BuildData info.key (BuildJob α)] : BuildSpec :=
+  {info, getBuildJob := BuildData.toBuildJob}
+
+@[inline] def mkConfigBuildSpec (facetType : String)
+(info : BuildInfo) (config : FacetConfig Fam ι facet) (h : BuildData info.key = Fam facet)
+: Except CliError BuildSpec := do
+  let some getJob := config.getJob?
+    | throw <| CliError.nonCliFacet facetType facet
+  return {info, getBuildJob := h ▸ getJob}
+
+def BuildSpec.build (self : BuildSpec) : RecBuildM (Job Unit) :=
+  self.getJob <$> buildIndexTop' self.info
+
+def buildSpecs (specs : Array BuildSpec) : BuildM PUnit := do
+  let jobs ← RecBuildM.run do specs.mapM (·.build)
+  jobs.forM (discard <| ·.await)
+
+/-! ## Parsing CLI Build Target Specifiers -/
+
+def parsePackageSpec (ws : Workspace) (spec : String) : Except CliError Package :=
+  if spec.isEmpty then
+    return ws.root
+  else
+    match ws.findPackage? <| stringToLegalOrSimpleName spec with
+    | some pkg => return pkg
+    | none => throw <| CliError.unknownPackage spec
+
+open Module in
+def resolveModuleTarget (ws : Workspace) (mod : Module) (facet : Name) : Except CliError BuildSpec :=
+  if facet.isAnonymous then
+    return mkBuildSpec <| mod.facet leanBinFacet
+  else if let some config := ws.findModuleFacetConfig? facet then do
+    mkConfigBuildSpec "module" (mod.facet facet) config rfl
+  else
+    throw <| CliError.unknownFacet "module" facet
+
+def resolveLibTarget (ws : Workspace) (lib : LeanLib) (facet : Name) : Except CliError (Array BuildSpec) :=
+  if facet.isAnonymous then
+    lib.defaultFacets.mapM (resolveFacet ·)
+  else
+    Array.singleton <$> resolveFacet facet
+where
+  resolveFacet facet :=
+    if let some config := ws.findLibraryFacetConfig? facet then do
+      mkConfigBuildSpec "library" (lib.facet facet) config rfl
+    else
+      throw <| CliError.unknownFacet "library" facet
+
+def resolveExeTarget (exe : LeanExe) (facet : Name) : Except CliError BuildSpec :=
+  if facet.isAnonymous || facet == `exe then
+    return mkBuildSpec exe.exe
+  else
+    throw <| CliError.unknownFacet "executable" facet
+
+def resolveExternLibTarget (lib : ExternLib) (facet : Name) : Except CliError BuildSpec :=
+  if facet.isAnonymous || facet = `static then
+    return mkBuildSpec lib.static
+  else if facet = `shared then
+    return mkBuildSpec lib.shared
+  else
+    throw <| CliError.unknownFacet "external library" facet
+
+def resolveCustomTarget (pkg : Package)
+(name facet : Name) (config : TargetConfig pkg.name name) : Except CliError BuildSpec :=
+  if !facet.isAnonymous then
+    throw <| CliError.invalidFacet name facet
+  else do
+    let info := pkg.target name
+    have h : BuildData info.key = CustomData (pkg.name, name) := rfl
+    return {info, getBuildJob := h ▸ config.getJob}
+
+def resolveTargetInPackage (ws : Workspace)
+(pkg : Package) (target facet : Name) : Except CliError (Array BuildSpec) :=
+  if let some config := pkg.findTargetConfig? target then
+    Array.singleton <$> resolveCustomTarget pkg target facet config
+  else if let some exe := pkg.findLeanExe? target then
+    Array.singleton <$> resolveExeTarget exe facet
+  else if let some lib := pkg.findExternLib? target then
+    Array.singleton <$> resolveExternLibTarget lib facet
+  else if let some lib := pkg.findLeanLib? target then
+    resolveLibTarget ws lib facet
+  else if let some mod := pkg.findModule? target then
+    Array.singleton <$> resolveModuleTarget ws mod facet
+  else
+    throw <| CliError.missingTarget pkg.name (target.toString false)
+
+def resolveDefaultPackageTarget (ws : Workspace) (pkg : Package) : Except CliError (Array BuildSpec) :=
+  pkg.defaultTargets.concatMapM (resolveTargetInPackage ws pkg · .anonymous)
+
+def resolvePackageTarget (ws : Workspace) (pkg : Package) (facet : Name) : Except CliError (Array BuildSpec) :=
+  if facet.isAnonymous then
+    resolveDefaultPackageTarget ws pkg
+  else if let some config := ws.findPackageFacetConfig? facet then do
+    Array.singleton <$> mkConfigBuildSpec "package" (pkg.facet facet) config rfl
+  else
+    throw <| CliError.unknownFacet "package" facet
+
+def resolveTargetInWorkspace (ws : Workspace)
+(target : Name) (facet : Name) : Except CliError (Array BuildSpec) :=
+  if let some ⟨pkg, config⟩ := ws.findTargetConfig? target then
+    Array.singleton <$> resolveCustomTarget pkg target facet config
+  else if let some exe := ws.findLeanExe? target then
+    Array.singleton <$> resolveExeTarget exe facet
+  else if let some lib := ws.findExternLib? target then
+    Array.singleton <$> resolveExternLibTarget lib facet
+  else if let some lib := ws.findLeanLib? target then
+    resolveLibTarget ws lib facet
+  else if let some pkg := ws.findPackage? target then
+    resolvePackageTarget ws pkg facet
+  else if let some mod := ws.findModule? target then
+    Array.singleton <$> resolveModuleTarget ws mod facet
+  else
+    throw <| CliError.unknownTarget target
+
+def resolveTargetBaseSpec
+(ws : Workspace) (spec : String) (facet : Name) : Except CliError (Array BuildSpec) := do
+  match spec.splitOn "/" with
+  | [spec] =>
+    if spec.isEmpty then
+      resolvePackageTarget ws ws.root facet
+    else if spec.startsWith "@" then
+      let pkg ← parsePackageSpec ws <| spec.drop 1
+      resolvePackageTarget ws pkg facet
+    else if spec.startsWith "+" then
+      let mod := spec.drop 1 |>.toName
+      if let some mod := ws.findModule? mod then
+        Array.singleton <$> resolveModuleTarget ws mod facet
+      else
+        throw <| CliError.unknownModule mod
+    else
+      resolveTargetInWorkspace ws (stringToLegalOrSimpleName spec) facet
+  | [pkgSpec, targetSpec] =>
+    let pkgSpec := if pkgSpec.startsWith "@" then pkgSpec.drop 1 else pkgSpec
+    let pkg ← parsePackageSpec ws pkgSpec
+    if targetSpec.isEmpty then
+      resolvePackageTarget ws pkg facet
+    else if targetSpec.startsWith "+" then
+      let mod := targetSpec.drop 1 |>.toName
+      if let some mod := pkg.findModule? mod then
+        Array.singleton <$> resolveModuleTarget ws mod facet
+      else
+        throw <| CliError.unknownModule mod
+    else
+      resolveTargetInPackage ws pkg targetSpec facet
+  | _ =>
+    throw <| CliError.invalidTargetSpec spec '/'
+
+def parseTargetSpec (ws : Workspace) (spec : String) : Except CliError (Array BuildSpec) := do
+  match spec.splitOn ":" with
+  | [spec] =>
+    resolveTargetBaseSpec ws spec .anonymous
+  | [rootSpec, facet] =>
+    resolveTargetBaseSpec ws rootSpec facet.toName
+  | _ =>
+    throw <| CliError.invalidTargetSpec spec ':'
+
+def parseTargetSpecs (ws : Workspace) (specs : List String) : Except CliError (Array BuildSpec) := do
+  let mut results := #[]
+  for spec in specs do
+    results := results ++ (← parseTargetSpec ws spec)
+  if results.isEmpty then
+    results ← resolveDefaultPackageTarget ws ws.root
+  return results

src/lake/Lake/CLI/Error.lean

@@ -0,0 +1,70 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+
+namespace Lake
+open Lean (Name)
+
+inductive CliError
+/- CLI Errors -/
+| missingCommand
+| unknownCommand (cmd : String)
+| missingArg (arg : String)
+| missingOptArg (opt arg : String)
+| unknownShortOption (opt : Char)
+| unknownLongOption (opt : String)
+| unexpectedArguments (args : List String)
+/- Init CLI Errors -/
+| unknownTemplate (spec : String)
+/- Build CLI Errors -/
+| unknownModule (mod : Name)
+| unknownPackage (spec : String)
+| unknownFacet (type : String) (facet : Name)
+| unknownTarget (target : Name)
+| missingModule (pkg : Name) (mod : Name)
+| missingTarget (pkg : Name) (spec : String)
+| nonCliTarget (target : Name)
+| nonCliFacet (type : String) (facet : Name)
+| invalidTargetSpec (spec : String) (tooMany : Char)
+| invalidFacet (target : Name) (facet : Name)
+/- Script CLI Error -/
+| unknownScript (script : String)
+| missingScriptDoc (script : String)
+| invalidScriptSpec (spec : String)
+/- Config Errors -/
+| unknownLeanInstall
+| unknownLakeInstall
+| leanRevMismatch (expected actual : String)
+deriving Inhabited, Repr
+
+namespace CliError
+
+def toString : CliError → String
+| missingCommand          => "missing command"
+| unknownCommand cmd      => s!"unknown command '{cmd}'"
+| missingArg arg          => s!"missing {arg}"
+| missingOptArg opt arg   => s!"missing {arg} after {opt}"
+| unknownShortOption opt  => s!"unknown short option '-{opt}'"
+| unknownLongOption opt   => s!"unknown long option '{opt}'"
+| unexpectedArguments as  => s!"unexpected arguments: {" ".intercalate as}"
+| unknownTemplate spec    => s!"unknown package template `{spec}`"
+| unknownModule mod       => s!"unknown module `{mod.toString false}`"
+| unknownPackage spec     => s!"unknown package `{spec}`"
+| unknownFacet ty f       => s!"unknown {ty} facet `{f.toString false}`"
+| unknownTarget t         => s!"unknown target `{t.toString false}`"
+| missingModule pkg mod   => s!"package '{pkg.toString false}' has no module '{mod.toString false}'"
+| missingTarget pkg spec  => s!"package '{pkg.toString false}' has no target '{spec}'"
+| nonCliTarget t          => s!"target `{t.toString false}` is not a buildable via `lake`"
+| nonCliFacet t f         => s!"{t} facet `{f.toString false}` is not a buildable via `lake`"
+| invalidTargetSpec s c   => s!"invalid script spec '{s}' (too many '{c}')"
+| invalidFacet t f        => s!"invalid facet `{f.toString false}`; target {t.toString false} has no facets"
+| unknownScript s         => s!"unknown script {s}"
+| missingScriptDoc s      => s!"no documentation provided for `{s}`"
+| invalidScriptSpec s     => s!"invalid script spec '{s}' (too many '/')"
+| unknownLeanInstall      => "could not detect a Lean installation"
+| unknownLakeInstall      => "could not detect the configuration of the Lake installation"
+| leanRevMismatch e a     => s!"expected Lean commit {e}, but got {if a.isEmpty then "nothing" else a}"
+
+instance : ToString CliError := ⟨toString⟩

src/lake/Lake/CLI/Help.lean

@@ -0,0 +1,242 @@
+/-
+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, Mac Malone
+-/
+import Lake.Version
+
+namespace Lake
+
+def usage :=
+uiVersionString ++ "
+
+USAGE:
+  lake [OPTIONS] <COMMAND>
+
+OPTIONS:
+  --version             print version and exit
+  --help, -h            print help of the program or a command and exit
+  --dir, -d=file        use the package configuration in a specific directory
+  --file, -f=file       use a specific file for the package configuration
+  --quiet, -q           hide progress messages
+  --verbose, -v         show verbose information (command invocations)
+  --lean=cmd            specify the `lean` command used by Lake
+  -K key[=value]        set the configuration file option named key
+  --old                 only rebuild modified modules (ignore transitive deps)
+  --update, -U          update manifest before building
+
+COMMANDS:
+  new <name> [<temp>]   create a Lean package in a new directory
+  init <name> [<temp>]  create a Lean package in the current directory
+  build [<targets>...]  build targets
+  update                update dependencies
+  upload <tag>          upload build artifacts to a GitHub release
+  clean                 remove build outputs
+  script                manage and run workspace scripts
+  scripts               shorthand for `lake script list`
+  run <script>          shorthand for `lake script run`
+  serve                 start the Lean language server
+  env <cmd> [<args>...] execute a command in the workspace's environment
+  exe <exe> [<args>...] build an exe and run it in the workspace's environment
+
+See `lake help <command>` for more information on a specific command."
+
+def templateHelp :=
+s!"The initial configuration and starter files are based on the template:
+
+  std                   library and executable; default
+  exe                   executable only
+  lib                   library only
+  math                  library only with a mathlib dependency"
+
+def helpNew :=
+s!"Create a Lean package in a new directory
+
+USAGE:
+  lake new <name> [<template>]
+
+{templateHelp}"
+
+def helpInit :=
+s!"Create a Lean package in the current directory
+
+USAGE:
+  lake init <name> [<template>]
+
+{templateHelp}"
+
+def helpBuild :=
+"Build targets
+
+USAGE:
+  lake build [<targets>...]
+
+A target is specified with a string of the form:
+
+  [[@]<package>/][<target>|[+]<module>][:<facet>]
+
+The optional `@` and `+` markers can be used to disambiguate packages
+and modules from other kinds of targets (i.e., executables and libraries).
+
+LIBRARY FACETS:         build the library's ...
+  lean (default)        Lean binaries (*.olean, *.ilean files)
+  static                static binary (*.a file)
+  shared                shared binary (*.so, *.dll, or *.dylib file)
+
+MODULE FACETS:          build the module's ...
+  deps                  transitive local imports & shared library dependencies
+  bin (default)         Lean binaries (*.olean, *.ilean files) and *.c file
+  o                     *.o object file (of its C file)
+  dynlib                shared library (e.g., for `--load-dynlib`)
+
+TARGET EXAMPLES:        build the ...
+  a                     default facet of target `a`
+  @a                    default target(s) of package `a`
+  +A                    olean and .ilean files of module `A`
+  a/b                   default facet of target `b` of package `a`
+  a/+A:c                C file of module `A` of package `a`
+  :foo                  facet `foo` of the root package
+
+A bare `build` command will build the default facet of the root package.
+Package dependencies are not updated during a build."
+
+def helpUpdate :=
+"Update dependencies
+
+USAGE:
+  lake update
+
+This command sets up the directory with the package's dependencies
+(i.e., `packagesDir`, which is, by default, `lake-packages`).
+
+For each (transitive) git dependency, the specified commit is checked out
+into a sub-directory of `packagesDir`. Already checked out dependencies are
+updated to the latest version compatible with the package's configuration.
+If there are dependencies on multiple versions of the same package, the
+version materialized is undefined. The specific revision of the resolved
+packages are cached in the `manifest.json` file of the `packagesDir`.
+
+No copy is made of local dependencies."
+
+def helpUpload :=
+"Upload build artifacts to a GitHub release
+
+USAGE:
+  lake upload <tag>
+
+Packs the root package's `buildDir` into a `tar.gz` archive using `tar` and
+then uploads the asset to the pre-existing GitHub release `tag` using `gh`."
+
+def helpClean :=
+"Remove build outputs
+
+USAGE:
+  lake clean
+
+Deletes the build directory of the package."
+
+def helpScriptCli :=
+"Manage Lake scripts
+
+USAGE:
+  lake script <COMMAND>
+
+COMMANDS:
+  list                  list available scripts
+  run <script>          run a script
+  doc <script>          print the docstring of a given script
+
+See `lake help <command>` for more information on a specific command."
+
+def helpScriptList :=
+"List available scripts
+
+USAGE:
+  lake script list
+
+This command prints the list of all available scripts in the workspace."
+
+def helpScriptRun :=
+"Run a script
+
+USAGE:
+  lake script run [<package>/]<script> [<args>...]
+
+This command runs the given `script` from `package`, passing `args` to it.
+Defaults to the root package.
+
+A bare `run` command will run the default script(s) of the root package
+(with no arguments)."
+
+def helpScriptDoc :=
+"Print a script's docstring
+
+USAGE:
+  lake script doc [<package>/]<script>
+
+Print the docstring of `script` in `package`. Defaults to the root package."
+
+def helpServe :=
+"Start the Lean language server
+
+USAGE:
+  lake serve [-- <args>...]
+
+Run the language server of the Lean installation (i.e., via `lean --server`)
+with the package configuration's `moreServerArgs` field and `args`.
+"
+
+def helpEnv :=
+"Execute a command in the workspace's environment
+
+USAGE:
+  lake env <cmd> [<args>...]
+
+Spawns a new process executing `cmd` with the given `args` and with
+the environment set based on the workspace configuration and the detected
+Lean/Lake installations.
+
+Specifically, this command sets the following environment variables:
+
+  LAKE                  set to the detected Lake executable
+  LAKE_HOME             set to the detected Lake home
+  LEAN_SYSROOT          set to the detected Lean sysroot
+  LEAN_AR               set to the detected Lean `ar` binary
+  LEAN_CC               set to the detected `cc` (if not using bundled one)
+  LEAN_PATH             adds the workspace's library directories
+  LEAN_SRC_PATH         adds the workspace's source directories
+  PATH                  adds the workspace's library directories (Windows)
+  DYLD_LIBRARY_PATH     adds the workspace's library directories (MacOS)
+  LD_LIBRARY_PATH       adds the workspace's library directories (other Unix)"
+
+def helpExe :=
+"Build an executable target and run it in the workspace's environment
+
+USAGE:
+  lake exe <exe-target> [<args>...]
+
+Looks for the executable target in the workspace (see `lake help build` to
+learn how to specify targets), builds it if it is out of date, and then runs
+it with the given `args` in the workspace's environment (see `lake help env`
+for how the environment is set)."
+
+def helpScript : (cmd : String) → String
+| "list"      => helpScriptList
+| "run"       => helpScriptRun
+| "doc"       => helpScriptDoc
+| _           => helpScriptCli
+
+def help : (cmd : String) → String
+| "new"       => helpNew
+| "init"      => helpInit
+| "build"     => helpBuild
+| "update"    => helpUpdate
+| "upload"    => helpUpload
+| "clean"     => helpClean
+| "script"    => helpScriptCli
+| "scripts"   => helpScriptList
+| "run"       => helpScriptRun
+| "serve"     => helpServe
+| "env"       => helpEnv
+| "exe"       => helpExe
+| _           => usage

src/lake/Lake/CLI/Init.lean

@@ -0,0 +1,205 @@
+/-
+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, Mac Malone
+-/
+import Lake.Util.Git
+import Lake.Util.Sugar
+import Lake.Config.Package
+import Lake.Config.Workspace
+import Lake.Load.Config
+import Lake.Build.Actions
+
+namespace Lake
+open Git System
+
+/-- The default module of an executable in `std` package. -/
+def defaultExeRoot : Name := `Main
+
+/-- `elan` toolchain file name -/
+def toolchainFileName : FilePath :=
+  "lean-toolchain"
+
+def gitignoreContents :=
+s!"/{defaultBuildDir}
+/{defaultPackagesDir}/*
+"
+
+def libFileContents :=
+  s!"def hello := \"world\""
+
+def mainFileName : FilePath :=
+  s!"{defaultExeRoot}.lean"
+
+def mainFileContents (libRoot : String) :=
+s!"import {libRoot}
+
+def main : IO Unit :=
+  IO.println s!\"Hello, \{hello}!\"
+"
+
+def exeFileContents :=
+s!"def main : IO Unit :=
+  IO.println s!\"Hello, world!\"
+"
+
+def stdConfigFileContents (pkgName libRoot : String) :=
+s!"import Lake
+open Lake DSL
+
+package {pkgName} \{
+  -- add package configuration options here
+}
+
+lean_lib {libRoot} \{
+  -- add library configuration options here
+}
+
+@[default_target]
+lean_exe {pkgName} \{
+  root := `Main
+}
+"
+
+def exeConfigFileContents (pkgName exeRoot : String) :=
+s!"import Lake
+open Lake DSL
+
+package {pkgName} \{
+  -- add package configuration options here
+}
+
+@[default_target]
+lean_exe {exeRoot} \{
+  -- add executable configuration options here
+}
+"
+
+def libConfigFileContents (pkgName libRoot : String) :=
+s!"import Lake
+open Lake DSL
+
+package {pkgName} \{
+  -- add package configuration options here
+}
+
+@[default_target]
+lean_lib {libRoot} \{
+  -- add library configuration options here
+}
+"
+
+def mathConfigFileContents (pkgName libRoot : String) :=
+s!"import Lake
+open Lake DSL
+
+package {pkgName} \{
+  -- add any package configuration options here
+}
+
+require mathlib from git
+  \"https://github.com/leanprover-community/mathlib4.git\"
+
+@[default_target]
+lean_lib {libRoot} \{
+  -- add any library configuration options here
+}
+"
+
+def mathToolchainUrl : String :=
+  "https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain"
+
+/-- The options for the template argument to `initPkg`. -/
+inductive InitTemplate
+| std | exe | lib | math
+deriving Repr, DecidableEq
+
+instance : Inhabited InitTemplate := ⟨.std⟩
+
+def InitTemplate.parse? : String → Option InitTemplate
+| "std" => some .std
+| "exe" => some .exe
+| "lib" => some .lib
+| "math" => some .math
+| _ => none
+
+def InitTemplate.configFileContents (pkgName root : String) : InitTemplate → String
+| .std => stdConfigFileContents pkgName root
+| .lib => libConfigFileContents pkgName root
+| .exe => exeConfigFileContents pkgName root
+| .math => mathConfigFileContents pkgName root
+
+def escapeName! : Name → String
+| .anonymous        => "[anonymous]"
+| .str .anonymous s => escape s
+| .str n s          => escapeName! n ++ "." ++ escape s
+| _                 => unreachable!
+where
+  escape s :=  Lean.idBeginEscape.toString ++ s ++ Lean.idEndEscape.toString
+
+/-- Initialize a new Lake package in the given directory with the given name. -/
+def initPkg (dir : FilePath) (name : String) (tmp : InitTemplate) : LogIO PUnit := do
+  let pkgName := stringToLegalOrSimpleName name
+
+  -- determine the name to use for the root
+  -- use upper camel case unless the specific module name already exists
+  let (root, rootFile, rootExists) ← do
+    let root := pkgName
+    let rootFile := Lean.modToFilePath dir root "lean"
+    let rootExists ← rootFile.pathExists
+    if tmp = .exe || rootExists then
+      pure (root, rootFile, rootExists)
+    else
+      let root := toUpperCamelCase (toUpperCamelCaseString name |>.toName)
+      let rootFile := Lean.modToFilePath dir root "lean"
+      pure (root, rootFile, ← rootFile.pathExists)
+
+  -- write default configuration file
+  let configFile := dir / defaultConfigFile
+  if (← configFile.pathExists) then
+    error  "package already initialized"
+  let rootNameStr := escapeName! root
+  let contents := tmp.configFileContents (escapeName! pkgName) rootNameStr
+  IO.FS.writeFile configFile contents
+
+  -- write example code if the files do not already exist
+  if tmp = .exe then
+    unless (← rootFile.pathExists) do
+      IO.FS.writeFile rootFile exeFileContents
+  else
+    if !rootExists then
+      IO.FS.createDirAll rootFile.parent.get!
+      IO.FS.writeFile rootFile libFileContents
+    if tmp = .std then
+      let mainFile := dir / mainFileName
+      unless (← mainFile.pathExists) do
+        IO.FS.writeFile mainFile <| mainFileContents rootNameStr
+
+  -- write Lean's toolchain to file (if it has one) for `elan`
+  if Lean.toolchain ≠ "" then
+    if tmp = .math then
+      download "lean-toolchain" mathToolchainUrl (dir / toolchainFileName)
+    else
+      IO.FS.writeFile (dir / toolchainFileName) <| Lean.toolchain ++ "\n"
+
+  -- update `.gitignore` with additional entries for Lake
+  let h ← IO.FS.Handle.mk (dir / ".gitignore") IO.FS.Mode.append
+  h.putStr gitignoreContents
+
+  -- initialize a `.git` repository if none already
+  unless (← FilePath.isDir <| dir / ".git") do
+    let repo := GitRepo.mk dir
+    try
+      repo.quietInit
+      unless upstreamBranch = "master" do
+        repo.checkoutBranch upstreamBranch
+    else
+      logWarning "failed to initialize git repository"
+
+def init (pkgName : String) (tmp : InitTemplate) : LogIO PUnit :=
+  initPkg "." pkgName tmp
+
+def new (pkgName : String) (tmp : InitTemplate) : LogIO PUnit := do
+  let dirName := pkgName.map fun chr => if chr == '.' then '-' else chr
+  IO.FS.createDir dirName
+  initPkg dirName pkgName tmp

src/lake/Lake/CLI/Main.lean

@@ -0,0 +1,384 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Load
+import Lake.Build.Imports
+import Lake.Util.Error
+import Lake.Util.MainM
+import Lake.Util.Cli
+import Lake.CLI.Init
+import Lake.CLI.Help
+import Lake.CLI.Build
+import Lake.CLI.Error
+import Lake.CLI.Actions
+import Lake.CLI.Serve
+
+-- # CLI
+
+open System
+open Lean (Json toJson fromJson? LeanPaths)
+
+namespace Lake
+
+/-! ## General options for top-level `lake` -/
+
+structure LakeOptions where
+  rootDir : FilePath := "."
+  configFile : FilePath := defaultConfigFile
+  leanInstall? : Option LeanInstall := none
+  lakeInstall? : Option LakeInstall := none
+  configOpts : NameMap String := {}
+  subArgs : List String := []
+  wantsHelp : Bool := false
+  verbosity : Verbosity := .normal
+  oldMode : Bool := false
+  updateDeps : Bool := false
+
+/-- Get the Lean installation. Error if missing. -/
+def LakeOptions.getLeanInstall (opts : LakeOptions) : Except CliError LeanInstall :=
+  match opts.leanInstall? with
+  | none => .error CliError.unknownLeanInstall
+  | some lean => .ok lean
+
+/-- Get the Lake installation. Error if missing. -/
+def LakeOptions.getLakeInstall (opts : LakeOptions) : Except CliError LakeInstall :=
+  match opts.lakeInstall? with
+  | none => .error CliError.unknownLakeInstall
+  | some lake => .ok lake
+
+/-- Get the Lean and Lake installation. Error if either is missing. -/
+def LakeOptions.getInstall (opts : LakeOptions) : Except CliError (LeanInstall × LakeInstall) := do
+  return (← opts.getLeanInstall, ← opts.getLakeInstall)
+
+/-- Compute the Lake environment based on `opts`. Error if an install is missing. -/
+def LakeOptions.computeEnv (opts : LakeOptions) : EIO CliError Lake.Env := do
+  Env.compute (← opts.getLakeInstall) (← opts.getLeanInstall)
+
+/-- Make a `LoadConfig` from a `LakeOptions`. -/
+def LakeOptions.mkLoadConfig (opts : LakeOptions) : EIO CliError LoadConfig :=
+  return {
+    env := ← opts.computeEnv
+    rootDir := opts.rootDir
+    configFile := opts.rootDir / opts.configFile
+    configOpts := opts.configOpts
+    leanOpts := Lean.Options.empty
+  }
+
+export LakeOptions (mkLoadConfig)
+
+/-! ## Monad -/
+
+abbrev CliMainM := ExceptT CliError MainM
+abbrev CliStateM := StateT LakeOptions CliMainM
+abbrev CliM := ArgsT CliStateM
+
+def CliM.run (self : CliM α) (args : List String) : BaseIO ExitCode := do
+  let (leanInstall?, lakeInstall?) ← findInstall?
+  let main := self args |>.run' {leanInstall?, lakeInstall?}
+  let main := main.run >>= fun | .ok a => pure a | .error e => error e.toString
+  main.run
+
+instance : MonadLift LogIO CliStateM :=
+  ⟨fun x => do MainM.runLogIO x (← get).verbosity⟩
+
+instance : MonadLift OptionIO MainM where
+  monadLift x := x.adaptExcept (fun _ => 1)
+
+/-! ## Argument Parsing -/
+
+def takeArg (arg : String) : CliM String := do
+  match (← takeArg?) with
+  | none => throw <| CliError.missingArg arg
+  | some arg => pure arg
+
+def takeOptArg (opt arg : String) : CliM String := do
+  match (← takeArg?) with
+  | none => throw <| CliError.missingOptArg opt arg
+  | some arg => pure arg
+
+/--
+Verify that there are no CLI arguments remaining
+before running the given action.
+-/
+def noArgsRem (act : CliStateM α) : CliM α := do
+  let args ← getArgs
+  if args.isEmpty then act else
+    throw <| CliError.unexpectedArguments args
+
+/-! ## Option Parsing -/
+
+def getWantsHelp : CliStateM Bool :=
+  (·.wantsHelp) <$> get
+
+def setLean (lean : String) : CliStateM PUnit := do
+  let leanInstall? ← findLeanCmdInstall? lean
+  modify ({·  with leanInstall?})
+
+def setConfigOpt (kvPair : String) : CliM PUnit :=
+  let pos := kvPair.posOf '='
+  let (key, val) :=
+    if pos = kvPair.endPos then
+      (kvPair.toName, "")
+    else
+      (kvPair.extract 0 pos |>.toName, kvPair.extract (kvPair.next pos) kvPair.endPos)
+  modifyThe LakeOptions fun opts =>
+    {opts with configOpts := opts.configOpts.insert key val}
+
+def lakeShortOption : (opt : Char) → CliM PUnit
+| 'q' => modifyThe LakeOptions ({· with verbosity := .quiet})
+| 'v' => modifyThe LakeOptions ({· with verbosity := .verbose})
+| 'd' => do let rootDir ← takeOptArg "-d" "path"; modifyThe LakeOptions ({· with rootDir})
+| 'f' => do let configFile ← takeOptArg "-f" "path"; modifyThe LakeOptions ({· with configFile})
+| 'K' => do setConfigOpt <| ← takeOptArg "-K" "key-value pair"
+| 'U' => modifyThe LakeOptions ({· with updateDeps := true})
+| 'h' => modifyThe LakeOptions ({· with wantsHelp := true})
+| opt => throw <| CliError.unknownShortOption opt
+
+def lakeLongOption : (opt : String) → CliM PUnit
+| "--quiet"   => modifyThe LakeOptions ({· with verbosity := .quiet})
+| "--verbose" => modifyThe LakeOptions ({· with verbosity := .verbose})
+| "--update"  => modifyThe LakeOptions ({· with updateDeps := true})
+| "--old"     => modifyThe LakeOptions ({· with oldMode := true})
+| "--dir"     => do let rootDir ← takeOptArg "--dir" "path"; modifyThe LakeOptions ({· with rootDir})
+| "--file"    => do let configFile ← takeOptArg "--file" "path"; modifyThe LakeOptions ({· with configFile})
+| "--lean"    => do setLean <| ← takeOptArg "--lean" "path or command"
+| "--help"    => modifyThe LakeOptions ({· with wantsHelp := true})
+| "--"        => do let subArgs ← takeArgs; modifyThe LakeOptions ({· with subArgs})
+| opt         => throw <| CliError.unknownLongOption opt
+
+def lakeOption :=
+  option {
+    short := lakeShortOption
+    long := lakeLongOption
+    longShort := shortOptionWithArg lakeShortOption
+  }
+
+/-! ## Actions -/
+
+/-- Verify the Lean version Lake was built with matches that of the give Lean installation. -/
+def verifyLeanVersion (leanInstall : LeanInstall) : Except CliError PUnit := do
+  unless leanInstall.githash == Lean.githash do
+    throw <| CliError.leanRevMismatch Lean.githash leanInstall.githash
+
+/-- Output the detected installs and verify the Lean version. -/
+def verifyInstall (opts : LakeOptions) : ExceptT CliError MainM PUnit := do
+  IO.println s!"Lean:\n{repr <| opts.leanInstall?}"
+  IO.println s!"Lake:\n{repr <| opts.lakeInstall?}"
+  let (leanInstall, _) ← opts.getInstall
+  verifyLeanVersion leanInstall
+
+def parseScriptSpec (ws : Workspace) (spec : String) : Except CliError (Package × String) :=
+  match spec.splitOn "/" with
+  | [script] => return (ws.root, script)
+  | [pkg, script] => return (← parsePackageSpec ws pkg, script)
+  | _ => throw <| CliError.invalidScriptSpec spec
+
+def parseTemplateSpec (spec : String) : Except CliError InitTemplate :=
+  if spec.isEmpty then
+    pure default
+  else if let some tmp := InitTemplate.parse? spec then
+    pure tmp
+  else
+    throw <| CliError.unknownTemplate spec
+
+/-! ## Commands -/
+
+namespace lake
+
+/-! ### `lake script` CLI -/
+
+namespace script
+
+protected def list : CliM PUnit := do
+  processOptions lakeOption
+  let config ← mkLoadConfig (← getThe LakeOptions)
+  noArgsRem do
+    let ws ← loadWorkspace config
+    ws.packageMap.forM fun _ pkg => do
+      let pkgName := pkg.name.toString (escape := false)
+      pkg.scripts.forM fun name _ =>
+        let scriptName := name.toString (escape := false)
+        IO.println s!"{pkgName}/{scriptName}"
+
+protected nonrec def run : CliM PUnit := do
+  processOptions lakeOption
+  let config ← mkLoadConfig (← getThe LakeOptions)
+  let ws ← loadWorkspace config
+  if let some spec ← takeArg? then
+    let args ← takeArgs
+    let (pkg, scriptName) ← parseScriptSpec ws spec
+    if let some script := pkg.scripts.find? scriptName then
+        exit <| ← script.run args |>.run {opaqueWs := ws}
+    else do
+      throw <| CliError.unknownScript scriptName
+  else
+    for script in ws.root.defaultScripts do
+      exitIfErrorCode <| ← script.run [] |>.run {opaqueWs := ws}
+    exit 0
+
+protected def doc : CliM PUnit := do
+  processOptions lakeOption
+  let spec ← takeArg "script name"
+  let config ← mkLoadConfig (← getThe LakeOptions)
+  noArgsRem do
+    let ws ← loadWorkspace config
+    let (pkg, scriptName) ← parseScriptSpec ws spec
+    if let some script := pkg.scripts.find? scriptName then
+      match script.doc? with
+      | some doc => IO.println doc
+      | none => throw <| CliError.missingScriptDoc scriptName
+    else
+      throw <| CliError.unknownScript scriptName
+
+protected def help : CliM PUnit := do
+  IO.println <| helpScript <| (← takeArg?).getD ""
+
+end script
+
+def scriptCli : (cmd : String) → CliM PUnit
+| "list"  => script.list
+| "run"   => script.run
+| "doc"   => script.doc
+| "help"  => script.help
+| cmd     => throw <| CliError.unknownCommand cmd
+
+/-! ### `lake` CLI -/
+
+protected def new : CliM PUnit := do
+  processOptions lakeOption
+  let pkgName ← takeArg "package name"
+  let template ← parseTemplateSpec <| (← takeArg?).getD ""
+  noArgsRem do MainM.runLogIO (new pkgName template) (← getThe LakeOptions).verbosity
+
+protected def init : CliM PUnit := do
+  processOptions lakeOption
+  let pkgName ← takeArg "package name"
+  let template ← parseTemplateSpec <| (← takeArg?).getD ""
+  noArgsRem do MainM.runLogIO (init pkgName template) (← getThe LakeOptions).verbosity
+
+protected def build : CliM PUnit := do
+  processOptions lakeOption
+  let opts ← getThe LakeOptions
+  let config ← mkLoadConfig opts
+  let ws ← loadWorkspace config opts.updateDeps
+  let targetSpecs ← takeArgs
+  let specs ← parseTargetSpecs ws targetSpecs
+  ws.runBuild (buildSpecs specs) opts.oldMode |>.run (MonadLog.io opts.verbosity)
+
+protected def resolveDeps : CliM PUnit := do
+  processOptions lakeOption
+  let opts ← getThe LakeOptions
+  let config ← mkLoadConfig opts
+  noArgsRem do
+    liftM <| discard <| (loadWorkspace config opts.updateDeps).run (MonadLog.io opts.verbosity)
+
+protected def update : CliM PUnit := do
+  processOptions lakeOption
+  let opts ← getThe LakeOptions
+  let config ← mkLoadConfig opts
+  noArgsRem do
+    liftM <| (updateManifest config).run (MonadLog.io opts.verbosity)
+
+protected def upload : CliM PUnit := do
+  processOptions lakeOption
+  let tag ← takeArg "release tag"
+  let opts ← getThe LakeOptions
+  let config ← mkLoadConfig opts
+  let ws ← loadWorkspace config
+  noArgsRem do
+    liftM <| uploadRelease ws.root tag |>.run (MonadLog.io opts.verbosity)
+
+protected def printPaths : CliM PUnit := do
+  processOptions lakeOption
+  let opts ← getThe LakeOptions
+  let config ← mkLoadConfig opts
+  printPaths config (← takeArgs) opts.oldMode opts.verbosity
+
+protected def clean : CliM PUnit := do
+  processOptions lakeOption
+  let config ← mkLoadConfig (← getThe LakeOptions)
+  noArgsRem do (← loadWorkspace config).clean
+
+protected def script : CliM PUnit := do
+  if let some cmd ← takeArg? then
+    processLeadingOptions lakeOption -- between `lake script <cmd>` and args
+    if (← getWantsHelp) then
+      IO.println <| helpScript cmd
+    else
+      scriptCli cmd
+  else
+    throw <| CliError.missingCommand
+
+protected def serve : CliM PUnit := do
+  processOptions lakeOption
+  let opts ← getThe LakeOptions
+  let args := opts.subArgs.toArray
+  let config ← mkLoadConfig opts
+  noArgsRem do exit <| ← serve config args
+
+protected def env : CliM PUnit := do
+  let cmd ← takeArg "command"; let args ← takeArgs
+  let config ← mkLoadConfig (← getThe LakeOptions)
+  let ws ← loadWorkspace config
+  let ctx := mkLakeContext ws
+  exit <| ← (env cmd args.toArray).run ctx
+
+protected def exe : CliM PUnit := do
+  let exeName ← takeArg "executable name"
+  let args ← takeArgs
+  let opts ← getThe LakeOptions
+  let config ← mkLoadConfig opts
+  let ws ← loadWorkspace config
+  let ctx := mkLakeContext ws
+  exit <| ← (exe exeName args.toArray opts.oldMode).run ctx
+
+protected def selfCheck : CliM PUnit := do
+  processOptions lakeOption
+  noArgsRem do verifyInstall (← getThe LakeOptions)
+
+protected def help : CliM PUnit := do
+  IO.println <| help <| (← takeArg?).getD ""
+
+end lake
+
+def lakeCli : (cmd : String) → CliM PUnit
+| "new"           => lake.new
+| "init"          => lake.init
+| "build"         => lake.build
+| "update"        => lake.update
+| "resolve-deps"  => lake.resolveDeps
+| "upload"        => lake.upload
+| "print-paths"   => lake.printPaths
+| "clean"         => lake.clean
+| "script"        => lake.script
+| "scripts"       => lake.script.list
+| "run"           => lake.script.run
+| "serve"         => lake.serve
+| "env"           => lake.env
+| "exe"           => lake.exe
+| "self-check"    => lake.selfCheck
+| "help"          => lake.help
+| cmd             => throw <| CliError.unknownCommand cmd
+
+def lake : CliM PUnit := do
+  match (← getArgs) with
+  | [] => IO.println usage
+  | ["--version"] => IO.println uiVersionString
+  | _ => -- normal CLI
+    processLeadingOptions lakeOption -- between `lake` and command
+    if let some cmd ← takeArg? then
+      processLeadingOptions lakeOption -- between `lake <cmd>` and args
+      if (← getWantsHelp) then
+        IO.println <| help cmd
+      else
+        lakeCli cmd
+    else
+      if (← getWantsHelp) then
+        IO.println usage
+      else
+        throw <| CliError.missingCommand
+
+def cli (args : List String) : BaseIO ExitCode :=
+  (lake).run args

src/lake/Lake/CLI/Serve.lean

@@ -0,0 +1,67 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Load
+import Lake.Build
+import Lake.Util.MainM
+
+namespace Lake
+open Lean (Json toJson fromJson? LeanPaths)
+
+/-- Exit code to return if `print-paths` cannot find the config file. -/
+def noConfigFileCode : ExitCode := 2
+
+/--
+Environment variable that is set when `lake serve` cannot parse the Lake configuration file
+and falls back to plain `lean --server`.
+-/
+def invalidConfigEnvVar := "LAKE_INVALID_CONFIG"
+
+/--
+Build a list of imports of the package
+and print the `.olean` and source directories of every used package.
+If no configuration file exists, exit silently with `noConfigFileCode` (i.e, 2).
+
+The `print-paths` command is used internally by Lean 4 server.
+-/
+def printPaths (config : LoadConfig) (imports : List String := [])
+(oldMode : Bool := false) (verbosity : Verbosity := .normal) : MainM PUnit := do
+  let configFile := config.rootDir / config.configFile
+  if (← configFile.pathExists) then
+    if let some errLog := (← IO.getEnv invalidConfigEnvVar) then
+      IO.eprint errLog
+      IO.eprintln s!"Invalid Lake configuration.  Please restart the server after fixing the Lake configuration file."
+      exit 1
+    let ws ← MainM.runLogIO (loadWorkspace config) verbosity
+    let dynlibs ← ws.runBuild (buildImportsAndDeps imports) oldMode
+      |>.run (MonadLog.eio verbosity)
+    IO.println <| Json.compress <| toJson {
+      oleanPath := ws.leanPath
+      srcPath := ws.leanSrcPath
+      loadDynlibPaths := dynlibs
+      : LeanPaths
+    }
+  else
+    exit noConfigFileCode
+
+/--
+Start the Lean LSP for the `Workspace` loaded from `config`
+with the given additional `args`.
+-/
+def serve (config : LoadConfig) (args : Array String) : IO UInt32 := do
+  let (extraEnv, moreServerArgs) ← do
+    let (log, ws?) ← loadWorkspace config |>.captureLog
+    IO.eprint log
+    if let some ws := ws? then
+      let ctx := mkLakeContext ws
+      pure (← LakeT.run ctx getAugmentedEnv, ws.root.moreServerArgs)
+    else
+      IO.eprint "warning: package configuration has errors, falling back to plain `lean --server`"
+      pure (config.env.installVars.push (invalidConfigEnvVar, log), #[])
+  (← IO.Process.spawn {
+    cmd := config.env.lean.lean.toString
+    args := #["--server"] ++ moreServerArgs ++ args
+    env := extraEnv
+  }).wait