feat: safe exponentiation

- Adds configuration option `exponentiation.threshold`
- An expression `b^n` where `b` and `n` are literals is not reduced by
  `whnf`, `simp`, and `isDefEq` if `n > exponentiation.threshold`.

Motivation: prevents system from becoming irresponsive.

TODO: improve support in the kernel. It is using a hard-coded limit
for now.

.github/workflows/ci.yml

@@ -470,6 +470,11 @@ jobs:
           prerelease: ${{ !startsWith(github.ref, 'refs/tags/v') || contains(github.ref, '-rc') }}
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+      - name: Update release.lean-lang.org
+        run: |
+          gh workflow -R leanprover/release-index run update-index.yml
+        env:
+          GITHUB_TOKEN: ${{ secrets.RELEASE_INDEX_TOKEN }}
 
   # This job creates nightly releases during the cron job.
   # It is responsible for creating the tag, and automatically generating a changelog.
@@ -512,3 +517,8 @@ jobs:
           repository: ${{ github.repository_owner }}/lean4-nightly
         env:
           GITHUB_TOKEN: ${{ secrets.PUSH_NIGHTLY_TOKEN }}
+      - name: Update release.lean-lang.org
+        run: |
+          gh workflow -R leanprover/release-index run update-index.yml
+        env:
+          GITHUB_TOKEN: ${{ secrets.RELEASE_INDEX_TOKEN }}

RELEASES.md

@@ -8,13 +8,326 @@ This file contains work-in-progress notes for the upcoming release, as well as p
 Please check the [releases](https://github.com/leanprover/lean4/releases) page for the current status
 of each version.
 
-v4.10.0
+v4.11.0
 ----------
 Development in progress.
 
+v4.10.0
+----------
+Release candidate, release notes will be copied from branch `releases/v4.10.0` once completed.
+
 v4.9.0
 ---------- 
-Release candidate, release notes will be copied from branch `releases/v4.9.0` once completed.
+
+### Language features, tactics, and metaprograms
+
+* **Definition transparency**
+  * [#4053](https://github.com/leanprover/lean4/pull/4053) adds the `seal` and `unseal` commands, which make definitions locally be irreducible or semireducible.
+  * [#4061](https://github.com/leanprover/lean4/pull/4061) marks functions defined by well-founded recursion with `@[irreducible]` by default,
+    which should prevent the expensive and often unfruitful unfolding of such definitions (see breaking changes below).
+* **Incrementality**
+  * [#3940](https://github.com/leanprover/lean4/pull/3940) extends incremental elaboration into various steps inside of declarations:
+    definition headers, bodies, and tactics.
+    ![Recording 2024-05-10](https://github.com/leanprover/lean4/assets/109126/c9d67b6f-c131-4bc3-a0de-7d63eaf1bfc9).
+  * [250994](https://github.com/leanprover/lean4/commit/250994166ce036ab8644e459129f51ea79c1c2d2)
+    and [67338b](https://github.com/leanprover/lean4/commit/67338bac2333fa39a8656e8f90574784e4c23d3d)
+    add `@[incremental]` attribute to mark an elaborator as supporting incremental elaboration.
+  * [#4259](https://github.com/leanprover/lean4/pull/4259) improves resilience by ensuring incremental commands and tactics are reached only in supported ways.
+  * [#4268](https://github.com/leanprover/lean4/pull/4268) adds special handling for `:= by` so that stray tokens in tactic blocks do not inhibit incrementality.
+  * [#4308](https://github.com/leanprover/lean4/pull/4308) adds incremental `have` tactic.
+  * [#4340](https://github.com/leanprover/lean4/pull/4340) fixes incorrect info tree reuse.
+  * [#4364](https://github.com/leanprover/lean4/pull/4364) adds incrementality for careful command macros such as `set_option in theorem`, `theorem foo.bar`, and `lemma`.
+  * [#4395](https://github.com/leanprover/lean4/pull/4395) adds conservative fix for whitespace handling to avoid incremental reuse leading to goals in front of the text cursor being shown.
+  * [#4407](https://github.com/leanprover/lean4/pull/4407) fixes non-incremental commands in macros blocking further incremental reporting.
+  * [#4436](https://github.com/leanprover/lean4/pull/4436) fixes incremental reporting when there are nested tactics in terms.
+* **Functional induction**
+  * [#4135](https://github.com/leanprover/lean4/pull/4135) ensures that the names used for functional induction are reserved.
+  * [#4327](https://github.com/leanprover/lean4/pull/4327) adds support for structural recursion on reflexive types.
+    For example,
+    ```lean4
+    inductive Many (α : Type u) where
+      | none : Many α
+      | more : α → (Unit → Many α) → Many α
+
+    def Many.map {α β : Type u} (f : α → β) : Many α → Many β
+      | .none => .none
+      | .more x xs => .more (f x) (fun _ => (xs ()).map f)
+
+    #check Many.map.induct
+    /-
+    Many.map.induct {α β : Type u} (f : α → β) (motive : Many α → Prop)
+      (case1 : motive Many.none)
+      (case2 : ∀ (x : α) (xs : Unit → Many α), motive (xs ()) → motive (Many.more x xs)) :
+      ∀ (a : Many α), motive a
+    -/
+    ```
+* [#3903](https://github.com/leanprover/lean4/pull/3903) makes the Lean frontend normalize all line endings to LF before processing.
+  This lets Lean be insensitive to CRLF vs LF line endings, improving the cross-platform experience and making Lake hashes be faithful to what Lean processes.
+* [#4130](https://github.com/leanprover/lean4/pull/4130) makes the tactic framework be able to recover from runtime errors (for example, deterministic timeouts or maximum recursion depth errors).
+* `split` tactic
+  * [#4211](https://github.com/leanprover/lean4/pull/4211) fixes `split at h` when `h` has forward dependencies.
+  * [#4349](https://github.com/leanprover/lean4/pull/4349) allows `split` for `if`-expressions to work on non-propositional goals.
+* `apply` tactic
+  * [#3929](https://github.com/leanprover/lean4/pull/3929) makes error message for `apply` show implicit arguments in unification errors as needed.
+    Modifies `MessageData` type (see breaking changes below).
+* `cases` tactic
+  * [#4224](https://github.com/leanprover/lean4/pull/4224) adds support for unification of offsets such as `x + 20000 = 20001` in `cases` tactic.
+* `omega` tactic
+  * [#4073](https://github.com/leanprover/lean4/pull/4073) lets `omega` fall back to using classical `Decidable` instances when setting up contradiction proofs.
+  * [#4141](https://github.com/leanprover/lean4/pull/4141) and [#4184](https://github.com/leanprover/lean4/pull/4184) fix bugs.
+  * [#4264](https://github.com/leanprover/lean4/pull/4264) improves `omega` error message if no facts found in local context.
+  * [#4358](https://github.com/leanprover/lean4/pull/4358) improves expression matching in `omega` by using `match_expr`.
+* `simp` tactic
+  * [#4176](https://github.com/leanprover/lean4/pull/4176) makes names of erased lemmas clickable.
+  * [#4208](https://github.com/leanprover/lean4/pull/4208) adds a pretty printer for discrimination tree keys.
+  * [#4202](https://github.com/leanprover/lean4/pull/4202) adds `Simp.Config.index` configuration option,
+    which controls whether to use the full discrimination tree when selecting candidate simp lemmas.
+    When `index := false`, only the head function is taken into account, like in Lean 3.
+    This feature can help users diagnose tricky simp failures or issues in code from libraries
+    developed using Lean 3 and then ported to Lean 4.
+    
+    In the following example, it will report that `foo` is a problematic theorem.
+    ```lean
+    opaque f : Nat → Nat → Nat
+
+    @[simp] theorem foo : f x (x, y).2 = y := by sorry
+
+    example : f a b ≤ b := by
+      set_option diagnostics true in
+      simp (config := { index := false })
+    /-
+    [simp] theorems with bad keys
+      foo, key: f _ (@Prod.mk ℕ ℕ _ _).2
+    -/
+    ```
+    With the information above, users can annotate theorems such as `foo` using `no_index` for problematic subterms. Example:
+    ```lean
+    opaque f : Nat → Nat → Nat
+
+    @[simp] theorem foo : f x (no_index (x, y).2) = y := by sorry
+    
+    example : f a b ≤ b := by
+      simp -- `foo` is still applied with `index := true`
+    ```
+  * [#4274](https://github.com/leanprover/lean4/pull/4274) prevents internal `match` equational theorems from appearing in simp trace.
+  * [#4177](https://github.com/leanprover/lean4/pull/4177) and [#4359](https://github.com/leanprover/lean4/pull/4359) make `simp` continue even if a simp lemma does not elaborate, if the tactic state is in recovery mode.
+  * [#4341](https://github.com/leanprover/lean4/pull/4341) fixes panic when applying `@[simp]` to malformed theorem syntax.
+  * [#4345](https://github.com/leanprover/lean4/pull/4345) fixes `simp` so that it does not use the forward version of a user-specified backward theorem.
+  * [#4352](https://github.com/leanprover/lean4/pull/4352) adds missing `dsimp` simplifications for fixed parameters of generated congruence theorems.
+  * [#4362](https://github.com/leanprover/lean4/pull/4362) improves trace messages for `simp` so that constants are hoverable.
+* **Elaboration**
+  * [#4046](https://github.com/leanprover/lean4/pull/4046) makes subst notation (`he ▸ h`) try rewriting in both directions even when there is no expected type available.
+  * [#3328](https://github.com/leanprover/lean4/pull/3328) adds support for identifiers in autoparams (for example, `rfl` in `(h : x = y := by exact rfl)`).
+  * [#4096](https://github.com/leanprover/lean4/pull/4096) changes how the type in `let` and `have` is elaborated, requiring that any tactics in the type be evaluated before proceeding, improving performance.
+  * [#4215](https://github.com/leanprover/lean4/pull/4215) ensures the expression tree elaborator commits to the computed "max type" for the entire arithmetic expression.
+  * [#4267](https://github.com/leanprover/lean4/pull/4267) cases signature elaboration errors to show even if there are parse errors in the body.
+  * [#4368](https://github.com/leanprover/lean4/pull/4368) improves error messages when numeric literals fail to synthesize an `OfNat` instance,
+    including special messages warning when the expected type of the numeral can be a proposition.
+* **Metaprogramming**
+  * [#4167](https://github.com/leanprover/lean4/pull/4167) adds `Lean.MVarId.revertAll` to revert all free variables.
+  * [#4169](https://github.com/leanprover/lean4/pull/4169) adds `Lean.MVarId.ensureNoMVar` to ensure the goal's target contains no expression metavariables.
+  * [#4180](https://github.com/leanprover/lean4/pull/4180) adds `cleanupAnnotations` parameter to `forallTelescope` methods.
+  * [#4307](https://github.com/leanprover/lean4/pull/4307) adds support for parser aliases in syntax quotations.
+* Work toward implementing `grind` tactic
+  * [0a515e](https://github.com/leanprover/lean4/commit/0a515e2ec939519dafb4b99daa81d6bf3c411404)
+    and [#4164](https://github.com/leanprover/lean4/pull/4164)
+    add `grind_norm` and `grind_norm_proc` attributes and `@[grind_norm]` theorems.
+  * [#4170](https://github.com/leanprover/lean4/pull/4170), [#4221](https://github.com/leanprover/lean4/pull/4221),
+    and [#4249](https://github.com/leanprover/lean4/pull/4249) create `grind` preprocessor and core module.
+  * [#4235](https://github.com/leanprover/lean4/pull/4235) and [d6709e](https://github.com/leanprover/lean4/commit/d6709eb1576c5d40fc80462637dc041f970e4d9f)
+    add special `cases` tactic to `grind` along with `@[grind_cases]` attribute to mark types that this `cases` tactic should automatically apply to.
+  * [#4243](https://github.com/leanprover/lean4/pull/4243) adds special `injection?` tactic to `grind`.
+* **Other fixes or improvements**
+  * [#4065](https://github.com/leanprover/lean4/pull/4065) fixes a bug in the `Nat.reduceLeDiff` simproc.
+  * [#3969](https://github.com/leanprover/lean4/pull/3969) makes deprecation warnings activate even for generalized field notation ("dot notation").
+  * [#4132](https://github.com/leanprover/lean4/pull/4132) fixes the `sorry` term so that it does not activate the implicit lambda feature
+  * [9803c5](https://github.com/leanprover/lean4/commit/9803c5dd63dc993628287d5f998525e74af03839)
+    and [47c8e3](https://github.com/leanprover/lean4/commit/47c8e340d65b01f4d9f011686e3dda0d4bb30a20)
+    move `cdot` and `calc` parsers to `Lean` namespace.
+  * [#4252](https://github.com/leanprover/lean4/pull/4252) fixes the `case` tactic so that it is usable in macros by having it erase macro scopes from the tag.
+  * [26b671](https://github.com/leanprover/lean4/commit/26b67184222e75529e1b166db050aaebee323d2d)
+    and [cc33c3](https://github.com/leanprover/lean4/commit/cc33c39cb022d8a3166b1e89677c78835ead1fc7)
+    extract `haveId` syntax.
+  * [#4335](https://github.com/leanprover/lean4/pull/4335) fixes bugs in partial `calc` tactic when there is mdata or metavariables.
+  * [#4329](https://github.com/leanprover/lean4/pull/4329) makes `termination_by?` report unused each unused parameter as `_`.
+* **Docs:** [#4238](https://github.com/leanprover/lean4/pull/4238), [#4294](https://github.com/leanprover/lean4/pull/4294),
+  [#4338](https://github.com/leanprover/lean4/pull/4338).
+
+### Language server, widgets, and IDE extensions
+* [#4066](https://github.com/leanprover/lean4/pull/4066) fixes features like "Find References" when browsing core Lean sources.
+* [#4254](https://github.com/leanprover/lean4/pull/4254) allows embedding user widgets in structured messages.
+  Companion PR is [vscode-lean4#449](https://github.com/leanprover/vscode-lean4/pull/449).
+* [#4445](https://github.com/leanprover/lean4/pull/4445) makes watchdog more resilient against badly behaving clients.
+
+### Library
+* [#4059](https://github.com/leanprover/lean4/pull/4059) upstreams many `List` and `Array` operations and theorems from Batteries.
+* [#4055](https://github.com/leanprover/lean4/pull/4055) removes the unused `Inhabited` instance for `Subtype`.
+* [#3967](https://github.com/leanprover/lean4/pull/3967) adds dates in existing `@[deprecated]` attributes.
+* [#4231](https://github.com/leanprover/lean4/pull/4231) adds boilerplate `Char`, `UInt`, and `Fin` theorems.
+* [#4205](https://github.com/leanprover/lean4/pull/4205) fixes the `MonadStore` type classes to use `semiOutParam`.
+* [#4350](https://github.com/leanprover/lean4/pull/4350) renames `IsLawfulSingleton` to `LawfulSingleton`.
+* `Nat`
+  * [#4094](https://github.com/leanprover/lean4/pull/4094) swaps `Nat.zero_or` and `Nat.or_zero`.
+  * [#4098](https://github.com/leanprover/lean4/pull/4098) and [#4145](https://github.com/leanprover/lean4/pull/4145)
+    change the definition of `Nat.mod` so that `n % (m + n)` reduces when `n` is literal without relying on well-founded recursion,
+    which becomes irreducible by default in [#4061](https://github.com/leanprover/lean4/pull/4061).
+  * [#4188](https://github.com/leanprover/lean4/pull/4188) redefines `Nat.testBit` to be more performant.
+  * Theorems: [#4199](https://github.com/leanprover/lean4/pull/4199).
+* `Array`
+  * [#4074](https://github.com/leanprover/lean4/pull/4074) improves the functional induction principle `Array.feraseIdx.induct`.
+* `List`
+  * [#4172](https://github.com/leanprover/lean4/pull/4172) removes `@[simp]` from `List.length_pos`.
+* `Option`
+  * [#4037](https://github.com/leanprover/lean4/pull/4037) adds theorems to simplify `Option`-valued dependent if-then-else.
+  * [#4314](https://github.com/leanprover/lean4/pull/4314) removes `@[simp]` from `Option.bind_eq_some`.
+* `BitVec`
+  * Theorems: [#3920](https://github.com/leanprover/lean4/pull/3920), [#4095](https://github.com/leanprover/lean4/pull/4095),
+    [#4075](https://github.com/leanprover/lean4/pull/4075), [#4148](https://github.com/leanprover/lean4/pull/4148),
+    [#4165](https://github.com/leanprover/lean4/pull/4165), [#4178](https://github.com/leanprover/lean4/pull/4178),
+    [#4200](https://github.com/leanprover/lean4/pull/4200), [#4201](https://github.com/leanprover/lean4/pull/4201),
+    [#4298](https://github.com/leanprover/lean4/pull/4298), [#4299](https://github.com/leanprover/lean4/pull/4299),
+    [#4257](https://github.com/leanprover/lean4/pull/4257), [#4179](https://github.com/leanprover/lean4/pull/4179),
+    [#4321](https://github.com/leanprover/lean4/pull/4321), [#4187](https://github.com/leanprover/lean4/pull/4187).
+  * [#4193](https://github.com/leanprover/lean4/pull/4193) adds simprocs for reducing `x >>> i` and `x <<< i` where `i` is a bitvector literal.
+  * [#4194](https://github.com/leanprover/lean4/pull/4194) adds simprocs for reducing `(x <<< i) <<< j` and `(x >>> i) >>> j` where `i` and `j` are natural number literals.
+  * [#4229](https://github.com/leanprover/lean4/pull/4229) redefines `rotateLeft`/`rotateRight` to use modulo reduction of shift offset.
+  * [0d3051](https://github.com/leanprover/lean4/commit/0d30517dca094a07bcb462252f718e713b93ffba) makes `<num>#<term>` bitvector literal notation global.
+* `Char`/`String`
+  * [#4143](https://github.com/leanprover/lean4/pull/4143) modifies `String.substrEq` to avoid linter warnings in downstream code.
+  * [#4233](https://github.com/leanprover/lean4/pull/4233) adds simprocs for `Char` and `String` inequalities.
+  * [#4348](https://github.com/leanprover/lean4/pull/4348) upstreams Mathlib lemmas.
+  * [#4354](https://github.com/leanprover/lean4/pull/4354) upstreams basic `String` lemmas.
+* `HashMap`
+  * [#4248](https://github.com/leanprover/lean4/pull/4248) fixes implicitness of typeclass arguments in `HashMap.ofList`.
+* `IO`
+  * [#4036](https://github.com/leanprover/lean4/pull/4036) adds `IO.Process.getCurrentDir` and `IO.Process.setCurrentDir` for adjusting the current process's working directory.
+* **Cleanup:** [#4077](https://github.com/leanprover/lean4/pull/4077), [#4189](https://github.com/leanprover/lean4/pull/4189),
+  [#4304](https://github.com/leanprover/lean4/pull/4304).
+* **Docs:** [#4001](https://github.com/leanprover/lean4/pull/4001), [#4166](https://github.com/leanprover/lean4/pull/4166),
+  [#4332](https://github.com/leanprover/lean4/pull/4332).
+
+### Lean internals
+* **Defeq and WHNF algorithms**
+  * [#4029](https://github.com/leanprover/lean4/pull/4029) remove unnecessary `checkpointDefEq`
+  * [#4206](https://github.com/leanprover/lean4/pull/4206) fixes `isReadOnlyOrSyntheticOpaque` to respect metavariable depth.
+  * [#4217](https://github.com/leanprover/lean4/pull/4217) fixes missing occurs check for delayed assignments.
+* **Definition transparency**
+  * [#4052](https://github.com/leanprover/lean4/pull/4052) adds validation to application of `@[reducible]`/`@[semireducible]`/`@[irreducible]` attributes (with `local`/`scoped` modifiers as well).
+    Setting `set_option allowUnsafeReductibility true` turns this validation off.
+* **Inductive types**
+  * [#3591](https://github.com/leanprover/lean4/pull/3591) fixes a bug where indices could be incorrectly promoted to parameters.
+  * [#3398](https://github.com/leanprover/lean4/pull/3398) fixes a bug in the injectivity theorem generator.
+  * [#4342](https://github.com/leanprover/lean4/pull/4342) fixes elaboration of mutual inductives with instance parameters.
+* **Diagnostics and profiling**
+  * [#3986](https://github.com/leanprover/lean4/pull/3986) adds option `trace.profiler.useHeartbeats` to switch `trace.profiler.threshold` to being in terms of heartbeats instead of milliseconds.
+  * [#4082](https://github.com/leanprover/lean4/pull/4082) makes `set_option diagnostics true` report kernel diagnostic information.
+* **Typeclass resolution**
+  * [#4119](https://github.com/leanprover/lean4/pull/4119) fixes multiple issues with TC caching interacting with `synthPendingDepth`, adds `maxSynthPendingDepth` option with default value `1`.
+  * [#4210](https://github.com/leanprover/lean4/pull/4210) ensures local instance cache does not contain multiple copies of the same instance.
+  * [#4216](https://github.com/leanprover/lean4/pull/4216) fix handling of metavariables, to avoid needing to set the option `backward.synthInstance.canonInstances` to `false`.
+* **Other fixes or improvements**
+  * [#4080](https://github.com/leanprover/lean4/pull/4080) fixes propagation of state for `Lean.Elab.Command.liftCoreM` and `Lean.Elab.Command.liftTermElabM`.
+  * [#3944](https://github.com/leanprover/lean4/pull/3944) makes the `Repr` deriving handler be consistent between `structure` and `inductive` for how types and proofs are erased.
+  * [#4113](https://github.com/leanprover/lean4/pull/4113) propagates `maxHeartbeats` to kernel to control "(kernel) deterministic timeout" error.
+  * [#4125](https://github.com/leanprover/lean4/pull/4125) reverts [#3970](https://github.com/leanprover/lean4/pull/3970) (monadic generalization of `FindExpr`).
+  * [#4128](https://github.com/leanprover/lean4/pull/4128) catches stack overflow in auto-bound implicits feature.
+  * [#4129](https://github.com/leanprover/lean4/pull/4129) adds `tryCatchRuntimeEx` combinator to replace `catchRuntimeEx` reader state.
+  * [#4155](https://github.com/leanprover/lean4/pull/4155) simplifies the expression canonicalizer.
+  * [#4151](https://github.com/leanprover/lean4/pull/4151) and [#4369](https://github.com/leanprover/lean4/pull/4369)
+    add many missing trace classes.
+  * [#4185](https://github.com/leanprover/lean4/pull/4185) makes congruence theorem generators clean up type annotations of argument types.
+  * [#4192](https://github.com/leanprover/lean4/pull/4192) fixes restoration of infotrees when auto-bound implicit feature is activated,
+    fixing a pretty printing error in hovers and strengthening the unused variable linter.
+  * [dfb496](https://github.com/leanprover/lean4/commit/dfb496a27123c3864571aec72f6278e2dad1cecf) fixes `declareBuiltin` to allow it to be called multiple times per declaration.
+  * Cleanup: [#4112](https://github.com/leanprover/lean4/pull/4112), [#4126](https://github.com/leanprover/lean4/pull/4126), [#4091](https://github.com/leanprover/lean4/pull/4091), [#4139](https://github.com/leanprover/lean4/pull/4139), [#4153](https://github.com/leanprover/lean4/pull/4153).
+  * Tests: [030406](https://github.com/leanprover/lean4/commit/03040618b8f9b35b7b757858483e57340900cdc4), [#4133](https://github.com/leanprover/lean4/pull/4133).
+
+### Compiler, runtime, and FFI
+* [#4100](https://github.com/leanprover/lean4/pull/4100) improves reset/reuse algorithm; it now runs a second pass relaxing the constraint that reused memory cells must only be for the exact same constructor.
+* [#2903](https://github.com/leanprover/lean4/pull/2903) fixes segfault in old compiler from mishandling `noConfusion` applications.
+* [#4311](https://github.com/leanprover/lean4/pull/4311) fixes bug in constant folding.
+* [#3915](https://github.com/leanprover/lean4/pull/3915) documents the runtime memory layout for inductive types.
+
+### Lake
+* [#4057](https://github.com/leanprover/lean4/pull/4057) adds support for docstrings on `require` commands.
+* [#4088](https://github.com/leanprover/lean4/pull/4088) improves hovers for `family_def` and `library_data` commands.
+* [#4147](https://github.com/leanprover/lean4/pull/4147) adds default `README.md` to package templates
+* [#4261](https://github.com/leanprover/lean4/pull/4261) extends `lake test` help page, adds help page for `lake check-test`,
+  adds `lake lint` and tag `@[lint_driver]`, adds support for specifying test and lint drivers from dependencies,
+  adds `testDriverArgs` and `lintDriverArgs` options, adds support for library test drivers,
+  makes `lake check-test` and `lake check-lint` only load the package without dependencies.
+* [#4270](https://github.com/leanprover/lean4/pull/4270) adds `lake pack` and `lake unpack` for packing and unpacking Lake build artifacts from an archive.
+* [#4083](https://github.com/leanprover/lean4/pull/4083)
+  Switches the manifest format to use `major.minor.patch` semantic
+  versions. Major version increments indicate breaking changes (e.g., new
+  required fields and semantic changes to existing fields). Minor version
+  increments (after `0.x`) indicate backwards-compatible extensions (e.g.,
+  adding optional fields, removing fields). This change is backwards
+  compatible. Lake will still successfully read old manifests with numeric
+  versions. It will treat the numeric version `N` as semantic version
+  `0.N.0`. Lake will also accept manifest versions with `-` suffixes
+  (e.g., `x.y.z-foo`) and then ignore the suffix.
+* [#4273](https://github.com/leanprover/lean4/pull/4273) adds a lift from `JobM` to `FetchM` for backwards compatibility reasons.
+* [#4351](https://github.com/leanprover/lean4/pull/4351) fixes `LogIO`-to-`CliM`-lifting performance issues.
+* [#4343](https://github.com/leanprover/lean4/pull/4343) make Lake store the dependency trace for a build in
+  the cached build long and then verifies that it matches the trace of the current build before replaying the log.
+* [#4402](https://github.com/leanprover/lean4/pull/4402) moves the cached log into the trace file (no more `.log.json`).
+  This means logs are no longer cached on fatal errors and this ensures that an out-of-date log is not associated with an up-to-date trace.
+  Separately, `.hash` file generation was changed to be more reliable as well.
+  The `.hash` files are deleted as part of the build and always regenerate with `--rehash`.
+* **Other fixes or improvements**
+  * [#4056](https://github.com/leanprover/lean4/pull/4056) cleans up tests
+  * [#4244](https://github.com/leanprover/lean4/pull/4244) fixes `noRelease` test when Lean repo is tagged
+  * [#4346](https://github.com/leanprover/lean4/pull/4346) improves `tests/serve`
+  * [#4356](https://github.com/leanprover/lean4/pull/4356) adds build log path to the warning for a missing or invalid build log.
+
+### DevOps
+* [#3984](https://github.com/leanprover/lean4/pull/3984) adds a script (`script/rebase-stage0.sh`) for `git rebase -i` that automatically updates each stage0.
+* [#4108](https://github.com/leanprover/lean4/pull/4108) finishes renamings from transition to Std to Batteries.
+* [#4109](https://github.com/leanprover/lean4/pull/4109) adjusts the Github bug template to mention testing using [live.lean-lang.org](https://live.lean-lang.org).
+* [#4136](https://github.com/leanprover/lean4/pull/4136) makes CI rerun only when `full-ci` label is added or removed.
+* [#4175](https://github.com/leanprover/lean4/pull/4175) and [72b345](https://github.com/leanprover/lean4/commit/72b345c621a9a06d3a5a656da2b793a5eea5f168)
+  switch to using `#guard_msgs` to run tests as much as possible.
+* [#3125](https://github.com/leanprover/lean4/pull/3125) explains the Lean4 `pygments` lexer.
+* [#4247](https://github.com/leanprover/lean4/pull/4247) sets up a procedure for preparing release notes.
+* [#4032](https://github.com/leanprover/lean4/pull/4032) modernizes build instructions and workflows.
+* [#4255](https://github.com/leanprover/lean4/pull/4255) moves some expensive checks from merge queue to releases.
+* [#4265](https://github.com/leanprover/lean4/pull/4265) adds aarch64 macOS as native compilation target for CI.
+* [f05a82](https://github.com/leanprover/lean4/commit/f05a82799a01569edeb5e2594cd7d56282320f9e) restores macOS aarch64 install suffix in CI
+* [#4317](https://github.com/leanprover/lean4/pull/4317) updates build instructions for macOS.
+* [#4333](https://github.com/leanprover/lean4/pull/4333) adjusts workflow to update Batteries in manifest when creating `lean-pr-testing-NNNN` Mathlib branches.
+* [#4355](https://github.com/leanprover/lean4/pull/4355) simplifies `lean4checker` step of release checklist.
+* [#4361](https://github.com/leanprover/lean4/pull/4361) adds installing elan to `pr-release` CI step.
+
+### Breaking changes
+While most changes could be considered to be a breaking change, this section makes special note of API changes.
+
+* `Nat.zero_or` and `Nat.or_zero` have been swapped ([#4094](https://github.com/leanprover/lean4/pull/4094)).
+* `IsLawfulSingleton` is now `LawfulSingleton` ([#4350](https://github.com/leanprover/lean4/pull/4350)).
+* `BitVec.rotateLeft` and `BitVec.rotateRight` now take the shift modulo the bitwidth ([#4229](https://github.com/leanprover/lean4/pull/4229)).
+* These are no longer simp lemmas:
+  `List.length_pos` ([#4172](https://github.com/leanprover/lean4/pull/4172)),
+  `Option.bind_eq_some` ([#4314](https://github.com/leanprover/lean4/pull/4314)).
+* Types in `let` and `have` (both the expressions and tactics) may fail to elaborate due to new restrictions on what sorts of elaboration problems may be postponed ([#4096](https://github.com/leanprover/lean4/pull/4096)).
+  In particular, tactics embedded in the type will no longer make use of the type of `value` in expressions such as `let x : type := value; body`.
+* Now functions defined by well-founded recursion are marked with `@[irreducible]` by default ([#4061](https://github.com/leanprover/lean4/pull/4061)).
+  Existing proofs that hold by definitional equality (e.g. `rfl`) can be
+  rewritten to explictly unfold the function definition (using `simp`,
+  `unfold`, `rw`), or the recursive function can be temporarily made
+  semireducible (using `unseal f in` before the command), or the function
+  definition itself can be marked as `@[semireducible]` to get the previous
+  behavior.
+* Due to [#3929](https://github.com/leanprover/lean4/pull/3929):
+  * The `MessageData.ofPPFormat` constructor has been removed.
+    Its functionality has been split into two:
+
+    - for lazy structured messages, please use `MessageData.lazy`;
+    - for embedding `Format` or `FormatWithInfos`, use `MessageData.ofFormatWithInfos`.
+
+    An example migration can be found in [#3929](https://github.com/leanprover/lean4/pull/3929/files#diff-5910592ab7452a0e1b2616c62d22202d2291a9ebb463145f198685aed6299867L109).
+
+  * The `MessageData.ofFormat` constructor has been turned into a function.
+    If you need to inspect `MessageData`, you can pattern-match on `MessageData.ofFormatWithInfos`.
 
 v4.8.0
 ---------

doc/dev/release_checklist.md

@@ -13,13 +13,11 @@ We'll use `v4.6.0` as the intended release version as a running example.
   - `set(LEAN_VERSION_MINOR 6)` (for whichever `6` is appropriate)
   - `set(LEAN_VERSION_IS_RELEASE 1)`
   - (both of these should already be in place from the release candidates)
-- It is possible that the `v4.6.0` section of `RELEASES.md` is out of sync between
-  `releases/v4.6.0` and `master`. This should be reconciled:
-  - Run `git diff master RELEASES.md`.
-  - You should expect to see additons on `master` in the `v4.7.0-rc1` section; ignore these.
-    (i.e. the new release notes for the upcoming release candidate).
-  - Reconcile discrepancies in the `v4.6.0` section,
-    usually via copy and paste and a commit to `releases/v4.6.0`.
+- In `RELEASES.md`, verify that the `v4.6.0` section has been completed during the release candidate cycle.
+  It should be in bullet point form, with a point for every significant PR,
+  and may have a paragraph describing each major new language feature.
+  It should have a "breaking changes" section calling out changes that are specifically likely
+  to cause problems for downstream users.
 - `git tag v4.6.0`
 - `git push $REMOTE v4.6.0`, where `$REMOTE` is the upstream Lean repository (e.g., `origin`, `upstream`)
 - Now wait, while CI runs.
@@ -189,8 +187,12 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
   Please also make sure that whoever is handling social media knows the release is out.
 - Begin the next development cycle (i.e. for `v4.8.0`) on the Lean repository, by making a PR that:
   - Updates `src/CMakeLists.txt` to say `set(LEAN_VERSION_MINOR 8)`
-  - Removes `(in development)` from the section heading in `RELEASES.md` for `v4.7.0`,
-    and creates a new `v4.8.0 (in development)` section heading.
+  - In `RELEASES.md`, update the `v4.7.0` section to say:
+    "Release candidate, release notes will be copied from branch `releases/v4.7.0` once completed."
+    Make sure that whoever is preparing the release notes during this cycle knows that it is their job to do so!
+  - In `RELEASES.md`, update the `v4.8.0` section to say:
+    "Development in progress".
+  - In `RELEASES.md`, verify that the old section `v4.6.0` has the full releases notes from the `releases/v4.6.0` branch.
 
 ## Time estimates:
 Slightly longer than the corresponding steps for a stable release.

nix/bootstrap.nix

@@ -125,8 +125,10 @@ rec {
       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"} \
-          ${if stdenv.isDarwin then "-Wl,-force_load,${Init.staticLib}/libInit.a -Wl,-force_load,${Lean.staticLib}/libStd.a -Wl,-force_load,${Lean.staticLib}/libLean.a -Wl,-force_load,${leancpp}/lib/lean/libleancpp.a ${leancpp}/lib/libleanrt_initial-exec.a -lc++"
-            else "-Wl,--whole-archive -lInit -lStd -lLean -lleancpp ${leancpp}/lib/libleanrt_initial-exec.a -Wl,--no-whole-archive -lstdc++"} -lm ${stdlibLinkFlags} \
+          ${if stdenv.isDarwin
+            then "-Wl,-force_load,${Init.staticLib}/libInit.a -Wl,-force_load,${Std.staticLib}/libStd.a -Wl,-force_load,${Lean.staticLib}/libLean.a -Wl,-force_load,${leancpp}/lib/lean/libleancpp.a ${leancpp}/lib/libleanrt_initial-exec.a -lc++"
+            else "-Wl,--whole-archive -lInit -lStd -lLean -lleancpp ${leancpp}/lib/libleanrt_initial-exec.a -Wl,--no-whole-archive -lstdc++"} \
+          -lm ${stdlibLinkFlags} \
           $(${llvmPackages.libllvm.dev}/bin/llvm-config --ldflags --libs) \
           -o $out/$libName
       '';

nix/buildLeanPackage.nix

@@ -224,7 +224,8 @@ with builtins; let
   allLinkFlags = lib.foldr (shared: acc: acc ++ [ "-L${shared}" "-l${shared.linkName or shared.name}" ]) linkFlags allNativeSharedLibs;
 
   objects   = mapAttrs (_: m: m.obj) mods';
-  staticLib = runCommand "${name}-lib" { buildInputs = [ stdenv.cc.bintools.bintools ]; } ''
+  bintools = if stdenv.isDarwin then darwin.cctools else stdenv.cc.bintools.bintools;
+  staticLib = runCommand "${name}-lib" { buildInputs = [ bintools ]; } ''
     mkdir -p $out
     ar Trcs $out/lib${libName}.a ${lib.concatStringsSep " " (map (drv: "${drv}/${drv.oPath}") (attrValues objects))};
   '';

src/CMakeLists.txt

@@ -9,7 +9,7 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
-set(LEAN_VERSION_MINOR 10)
+set(LEAN_VERSION_MINOR 11)
 set(LEAN_VERSION_PATCH 0)
 set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")

src/Init/Data/Array.lean

@@ -10,5 +10,6 @@ import Init.Data.Array.BinSearch
 import Init.Data.Array.InsertionSort
 import Init.Data.Array.DecidableEq
 import Init.Data.Array.Mem
+import Init.Data.Array.Attach
 import Init.Data.Array.BasicAux
 import Init.Data.Array.Lemmas

src/Init/Data/Array/Attach.lean

@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2021 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner, Mario Carneiro
+-/
+prelude
+import Init.Data.Array.Mem
+import Init.Data.List.Attach
+
+namespace Array
+
+/--
+Unsafe implementation of `attachWith`, taking advantage of the fact that the representation of
+`Array {x // P x}` is the same as the input `Array α`.
+-/
+@[inline] private unsafe def attachWithImpl
+    (xs : Array α) (P : α → Prop) (_ : ∀ x ∈ xs, P x) : Array {x // P x} := unsafeCast xs
+
+/-- `O(1)`. "Attach" a proof `P x` that holds for all the elements of `xs` to produce a new array
+  with the same elements but in the type `{x // P x}`. -/
+@[implemented_by attachWithImpl] def attachWith
+    (xs : Array α) (P : α → Prop) (H : ∀ x ∈ xs, P x) : Array {x // P x} :=
+  ⟨xs.data.attachWith P fun x h => H x (Array.Mem.mk h)⟩
+
+/-- `O(1)`. "Attach" the proof that the elements of `xs` are in `xs` to produce a new array
+  with the same elements but in the type `{x // x ∈ xs}`. -/
+@[inline] def attach (xs : Array α) : Array {x // x ∈ xs} := xs.attachWith _ fun _ => id
+
+end Array

src/Init/Data/Array/Basic.lean

@@ -60,8 +60,6 @@ def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
 instance : GetElem (Array α) USize α fun xs i => i.toNat < xs.size where
   getElem xs i h := xs.uget i h
 
-instance : LawfulGetElem (Array α) USize α fun xs i => i.toNat < xs.size where
-
 def back [Inhabited α] (a : Array α) : α :=
   a.get! (a.size - 1)
 

src/Init/Data/Array/Lemmas.lean

@@ -220,7 +220,7 @@ theorem getElem?_len_le (a : Array α) {i : Nat} (h : a.size ≤ i) : a[i]? = no
 theorem getD_get? (a : Array α) (i : Nat) (d : α) :
   Option.getD a[i]? d = if p : i < a.size then a[i]'p else d := by
   if h : i < a.size then
-    simp [setD, h, getElem?]
+    simp [setD, h, getElem?_def]
   else
     have p : i ≥ a.size := Nat.le_of_not_gt h
     simp [setD, getElem?_len_le _ p, h]
@@ -383,18 +383,18 @@ theorem get?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x el
   | Or.inl g =>
     have h1 : i < a.size + 1 := by omega
     have h2 : i ≠ a.size := by omega
-    simp [getElem?, size_push, g, h1, h2, get_push_lt]
+    simp [getElem?_def, size_push, g, h1, h2, get_push_lt]
   | Or.inr (Or.inl heq) =>
     simp [heq, getElem?_pos, get_push_eq]
   | Or.inr (Or.inr g) =>
-    simp only [getElem?, size_push]
+    simp only [getElem?_def, size_push]
     have h1 : ¬ (i < a.size) := by omega
     have h2 : ¬ (i < a.size + 1) := by omega
     have h3 : i ≠ a.size := by omega
     simp [h1, h2, h3]
 
 @[simp] theorem get?_size {a : Array α} : a[a.size]? = none := by
-  simp only [getElem?, Nat.lt_irrefl, dite_false]
+  simp only [getElem?_def, Nat.lt_irrefl, dite_false]
 
 @[simp] theorem data_set (a : Array α) (i v) : (a.set i v).data = a.data.set i.1 v := rfl
 

src/Init/Data/Array/Subarray.lean

@@ -47,8 +47,6 @@ def get (s : Subarray α) (i : Fin s.size) : α :=
 instance : GetElem (Subarray α) Nat α fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
-instance : LawfulGetElem (Subarray α) Nat α fun xs i => i < xs.size where
-
 @[inline] def getD (s : Subarray α) (i : Nat) (v₀ : α) : α :=
   if h : i < s.size then s.get ⟨i, h⟩ else v₀
 

src/Init/Data/BitVec/Lemmas.lean

@@ -1043,8 +1043,16 @@ theorem ofInt_add {n} (x y : Int) : BitVec.ofInt n (x + y) =
 
 theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toNat) := by rfl
 
-@[simp, bv_toNat] theorem toNat_sub {n} (x y : BitVec n) :
-  (x - y).toNat = (((2^n - y.toNat) + x.toNat) % 2^n) := rfl
+@[simp] theorem toNat_sub {n} (x y : BitVec n) :
+    (x - y).toNat = (((2^n - y.toNat) + x.toNat) % 2^n) := rfl
+
+-- We prefer this lemma to `toNat_sub` for the `bv_toNat` simp set.
+-- For reasons we don't yet understand, unfolding via `toNat_sub` sometimes
+-- results in `omega` generating proof terms that are very slow in the kernel.
+@[bv_toNat] theorem toNat_sub' {n} (x y : BitVec n) :
+    (x - y).toNat = ((x.toNat + (2^n - y.toNat)) % 2^n) := by
+  rw [toNat_sub, Nat.add_comm]
+
 @[simp] theorem toFin_sub (x y : BitVec n) : (x - y).toFin = toFin x - toFin y := rfl
 
 @[simp] theorem ofFin_sub (x : Fin (2^n)) (y : BitVec n) : .ofFin x - y = .ofFin (x - y.toFin) :=

src/Init/Data/ByteArray/Basic.lean

@@ -52,13 +52,9 @@ def get : (a : @& ByteArray) → (@& Fin a.size) → UInt8
 instance : GetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
-instance : LawfulGetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
-
 instance : GetElem ByteArray USize UInt8 fun xs i => i.val < xs.size where
   getElem xs i h := xs.uget i h
 
-instance : LawfulGetElem ByteArray USize UInt8 fun xs i => i.val < xs.size where
-
 @[extern "lean_byte_array_set"]
 def set! : ByteArray → (@& Nat) → UInt8 → ByteArray
   | ⟨bs⟩, i, b => ⟨bs.set! i b⟩
@@ -96,20 +92,24 @@ protected def append (a : ByteArray) (b : ByteArray) : ByteArray :=
 
 instance : Append ByteArray := ⟨ByteArray.append⟩
 
-partial def toList (bs : ByteArray) : List UInt8 :=
+def toList (bs : ByteArray) : List UInt8 :=
   let rec loop (i : Nat) (r : List UInt8) :=
     if i < bs.size then
       loop (i+1) (bs.get! i :: r)
     else
       r.reverse
+    termination_by bs.size - i
+    decreasing_by decreasing_trivial_pre_omega
   loop 0 []
 
-@[inline] partial def findIdx? (a : ByteArray) (p : UInt8 → Bool) (start := 0) : Option Nat :=
+@[inline] def findIdx? (a : ByteArray) (p : UInt8 → Bool) (start := 0) : Option Nat :=
   let rec @[specialize] loop (i : Nat) :=
     if i < a.size then
       if p (a.get! i) then some i else loop (i+1)
     else
       none
+    termination_by a.size - i
+    decreasing_by decreasing_trivial_pre_omega
   loop start
 
 /--

src/Init/Data/FloatArray/Basic.lean

@@ -58,13 +58,9 @@ def get? (ds : FloatArray) (i : Nat) : Option Float :=
 instance : GetElem FloatArray Nat Float fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
-instance : LawfulGetElem FloatArray Nat Float fun xs i => i < xs.size where
-
 instance : GetElem FloatArray USize Float fun xs i => i.val < xs.size where
   getElem xs i h := xs.uget i h
 
-instance : LawfulGetElem FloatArray USize Float fun xs i => i.val < xs.size where
-
 @[extern "lean_float_array_uset"]
 def uset : (a : FloatArray) → (i : USize) → Float → i.toNat < a.size → FloatArray
   | ⟨ds⟩, i, v, h => ⟨ds.uset i v h⟩

src/Init/Data/List.lean

@@ -8,6 +8,7 @@ import Init.Data.List.Basic
 import Init.Data.List.BasicAux
 import Init.Data.List.Control
 import Init.Data.List.Lemmas
+import Init.Data.List.Attach
 import Init.Data.List.Impl
 import Init.Data.List.TakeDrop
 import Init.Data.List.Notation

src/Init/Data/List/Attach.lean

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2023 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+prelude
+import Init.Data.List.Lemmas
+
+namespace List
+
+/-- `O(n)`. Partial map. If `f : Π a, P a → β` is a partial function defined on
+  `a : α` satisfying `P`, then `pmap f l h` is essentially the same as `map f l`
+  but is defined only when all members of `l` satisfy `P`, using the proof
+  to apply `f`. -/
+@[simp] def pmap {P : α → Prop} (f : ∀ a, P a → β) : ∀ l : List α, (H : ∀ a ∈ l, P a) → List β
+  | [], _ => []
+  | a :: l, H => f a (forall_mem_cons.1 H).1 :: pmap f l (forall_mem_cons.1 H).2
+
+/--
+Unsafe implementation of `attachWith`, taking advantage of the fact that the representation of
+`List {x // P x}` is the same as the input `List α`.
+(Someday, the compiler might do this optimization automatically, but until then...)
+-/
+@[inline] private unsafe def attachWithImpl
+    (l : List α) (P : α → Prop) (_ : ∀ x ∈ l, P x) : List {x // P x} := unsafeCast l
+
+/-- `O(1)`. "Attach" a proof `P x` that holds for all the elements of `l` to produce a new list
+  with the same elements but in the type `{x // P x}`. -/
+@[implemented_by attachWithImpl] def attachWith
+    (l : List α) (P : α → Prop) (H : ∀ x ∈ l, P x) : List {x // P x} := pmap Subtype.mk l H
+
+/-- `O(1)`. "Attach" the proof that the elements of `l` are in `l` to produce a new list
+  with the same elements but in the type `{x // x ∈ l}`. -/
+@[inline] def attach (l : List α) : List {x // x ∈ l} := attachWith l _ fun _ => id
+
+/-- Implementation of `pmap` using the zero-copy version of `attach`. -/
+@[inline] private def pmapImpl {P : α → Prop} (f : ∀ a, P a → β) (l : List α) (H : ∀ a ∈ l, P a) :
+    List β := (l.attachWith _ H).map fun ⟨x, h'⟩ => f x h'
+
+@[csimp] private theorem pmap_eq_pmapImpl : @pmap = @pmapImpl := by
+  funext α β p f L h'
+  let rec go : ∀ L' (hL' : ∀ ⦃x⦄, x ∈ L' → p x),
+      pmap f L' hL' = map (fun ⟨x, hx⟩ => f x hx) (pmap Subtype.mk L' hL')
+  | nil, hL' => rfl
+  | cons _ L', hL' => congrArg _ <| go L' fun _ hx => hL' (.tail _ hx)
+  exact go L h'

src/Init/Data/List/Lemmas.lean

@@ -154,7 +154,7 @@ theorem get?_eq_none : l.get? n = none ↔ length l ≤ n :=
   ⟨fun e => Nat.ge_of_not_lt (fun h' => by cases e ▸ get?_eq_some.2 ⟨h', rfl⟩), get?_len_le⟩
 
 @[simp] theorem get?_eq_getElem? (l : List α) (i : Nat) : l.get? i = l[i]? := by
-  simp only [getElem?]; split
+  simp only [getElem?, decidableGetElem?]; split
   · exact (get?_eq_get ‹_›)
   · exact (get?_eq_none.2 <| Nat.not_lt.1 ‹_›)
 

src/Init/GetElem.lean

@@ -7,22 +7,57 @@ prelude
 import Init.Util
 
 @[never_extract]
-private def outOfBounds [Inhabited α] : α :=
+def outOfBounds [Inhabited α] : α :=
   panic! "index out of bounds"
 
-/--
-The class `GetElem coll idx elem valid` implements the `xs[i]` notation.
-Given `xs[i]` with `xs : coll` and `i : idx`, Lean looks for an instance of
-`GetElem coll idx elem valid` and uses this to infer the type of return
-value `elem` and side conditions `valid` required to ensure `xs[i]` yields
-a valid value of type `elem`.
+theorem outOfBounds_eq_default [Inhabited α] : (outOfBounds : α) = default := rfl
+
+/--
+The classes `GetElem` and `GetElem?` implement lookup notation,
+specifically `xs[i]`, `xs[i]?`, `xs[i]!`, and `xs[i]'p`.
+
+Both classes are indexed by types `coll`, `idx`, and `elem` which are
+the collection, the index, and the element types.
+A single collection may support lookups with multiple index
+types. The relation `valid` determines when the index is guaranteed to be
+valid; lookups of valid indices are guaranteed not to fail.
+
+For example, an instance for arrays looks like
+`GetElem (Array α) Nat α (fun xs i => i < xs.size)`. In other words, given an
+array `xs` and a natural number `i`, `xs[i]` will return an `α` when `valid xs i`
+holds, which is true when `i` is less than the size of the array. `Array`
+additionally supports indexing with `USize` instead of `Nat`.
+In either case, because the bounds are checked at compile time,
+no runtime check is required.
+
+Given `xs[i]` with `xs : coll` and `i : idx`, Lean looks for an instance of
+`GetElem coll idx elem valid` and uses this to infer the type of the return
+value `elem` and side condition `valid` required to ensure `xs[i]` yields
+a valid value of type `elem`. The tactic `get_elem_tactic` is
+invoked to prove validity automatically. The `xs[i]'p` notation uses the
+proof `p` to satisfy the validity condition.
+If the proof `p` is long, it is often easier to place the
+proof in the context using `have`, because `get_elem_tactic` tries
+`assumption`.
 
-For example, the instance for arrays looks like
-`GetElem (Array α) Nat α (fun xs i => i < xs.size)`.
 
 The proof side-condition `valid xs i` is automatically dispatched by the
-`get_elem_tactic` tactic, which can be extended by adding more clauses to
-`get_elem_tactic_trivial`.
+`get_elem_tactic` tactic; this tactic can be extended by adding more clauses to
+`get_elem_tactic_trivial` using `macro_rules`.
+
+`xs[i]?` and `xs[i]!` do not impose a proof obligation; the former returns
+an `Option elem`, with `none` signalling that the value isn't present, and
+the latter returns `elem` but panics if the value isn't there, returning
+`default : elem` based on the `Inhabited elem` instance.
+These are provided by the `GetElem?` class, for which there is a default instance
+generated from a `GetElem` class as long as `valid xs i` is always decidable.
+
+Important instances include:
+  * `arr[i] : α` where `arr : Array α` and `i : Nat` or `i : USize`: does array
+    indexing with no runtime bounds check and a proof side goal `i < arr.size`.
+  * `l[i] : α` where `l : List α` and `i : Nat`: index into a list, with proof
+    side goal `i < l.length`.
+
 -/
 class GetElem (coll : Type u) (idx : Type v) (elem : outParam (Type w))
               (valid : outParam (coll → idx → Prop)) where
@@ -30,33 +65,10 @@ class GetElem (coll : Type u) (idx : Type v) (elem : outParam (Type w))
   The syntax `arr[i]` gets the `i`'th element of the collection `arr`. If there
   are proof side conditions to the application, they will be automatically
   inferred by the `get_elem_tactic` tactic.
-
-  The actual behavior of this class is type-dependent, but here are some
-  important implementations:
-  * `arr[i] : α` where `arr : Array α` and `i : Nat` or `i : USize`: does array
-    indexing with no bounds check and a proof side goal `i < arr.size`.
-  * `l[i] : α` where `l : List α` and `i : Nat`: index into a list, with proof
-    side goal `i < l.length`.
-  * `stx[i] : Syntax` where `stx : Syntax` and `i : Nat`: get a syntax argument,
-    no side goal (returns `.missing` out of range)
-
-  There are other variations on this syntax:
-  * `arr[i]!` is syntax for `getElem! arr i` which should panic and return
-    `default : α` if the index is not valid.
-  * `arr[i]?` is syntax for `getElem?` which should return `none` if the index
-    is not valid.
-  * `arr[i]'h` is syntax for `getElem arr i h` with `h` an explicit proof the
-    index is valid.
   -/
   getElem (xs : coll) (i : idx) (h : valid xs i) : elem
 
-  getElem? (xs : coll) (i : idx) [Decidable (valid xs i)] : Option elem :=
-    if h : _ then some (getElem xs i h) else none
-
-  getElem! [Inhabited elem] (xs : coll) (i : idx) [Decidable (valid xs i)] : elem :=
-    match getElem? xs i with | some e => e | none => outOfBounds
-
-export GetElem (getElem getElem! getElem?)
+export GetElem (getElem)
 
 @[inherit_doc getElem]
 syntax:max term noWs "[" withoutPosition(term) "]" : term
@@ -66,6 +78,30 @@ macro_rules | `($x[$i]) => `(getElem $x $i (by get_elem_tactic))
 syntax term noWs "[" withoutPosition(term) "]'" term:max : term
 macro_rules | `($x[$i]'$h) => `(getElem $x $i $h)
 
+/-- Helper function for implementation of `GetElem?.getElem?`. -/
+abbrev decidableGetElem? [GetElem coll idx elem valid] (xs : coll) (i : idx) [Decidable (valid xs i)] :
+    Option elem :=
+  if h : valid xs i then some xs[i] else none
+
+@[inherit_doc GetElem]
+class GetElem? (coll : Type u) (idx : Type v) (elem : outParam (Type w))
+    (valid : outParam (coll → idx → Prop)) extends GetElem coll idx elem valid where
+  /--
+  The syntax `arr[i]?` gets the `i`'th element of the collection `arr`,
+  if it is present (and wraps it in `some`), and otherwise returns `none`.
+  -/
+  getElem? : coll → idx → Option elem
+
+  /--
+  The syntax `arr[i]!` gets the `i`'th element of the collection `arr`,
+  if it is present, and otherwise panics at runtime and returns the `default` term
+  from `Inhabited elem`.
+  -/
+  getElem! [Inhabited elem] (xs : coll) (i : idx) : elem :=
+    match getElem? xs i with | some e => e | none => outOfBounds
+
+export GetElem? (getElem? getElem!)
+
 /--
 The syntax `arr[i]?` gets the `i`'th element of the collection `arr` or
 returns `none` if `i` is out of bounds.
@@ -78,32 +114,43 @@ panics `i` is out of bounds.
 -/
 macro:max x:term noWs "[" i:term "]" noWs "!" : term => `(getElem! $x $i)
 
+instance (priority := low) [GetElem coll idx elem valid] [∀ xs i, Decidable (valid xs i)] :
+    GetElem? coll idx elem valid where
+  getElem? xs i := decidableGetElem? xs i
+
 class LawfulGetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w))
-   (dom : outParam (cont → idx → Prop)) [ge : GetElem cont idx elem dom] : Prop where
+   (dom : outParam (cont → idx → Prop)) [ge : GetElem? cont idx elem dom] : Prop where
 
   getElem?_def (c : cont) (i : idx) [Decidable (dom c i)] :
-    c[i]? = if h : dom c i then some (c[i]'h) else none := by intros; eq_refl
-  getElem!_def [Inhabited elem] (c : cont) (i : idx) [Decidable (dom c i)] :
-    c[i]! = match c[i]? with | some e => e | none => default := by intros; eq_refl
+      c[i]? = if h : dom c i then some (c[i]'h) else none := by
+    intros
+    try simp only [getElem?] <;> congr
+  getElem!_def [Inhabited elem] (c : cont) (i : idx) :
+      c[i]! = match c[i]? with | some e => e | none => default := by
+    intros
+    simp only [getElem!, getElem?, outOfBounds_eq_default]
 
 export LawfulGetElem (getElem?_def getElem!_def)
 
-theorem getElem?_pos [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
+instance (priority := low) [GetElem coll idx elem valid] [∀ xs i, Decidable (valid xs i)] :
+    LawfulGetElem coll idx elem valid where
+
+theorem getElem?_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] : c[i]? = some (c[i]'h) := by
   rw [getElem?_def]
   exact dif_pos h
 
-theorem getElem?_neg [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
+theorem getElem?_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]? = none := by
   rw [getElem?_def]
   exact dif_neg h
 
-theorem getElem!_pos [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
+theorem getElem!_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     [Inhabited elem] (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] :
     c[i]! = c[i]'h := by
   simp only [getElem!_def, getElem?_def, h]
 
-theorem getElem!_neg [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
+theorem getElem!_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     [Inhabited elem] (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]! = default := by
   simp only [getElem!_def, getElem?_def, h]
 
@@ -111,22 +158,23 @@ namespace Fin
 
 instance instGetElemFinVal [GetElem cont Nat elem dom] : GetElem cont (Fin n) elem fun xs i => dom xs i where
   getElem xs i h := getElem xs i.1 h
+
+instance instGetElem?FinVal [GetElem? cont Nat elem dom] : GetElem? cont (Fin n) elem fun xs i => dom xs i where
   getElem? xs i := getElem? xs i.val
   getElem! xs i := getElem! xs i.val
 
-instance [GetElem cont Nat elem dom] [h : LawfulGetElem cont Nat elem dom] :
+instance [GetElem? cont Nat elem dom] [h : LawfulGetElem cont Nat elem dom] :
       LawfulGetElem cont (Fin n) elem fun xs i => dom xs i where
-
   getElem?_def _c _i _d := h.getElem?_def ..
-  getElem!_def _c _i _d := h.getElem!_def ..
+  getElem!_def _c _i := h.getElem!_def ..
 
-@[simp] theorem getElem_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i) :
+@[simp] theorem getElem_fin [GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i) :
     a[i] = a[i.1] := rfl
 
-@[simp] theorem getElem?_fin [h : GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n)
+@[simp] theorem getElem?_fin [h : GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n)
     [Decidable (Dom a i)] : a[i]? = a[i.1]? := by rfl
 
-@[simp] theorem getElem!_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n)
+@[simp] theorem getElem!_fin [GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n)
     [Decidable (Dom a i)] [Inhabited Elem] : a[i]! = a[i.1]! := rfl
 
 macro_rules
@@ -139,8 +187,6 @@ namespace List
 instance : GetElem (List α) Nat α fun as i => i < as.length where
   getElem as i h := as.get ⟨i, h⟩
 
-instance : LawfulGetElem (List α) Nat α fun as i => i < as.length where
-
 @[simp] theorem getElem_cons_zero (a : α) (as : List α) (h : 0 < (a :: as).length) : getElem (a :: as) 0 h = a := by
   rfl
 
@@ -163,8 +209,6 @@ namespace Array
 instance : GetElem (Array α) Nat α fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
-instance : LawfulGetElem (Array α) Nat α fun xs i => i < xs.size where
-
 end Array
 
 namespace Lean.Syntax
@@ -172,6 +216,4 @@ namespace Lean.Syntax
 instance : GetElem Syntax Nat Syntax fun _ _ => True where
   getElem stx i _ := stx.getArg i
 
-instance : LawfulGetElem Syntax Nat Syntax fun _ _ => True where
-
 end Lean.Syntax

src/Init/MetaTypes.lean

@@ -218,6 +218,14 @@ structure Config where
   to find candidate `simp` theorems. It approximates Lean 3 `simp` behavior.
   -/
   index             : Bool := true
+  /--
+  When `true` (default: `false`), `simp` will **not** create a proof for a rewriting rule associated
+  with an `rfl`-theorem.
+  Rewriting rules are provided by users by annotating theorems with the attribute `@[simp]`.
+  If the proof of the theorem is just `rfl` (reflexivity), and `implicitDefEqProofs := true`, `simp`
+  will **not** create a proof term which is an application of the annotated theorem.
+  -/
+  implicitDefEqProofs : Bool := false
   deriving Inhabited, BEq
 
 -- Configuration object for `simp_all`

src/Lean/AddDecl.lean

@@ -8,8 +8,17 @@ import Lean.CoreM
 
 namespace Lean
 
+register_builtin_option debug.skipKernelTC : Bool := {
+  defValue := false
+  group    := "debug"
+  descr    := "skip kernel type checker. WARNING: setting this option to true may compromise soundness because your proofs will not be checked by the Lean kernel"
+}
+
 def Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration) : Except KernelException Environment :=
-  addDeclCore env (Core.getMaxHeartbeats opts).toUSize decl
+  if debug.skipKernelTC.get opts then
+    addDeclWithoutChecking env decl
+  else
+    addDeclCore env (Core.getMaxHeartbeats opts).toUSize decl
 
 def Environment.addAndCompile (env : Environment) (opts : Options) (decl : Declaration) : Except KernelException Environment := do
   let env ← addDecl env opts decl

src/Lean/CoreM.lean

@@ -211,12 +211,12 @@ instance : MonadTrace CoreM where
 
 structure SavedState extends State where
   /-- Number of heartbeats passed inside `withRestoreOrSaveFull`, not used otherwise. -/
-  passedHearbeats : Nat
+  passedHeartbeats : Nat
 deriving Nonempty
 
 def saveState : CoreM SavedState := do
   let s ← get
-  return { toState := s, passedHearbeats := 0 }
+  return { toState := s, passedHeartbeats := 0 }
 
 /--
 Incremental reuse primitive: if `reusableResult?` is `none`, runs `act` and returns its result
@@ -236,14 +236,14 @@ itself after calling `act` as well as by reuse-handling code such as the one sup
     (act : CoreM α) : CoreM (α × SavedState) := do
   if let some (val, state) := reusableResult? then
     set state.toState
-    IO.addHeartbeats state.passedHearbeats.toUInt64
+    IO.addHeartbeats state.passedHeartbeats.toUInt64
     return (val, state)
 
   let startHeartbeats ← IO.getNumHeartbeats
   let a ← act
   let s ← get
   let stopHeartbeats ← IO.getNumHeartbeats
-  return (a, { toState := s, passedHearbeats := stopHeartbeats - startHeartbeats })
+  return (a, { toState := s, passedHeartbeats := stopHeartbeats - startHeartbeats })
 
 /-- Restore backtrackable parts of the state. -/
 def SavedState.restore (b : SavedState) : CoreM Unit :=
@@ -472,23 +472,30 @@ def Exception.isInterrupt : Exception → Bool
 
 /--
 Custom `try-catch` for all monads based on `CoreM`. We usually don't want to catch "runtime
-exceptions" these monads, but on `CommandElabM`. See issues #2775 and #2744 as well as
-`MonadAlwaysExcept`. Also, we never want to catch interrupt exceptions inside the elaborator.
+exceptions" these monads, but on `CommandElabM` or, in specific cases, using `tryCatchRuntimeEx`.
+See issues #2775 and #2744 as well as `MonadAlwaysExcept`. Also, we never want to catch interrupt
+exceptions inside the elaborator.
 -/
 @[inline] protected def Core.tryCatch (x : CoreM α) (h : Exception → CoreM α) : CoreM α := do
   try
     x
   catch ex =>
     if ex.isInterrupt || ex.isRuntime then
-
-      throw ex -- We should use `tryCatchRuntimeEx` for catching runtime exceptions
+      throw ex
     else
       h ex
 
+/--
+A variant of `tryCatch` that also catches runtime exception (see also `tryCatch` documentation).
+Like `tryCatch`, this function does not catch interrupt exceptions, which are not considered runtime
+exceptions.
+-/
 @[inline] protected def Core.tryCatchRuntimeEx (x : CoreM α) (h : Exception → CoreM α) : CoreM α := do
   try
     x
   catch ex =>
+    if ex.isInterrupt then
+      throw ex
     h ex
 
 instance : MonadExceptOf Exception CoreM where
@@ -512,4 +519,16 @@ instance : MonadRuntimeException CoreM where
 @[inline] def mapCoreM [MonadControlT CoreM m] [Monad m] (f : forall {α}, CoreM α → CoreM α) {α} (x : m α) : m α :=
   controlAt CoreM fun runInBase => f <| runInBase x
 
+/--
+Returns `true` if the given message kind has not been reported in the message log,
+and then mark it as reported. Otherwise, returns `false`.
+We use this API to ensure we don't report the same kind of warning multiple times.
+-/
+def reportMessageKind (kind : Name) : CoreM Bool := do
+  if (← get).messages.reportedKinds.contains kind then
+    return false
+  else
+    modify fun s => { s with messages.reportedKinds := s.messages.reportedKinds.insert kind }
+    return true
+
 end Lean

src/Lean/Data/HashMap.lean

@@ -223,8 +223,6 @@ def insertIfNew (m : HashMap α β) (a : α) (b : β) : HashMap α β × Option
 instance : GetElem (HashMap α β) α (Option β) fun _ _ => True where
   getElem m k _ := m.find? k
 
-instance : LawfulGetElem (HashMap α β) α (Option β) fun _ _ => True where
-
 @[inline] def contains (m : HashMap α β) (a : α) : Bool :=
   match m with
   | ⟨ m, _ ⟩ => m.contains a

src/Lean/Data/PersistentArray.lean

@@ -72,8 +72,6 @@ def get! [Inhabited α] (t : PersistentArray α) (i : Nat) : α :=
 instance [Inhabited α] : GetElem (PersistentArray α) Nat α fun as i => i < as.size where
   getElem xs i _ := xs.get! i
 
-instance [Inhabited α] : LawfulGetElem (PersistentArray α) Nat α fun as i => i < as.size where
-
 partial def setAux : PersistentArrayNode α → USize → USize → α → PersistentArrayNode α
   | node cs, i, shift, a =>
     let j     := div2Shift i shift

src/Lean/Data/PersistentHashMap.lean

@@ -161,8 +161,6 @@ def find? {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → Op
 instance {_ : BEq α} {_ : Hashable α} : GetElem (PersistentHashMap α β) α (Option β) fun _ _ => True where
   getElem m i _ := m.find? i
 
-instance {_ : BEq α} {_ : Hashable α} : LawfulGetElem (PersistentHashMap α β) α (Option β) fun _ _ => True where
-
 @[inline] def findD {_ : BEq α} {_ : Hashable α} (m : PersistentHashMap α β) (a : α) (b₀ : β) : β :=
   (m.find? a).getD b₀
 

src/Lean/Elab/BuiltinTerm.lean

@@ -157,9 +157,19 @@ private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr :=
   registerSyntheticMVar ref mvarId <| SyntheticMVarKind.tactic tacticCode (← saveContext)
   return mvar
 
+register_builtin_option debug.byAsSorry : Bool := {
+  defValue := false
+  group    := "debug"
+  descr    := "replace `by ..` blocks with `sorry` IF the expected type is a proposition"
+}
+
 @[builtin_term_elab byTactic] def elabByTactic : TermElab := fun stx expectedType? => do
   match expectedType? with
-  | some expectedType => mkTacticMVar expectedType stx
+  | some expectedType =>
+    if ← pure (debug.byAsSorry.get (← getOptions)) <&&> isProp expectedType then
+      mkSorry expectedType false
+    else
+      mkTacticMVar expectedType stx
   | none =>
     tryPostpone
     throwError ("invalid 'by' tactic, expected type has not been provided")

src/Lean/Elab/Command.lean

@@ -81,7 +81,10 @@ Remark: see comment at TermElabM
 @[always_inline]
 instance : Monad CommandElabM := let i := inferInstanceAs (Monad CommandElabM); { pure := i.pure, bind := i.bind }
 
-/-- Like `Core.tryCatch` but do catch runtime exceptions. -/
+/--
+Like `Core.tryCatchRuntimeEx`; runtime errors are generally used to abort term elaboration, so we do
+want to catch and process them at the command level.
+-/
 @[inline] protected def tryCatch (x : CommandElabM α) (h : Exception → CommandElabM α) :
     CommandElabM α := do
   try

src/Lean/Elab/LetRec.lean

@@ -30,20 +30,24 @@ structure LetRecView where
 
 /-  group ("let " >> nonReservedSymbol "rec ") >> sepBy1 (group (optional «attributes» >> letDecl)) ", " >> "; " >> termParser -/
 private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
-  let decls ← letRec[1][0].getSepArgs.mapM fun (attrDeclStx : Syntax) => do
+  let mut decls : Array LetRecDeclView := #[]
+  for attrDeclStx in letRec[1][0].getSepArgs do
     let docStr? ← expandOptDocComment? attrDeclStx[0]
     let attrOptStx := attrDeclStx[1]
     let attrs ← if attrOptStx.isNone then pure #[] else elabDeclAttrs attrOptStx[0]
     let decl := attrDeclStx[2][0]
     if decl.isOfKind `Lean.Parser.Term.letPatDecl then
       throwErrorAt decl "patterns are not allowed in 'let rec' expressions"
-    else if decl.isOfKind `Lean.Parser.Term.letIdDecl || decl.isOfKind `Lean.Parser.Term.letEqnsDecl then
+    else if decl.isOfKind ``Lean.Parser.Term.letIdDecl || decl.isOfKind ``Lean.Parser.Term.letEqnsDecl then
       let declId := decl[0]
       unless declId.isIdent do
         throwErrorAt declId "'let rec' expressions must be named"
       let shortDeclName := declId.getId
       let currDeclName? ← getDeclName?
       let declName := currDeclName?.getD Name.anonymous ++ shortDeclName
+      if decls.any fun decl => decl.declName == declName then
+        withRef declId do
+          throwError "'{declName}' has already been declared"
       checkNotAlreadyDeclared declName
       applyAttributesAt declName attrs AttributeApplicationTime.beforeElaboration
       addDocString' declName docStr?
@@ -62,8 +66,10 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
       else
         liftMacroM <| expandMatchAltsIntoMatch decl decl[3]
       let termination ← WF.elabTerminationHints ⟨attrDeclStx[3]⟩
-      pure { ref := declId, attrs, shortDeclName, declName, binderIds, type, mvar, valStx,
-             termination : LetRecDeclView }
+      decls := decls.push {
+        ref := declId, attrs, shortDeclName, declName,
+        binderIds, type, mvar, valStx, termination
+      }
     else
       throwUnsupportedSyntax
   return { decls, body := letRec[3] }

src/Lean/Elab/MutualDef.lean

@@ -846,10 +846,7 @@ private def levelMVarToParamHeaders (views : Array DefView) (headers : Array Def
   let rec process : StateRefT Nat TermElabM (Array DefViewElabHeader) := do
     let mut newHeaders := #[]
     for view in views, header in headers do
-      -- Remark: we should consider using `pure view.kind.isTheorem <||> isProp header.type`, and
-      -- also handle definitions. We used the following approach because it is less disruptive to Mathlib.
-      -- Moreover, the type of most definitions are not propositions anyway.
-      if ← pure view.kind.isTheorem <||> (pure view.kind.isExample <&&> isProp header.type) then
+      if ← pure view.kind.isTheorem <||> isProp header.type then
         newHeaders ←
           withLevelNames header.levelNames do
             return newHeaders.push { header with type := (← levelMVarToParam header.type), levelNames := (← getLevelNames) }

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

@@ -35,12 +35,61 @@ private def hasBadParamDep? (ys : Array Expr) (indParams : Array Expr) : MetaM (
         return some (p, y)
   return none
 
-private def throwStructuralFailed : MetaM α :=
-  throwError "structural recursion cannot be used"
-
-private def orelse' (x y : M α) : M α := do
-  let saveState ← get
-  orelseMergeErrors x (do set saveState; y)
+/--
+Pass to `k` the `RecArgInfo` for the `i`th parameter in the parameter list `xs`. This performs
+various sanity checks on the argument (is it even an inductive type etc).
+Also wraps all errors in a common “argument cannot be used” header
+-/
+def withRecArgInfo (numFixed : Nat) (xs : Array Expr) (i : Nat) (k : RecArgInfo → M α) : M α := do
+  mapError
+    (f := fun msg => m!"argument #{i+1} cannot be used for structural recursion{indentD msg}") do
+  if h : i < xs.size then
+    if i < numFixed then
+      throwError "it is unchanged in the recursive calls"
+    let x := xs[i]
+    let localDecl ← getFVarLocalDecl x
+    if localDecl.isLet then
+      throwError "it is a let-binding"
+    let xType ← whnfD localDecl.type
+    matchConstInduct xType.getAppFn (fun _ => throwError "its type is not an inductive") fun indInfo us => do
+    if !(← hasConst (mkBRecOnName indInfo.name)) then
+      throwError "its type does not have a recursor"
+    else if indInfo.isReflexive && !(← hasConst (mkBInductionOnName indInfo.name)) && !(← isInductivePredicate indInfo.name) then
+      throwError "its type is a reflexive inductive, but {mkBInductionOnName indInfo.name} does not exist and it is not an inductive predicate"
+    else
+      let indArgs    := xType.getAppArgs
+      let indParams  := indArgs.extract 0 indInfo.numParams
+      let indIndices := indArgs.extract indInfo.numParams indArgs.size
+      if !indIndices.all Expr.isFVar then
+        throwError "its type is an inductive family and indices are not variables{indentExpr xType}"
+      else if !indIndices.allDiff then
+        throwError " its type is an inductive family and indices are not pairwise distinct{indentExpr xType}"
+      else
+        let indexMinPos := getIndexMinPos xs indIndices
+        let numFixed    := if indexMinPos < numFixed then indexMinPos else numFixed
+        let fixedParams := xs.extract 0 numFixed
+        let ys          := xs.extract numFixed xs.size
+        match (← hasBadIndexDep? ys indIndices) with
+        | some (index, y) =>
+          throwError "its type is an inductive family{indentExpr xType}\nand index{indentExpr index}\ndepends on the non index{indentExpr y}"
+        | none =>
+          match (← hasBadParamDep? ys indParams) with
+          | some (indParam, y) =>
+            throwError "its type is an inductive datatype{indentExpr xType}\nand parameter{indentExpr indParam}\ndepends on{indentExpr y}"
+          | none =>
+            let indicesPos := indIndices.map fun index => match ys.indexOf? index with | some i => i.val | none => unreachable!
+            k { fixedParams := fixedParams
+                ys          := ys
+                pos         := i - fixedParams.size
+                indicesPos  := indicesPos
+                indName     := indInfo.name
+                indLevels   := us
+                indParams   := indParams
+                indIndices  := indIndices
+                reflexive   := indInfo.isReflexive
+                indPred     := ←isInductivePredicate indInfo.name }
+    else
+      throwError "the index #{i+1} exceeds {xs.size}, the number of parameters"
 
 /--
   Try to find an argument that is structurally smaller in every recursive application.
@@ -49,16 +98,10 @@ private def orelse' (x y : M α) : M α := do
   We give preference for arguments that are *not* indices of inductive types of other arguments.
   See issue #837 for an example where we can show termination using the index of an inductive family, but
   we don't get the desired definitional equalities.
-
-  We perform two passes. In the first-pass, we only consider arguments that are not indices.
-  In the second pass, we consider them.
-
-  TODO: explore whether there are better solutions, and whether there are other ways to break the heuristic used
-  for creating the smart unfolding auxiliary definition.
 -/
 partial def findRecArg (numFixed : Nat) (xs : Array Expr) (k : RecArgInfo → M α) : M α := do
   /- Collect arguments that are indices. See comment above. -/
-  let indicesRef : IO.Ref FVarIdSet ← IO.mkRef {}
+  let indicesRef : IO.Ref (Array Nat) ← IO.mkRef {}
   for x in xs do
     let xType ← inferType x
     /- Traverse all sub-expressions in the type of `x` -/
@@ -68,75 +111,22 @@ partial def findRecArg (numFixed : Nat) (xs : Array Expr) (k : RecArgInfo → M
         if info.numIndices > 0 && info.numParams + info.numIndices == e.getAppNumArgs then
           for arg in e.getAppArgs[info.numParams:] do
             forEachExpr arg fun e => do
-              if e.isFVar && xs.any (· == e) then
-                indicesRef.modify fun indices => indices.insert e.fvarId!
+              if let .some idx := xs.getIdx? e then
+                indicesRef.modify fun indices => indices.push idx
   let indices ← indicesRef.get
-  /- We perform two passes. See comment above. -/
-  let rec go (i : Nat) (firstPass : Bool) : M α := do
-    if h : i < xs.size then
-      let x := xs.get ⟨i, h⟩
-      trace[Elab.definition.structural] "findRecArg x: {x}, firstPass: {firstPass}"
-      let localDecl ← getFVarLocalDecl x
-      if localDecl.isLet then
-        throwStructuralFailed
-      else if firstPass == indices.contains localDecl.fvarId then
-        go (i+1) firstPass
-      else
-        let xType ← whnfD localDecl.type
-        matchConstInduct xType.getAppFn (fun _ => go (i+1) firstPass) fun indInfo us => do
-        if !(← hasConst (mkBRecOnName indInfo.name)) then
-          go (i+1) firstPass
-        else if indInfo.isReflexive && !(← hasConst (mkBInductionOnName indInfo.name)) && !(← isInductivePredicate indInfo.name) then
-          go (i+1) firstPass
-        else
-          let indArgs    := xType.getAppArgs
-          let indParams  := indArgs.extract 0 indInfo.numParams
-          let indIndices := indArgs.extract indInfo.numParams indArgs.size
-          if !indIndices.all Expr.isFVar then
-            orelse'
-              (throwError "argument #{i+1} was not used because its type is an inductive family and indices are not variables{indentExpr xType}")
-              (go (i+1) firstPass)
-          else if !indIndices.allDiff then
-            orelse'
-              (throwError "argument #{i+1} was not used because its type is an inductive family and indices are not pairwise distinct{indentExpr xType}")
-              (go (i+1) firstPass)
-          else
-            let indexMinPos := getIndexMinPos xs indIndices
-            let numFixed    := if indexMinPos < numFixed then indexMinPos else numFixed
-            let fixedParams := xs.extract 0 numFixed
-            let ys          := xs.extract numFixed xs.size
-            match (← hasBadIndexDep? ys indIndices) with
-            | some (index, y) =>
-              orelse'
-                (throwError "argument #{i+1} was not used because its type is an inductive family{indentExpr xType}\nand index{indentExpr index}\ndepends on the non index{indentExpr y}")
-                (go (i+1) firstPass)
-            | none =>
-              match (← hasBadParamDep? ys indParams) with
-              | some (indParam, y) =>
-                orelse'
-                  (throwError "argument #{i+1} was not used because its type is an inductive datatype{indentExpr xType}\nand parameter{indentExpr indParam}\ndepends on{indentExpr y}")
-                  (go (i+1) firstPass)
-              | none =>
-                let indicesPos := indIndices.map fun index => match ys.indexOf? index with | some i => i.val | none => unreachable!
-                orelse'
-                  (mapError
-                    (k { fixedParams := fixedParams
-                         ys          := ys
-                         pos         := i - fixedParams.size
-                         indicesPos  := indicesPos
-                         indName     := indInfo.name
-                         indLevels   := us
-                         indParams   := indParams
-                         indIndices  := indIndices
-                         reflexive := indInfo.isReflexive
-                         indPred := ←isInductivePredicate indInfo.name })
-                    (fun msg => m!"argument #{i+1} was not used for structural recursion{indentD msg}"))
-                  (go (i+1) firstPass)
-    else if firstPass then
-      go (i := numFixed) (firstPass := false)
-    else
-      throwStructuralFailed
-
-  go (i := numFixed) (firstPass := true)
+  let nonIndices := (Array.range xs.size).filter (fun i => !(indices.contains i))
+  let mut errors : Array MessageData := Array.mkArray xs.size m!""
+  let saveState ← get -- backtrack the state for each argument
+  for i in id (nonIndices ++ indices) do
+    let x := xs[i]!
+    trace[Elab.definition.structural] "findRecArg x: {x}"
+    try
+      set saveState
+      return (← withRecArgInfo numFixed xs i k)
+    catch e => errors := errors.set! i e.toMessageData
+  throwError
+    errors.foldl
+      (init := m!"structural recursion cannot be used:")
+      (f := (· ++ Format.line ++ Format.line ++ .))
 
 end Lean.Elab.Structural

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

@@ -66,7 +66,6 @@ private def elimRecursion (preDef : PreDefinition) : M (Nat × PreDefinition) :=
     let numFixed ← getFixedPrefix preDef.declName xs value
     trace[Elab.definition.structural] "numFixed: {numFixed}"
     findRecArg numFixed xs fun recArgInfo => do
-      -- when (recArgInfo.indName == `Nat) throwStructuralFailed -- HACK to skip Nat argument
       let valueNew ← if recArgInfo.indPred then
         mkIndPredBRecOn preDef.declName recArgInfo value
       else

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -22,12 +22,15 @@ Runs a term elaborator inside a tactic.
 This function ensures that term elaboration fails when backtracking,
 i.e., in `first| tac term | other`.
 -/
-def runTermElab (k : TermElabM α) (mayPostpone := false) : TacticM α := do
-  /- If error recovery is disabled, we disable `Term.withoutErrToSorry` -/
-  if (← read).recover then
-    go
-  else
-    Term.withoutErrToSorry go
+def runTermElab (k : TermElabM α) (mayPostpone := false) : TacticM α :=
+  -- We disable incrementality here so that nested tactics do not unexpectedly use and affect the
+  -- incrementality state of a calling incrementality-enabled tactic.
+  Term.withoutTacticIncrementality true do
+    /- If error recovery is disabled, we disable `Term.withoutErrToSorry` -/
+    if (← read).recover then
+      go
+    else
+      Term.withoutErrToSorry go
 where
   go := k <* Term.synthesizeSyntheticMVars (postpone := .ofBool mayPostpone)
 

src/Lean/Elab/Term.lean

@@ -1259,8 +1259,8 @@ private def isNoImplicitLambda (stx : Syntax) : Bool :=
 
 private def isTypeAscription (stx : Syntax) : Bool :=
   match stx with
-  | `(($_ : $_)) => true
-  | _            => false
+  | `(($_ : $[$_]?)) => true
+  | _                => false
 
 def hasNoImplicitLambdaAnnotation (type : Expr) : Bool :=
   annotation? `noImplicitLambda type |>.isSome

src/Lean/Environment.lean

@@ -244,10 +244,21 @@ inductive KernelException where
 
 namespace Environment
 
-/-- Type check given declaration and add it to the environment -/
+/--
+Type check given declaration and add it to the environment
+-/
 @[extern "lean_add_decl"]
 opaque addDeclCore (env : Environment) (maxHeartbeats : USize) (decl : @& Declaration) : Except KernelException Environment
 
+/--
+Add declaration to kernel without type checking it.
+**WARNING** This function is meant for temporarily working around kernel performance issues.
+It compromises soundness because, for example, a buggy tactic may produce an invalid proof,
+and the kernel will not catch it if the new option is set to true.
+-/
+@[extern "lean_add_decl_without_checking"]
+opaque addDeclWithoutChecking (env : Environment) (decl : @& Declaration) : Except KernelException Environment
+
 end Environment
 
 namespace ConstantInfo

src/Lean/Message.lean

@@ -350,6 +350,13 @@ structure MessageLog where
   hadErrors : Bool := false
   /-- The list of messages not already reported, in insertion order. -/
   unreported : PersistentArray Message := {}
+  /--
+  Set of message kinds that have been added to the log.
+  For example, we have the kind `unsafe.exponentiation.warning` for warning messages associated with
+  the configuration option `exponentiation.threshold`.
+  We don't produce a warning if the kind is already in the following set.
+  -/
+  reportedKinds : NameSet := {}
   deriving Inhabited
 
 namespace MessageLog
@@ -403,7 +410,7 @@ def indentExpr (e : Expr) : MessageData :=
   indentD e
 
 class AddMessageContext (m : Type → Type) where
-  /-- 
+  /--
   Without context, a `MessageData` object may be be missing information
   (e.g. hover info) for pretty printing, or may print an error. Hence,
   `addMessageContext` should be called on all constructed `MessageData`

src/Lean/Meta/Constructions.lean

@@ -9,14 +9,13 @@ import Lean.AddDecl
 import Lean.Meta.AppBuilder
 import Lean.Meta.CompletionName
 import Lean.Meta.Constructions.RecOn
+import Lean.Meta.Constructions.BRecOn
 
 namespace Lean
 
 @[extern "lean_mk_cases_on"] opaque mkCasesOnImp (env : Environment) (declName : @& Name) : Except KernelException Declaration
 @[extern "lean_mk_no_confusion_type"] opaque mkNoConfusionTypeCoreImp (env : Environment) (declName : @& Name) : Except KernelException Declaration
 @[extern "lean_mk_no_confusion"] opaque mkNoConfusionCoreImp (env : Environment) (declName : @& Name) : Except KernelException Declaration
-@[extern "lean_mk_below"] opaque mkBelowImp (env : Environment) (declName : @& Name) (ibelow : Bool) : Except KernelException Declaration
-@[extern "lean_mk_brec_on"] opaque mkBRecOnImp (env : Environment) (declName : @& Name) (ind : Bool) : Except KernelException Declaration
 
 open Meta
 
@@ -28,52 +27,6 @@ def mkCasesOn (declName : Name) : MetaM Unit := do
   modifyEnv fun env => markAuxRecursor env name
   modifyEnv fun env => addProtected env name
 
-private def mkBelowOrIBelow (declName : Name) (ibelow : Bool) : MetaM Unit := do
-  let .inductInfo indVal ← getConstInfo declName | return
-  unless indVal.isRec do return
-  if ← isPropFormerType indVal.type then return
-
-  let decl ← ofExceptKernelException (mkBelowImp (← getEnv) declName ibelow)
-  let name := decl.definitionVal!.name
-  addDecl decl
-  setReducibleAttribute name
-  modifyEnv fun env => addToCompletionBlackList env name
-  modifyEnv fun env => addProtected env name
-
-def mkBelow (declName : Name) : MetaM Unit := mkBelowOrIBelow declName true
-def mkIBelow (declName : Name) : MetaM Unit := mkBelowOrIBelow declName false
-
-private def mkBRecOrBInductionOn (declName : Name) (ind : Bool) : MetaM Unit := do
-  let .inductInfo indVal ← getConstInfo declName | return
-  unless indVal.isRec do return
-  if ← isPropFormerType indVal.type then return
-  let .recInfo recInfo ← getConstInfo (mkRecName declName) | return
-  unless recInfo.numMotives = indVal.all.length do
-    /-
-    The mutual declaration containing `declName` contains nested inductive datatypes.
-    We don't support this kind of declaration here yet. We probably never will :)
-    To support it, we will need to generate an auxiliary `below` for each nested inductive
-    type since their default `below` is not good here. For example, at
-    ```
-    inductive Term
-    | var : String -> Term
-    | app : String -> List Term -> Term
-    ```
-    The `List.below` is not useful since it will not allow us to recurse over the nested terms.
-    We need to generate another one using the auxiliary recursor `Term.rec_1` for `List Term`.
-    -/
-    return
-
-  let decl ← ofExceptKernelException (mkBRecOnImp (← getEnv) declName ind)
-  let name := decl.definitionVal!.name
-  addDecl decl
-  setReducibleAttribute name
-  modifyEnv fun env => markAuxRecursor env name
-  modifyEnv fun env => addProtected env name
-
-def mkBRecOn (declName : Name) : MetaM Unit := mkBRecOrBInductionOn declName false
-def mkBInductionOn (declName : Name) : MetaM Unit := mkBRecOrBInductionOn declName true
-
 def mkNoConfusionCore (declName : Name) : MetaM Unit := do
   -- Do not do anything unless can_elim_to_type. TODO: Extract to util
   let .inductInfo indVal ← getConstInfo declName | return
@@ -103,7 +56,6 @@ def mkNoConfusionEnum (enumName : Name) : MetaM Unit := do
     -- `noConfusionEnum` was not defined yet, so we use `mkNoConfusionCore`
     mkNoConfusionCore enumName
 where
-
   mkToCtorIdx : MetaM Unit := do
     let ConstantInfo.inductInfo info ← getConstInfo enumName | unreachable!
     let us := info.levelParams.map mkLevelParam

src/Lean/Meta/Constructions/BRecOn.lean

@@ -0,0 +1,393 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Joachim Breitner
+-/
+prelude
+import Lean.Meta.InferType
+import Lean.AuxRecursor
+import Lean.AddDecl
+import Lean.Meta.CompletionName
+
+namespace Lean
+open Meta
+
+section PProd
+
+/--!
+Helpers to construct types and values of `PProd` and project out of them, set up to use `And`
+instead of `PProd` if the universes allow. Maybe be extracted into a Utils module when useful
+elsewhere.
+-/
+
+private def mkPUnit : Level → Expr
+  | .zero => .const ``True []
+  | lvl   => .const ``PUnit [lvl]
+
+private def mkPProd (e1 e2 : Expr) : MetaM Expr := do
+  let lvl1 ← getLevel e1
+  let lvl2 ← getLevel e2
+  if lvl1 matches .zero && lvl2 matches .zero then
+    return mkApp2 (.const `And []) e1 e2
+  else
+    return mkApp2 (.const ``PProd [lvl1, lvl2]) e1 e2
+
+private def mkNProd (lvl : Level) (es : Array Expr) : MetaM Expr :=
+  es.foldrM (init := mkPUnit lvl) mkPProd
+
+private def mkPUnitMk : Level → Expr
+  | .zero => .const ``True.intro []
+  | lvl   => .const ``PUnit.unit [lvl]
+
+private def mkPProdMk (e1 e2 : Expr) : MetaM Expr := do
+  let t1 ← inferType e1
+  let t2 ← inferType e2
+  let lvl1 ← getLevel t1
+  let lvl2 ← getLevel t2
+  if lvl1 matches .zero && lvl2 matches .zero then
+    return mkApp4 (.const ``And.intro []) t1 t2 e1 e2
+  else
+    return mkApp4 (.const ``PProd.mk [lvl1, lvl2]) t1 t2 e1 e2
+
+private def mkNProdMk (lvl : Level) (es : Array Expr) : MetaM Expr :=
+  es.foldrM (init := mkPUnitMk lvl) mkPProdMk
+
+/-- `PProd.fst` or `And.left` (as projections) -/
+private def mkPProdFst (e : Expr) : MetaM Expr := do
+  let t ← whnf (← inferType e)
+  match_expr t with
+  | PProd _ _ => return .proj ``PProd 0 e
+  | And _ _ =>   return .proj ``And 0 e
+  | _ => throwError "Cannot project .1 out of{indentExpr e}\nof type{indentExpr t}"
+
+/-- `PProd.snd` or `And.right` (as projections) -/
+private def mkPProdSnd (e : Expr) : MetaM Expr := do
+  let t ← whnf (← inferType e)
+  match_expr t with
+  | PProd _ _ => return .proj ``PProd 1 e
+  | And _ _ =>   return .proj ``And 1 e
+  | _ => throwError "Cannot project .2 out of{indentExpr e}\nof type{indentExpr t}"
+
+end PProd
+
+/--
+If `minorType` is the type of a minor premies of a recursor, such as
+```
+  (cons : (head : α) → (tail : List α) → (tail_hs : motive tail) → motive (head :: tail))
+```
+of `List.rec`, constructs the corresponding argument to `List.rec` in the construction
+of `.below` definition; in this case
+```
+fun head tail tail_ih =>
+  PProd (PProd (motive tail) tail_ih) PUnit
+```
+of type
+```
+α → List α → Sort (max 1 u_1) → Sort (max 1 u_1)
+```
+The parameter `typeFormers` are the `motive`s.
+-/
+private def buildBelowMinorPremise (rlvl : Level) (typeFormers : Array Expr) (minorType : Expr) : MetaM Expr :=
+  forallTelescope minorType fun minor_args _ => do go #[] minor_args.toList
+where
+  ibelow := rlvl matches .zero
+  go (prods : Array Expr) : List Expr → MetaM Expr
+  | [] => mkNProd rlvl prods
+  | arg::args => do
+    let argType ← inferType arg
+    forallTelescope argType fun arg_args arg_type => do
+      if typeFormers.contains arg_type.getAppFn then
+        let name ← arg.fvarId!.getUserName
+        let type' ← forallTelescope argType fun args _ => mkForallFVars args (.sort rlvl)
+        withLocalDeclD name type' fun arg' => do
+          let snd ← mkForallFVars arg_args (mkAppN arg' arg_args)
+          let e' ← mkPProd argType snd
+          mkLambdaFVars #[arg'] (← go (prods.push e') args)
+      else
+        mkLambdaFVars #[arg] (← go prods args)
+
+/--
+Constructs the `.below` or `.ibelow` definition for a inductive predicate.
+
+For example for the `List` type, it constructs,
+```
+@[reducible] protected def List.below.{u_1, u} : {α : Type u} →
+  {motive : List α → Sort u_1} → List α → Sort (max 1 u_1) :=
+fun {α} {motive} t =>
+  List.rec PUnit (fun head tail tail_ih => PProd (PProd (motive tail) tail_ih) PUnit) t
+```
+and
+```
+@[reducible] protected def List.ibelow.{u} : {α : Type u} →
+  {motive : List α → Prop} → List α → Prop :=
+fun {α} {motive} t =>
+  List.rec True (fun head tail tail_ih => (motive tail ∧ tail_ih) ∧ True) t
+```
+-/
+private def mkBelowOrIBelow (indName : Name) (ibelow : Bool) : MetaM Unit := do
+  let .inductInfo indVal ← getConstInfo indName | return
+  unless indVal.isRec do return
+  if ← isPropFormerType indVal.type then return
+
+  let recName := mkRecName indName
+  -- The construction follows the type of `ind.rec`
+  let .recInfo recVal ← getConstInfo recName
+    | throwError "{recName} not a .recInfo"
+  let lvl::lvls := recVal.levelParams.map (Level.param ·)
+    | throwError "recursor {recName} has no levelParams"
+  let lvlParam := recVal.levelParams.head!
+  -- universe parameter names of ibelow/below
+  let blvls :=
+    -- For ibelow we instantiate the first universe parameter of `.rec` to `.zero`
+    if ibelow then recVal.levelParams.tail!
+              else recVal.levelParams
+  let .some ilvl ← typeFormerTypeLevel indVal.type
+    | throwError "type {indVal.type} of inductive {indVal.name} not a type former?"
+
+  -- universe level of the resultant type
+  let rlvl : Level :=
+    if ibelow then
+      0
+    else if indVal.isReflexive then
+      if let .max 1 lvl := ilvl then
+        mkLevelMax' (.succ lvl) lvl
+      else
+        mkLevelMax' (.succ lvl) ilvl
+    else
+      mkLevelMax' 1 lvl
+
+  let refType :=
+    if ibelow then
+      recVal.type.instantiateLevelParams [lvlParam] [0]
+    else if indVal.isReflexive then
+      recVal.type.instantiateLevelParams [lvlParam] [lvl.succ]
+    else
+      recVal.type
+
+  let decl ← forallTelescope refType fun refArgs _ => do
+    assert! refArgs.size == indVal.numParams + recVal.numMotives + recVal.numMinors + indVal.numIndices + 1
+    let params      : Array Expr := refArgs[:indVal.numParams]
+    let typeFormers : Array Expr := refArgs[indVal.numParams:indVal.numParams + recVal.numMotives]
+    let minors      : Array Expr := refArgs[indVal.numParams + recVal.numMotives:indVal.numParams + recVal.numMotives + recVal.numMinors]
+    let remaining   : Array Expr := refArgs[indVal.numParams + recVal.numMotives + recVal.numMinors:]
+
+    let mut val := .const recName (rlvl.succ :: lvls)
+    -- add parameters
+    val := mkAppN val params
+    -- add type formers
+    for typeFormer in typeFormers do
+      let arg ← forallTelescope (← inferType typeFormer) fun targs _ =>
+        mkLambdaFVars targs (.sort rlvl)
+      val := .app val arg
+    -- add minor premises
+    for minor in minors do
+      let arg ← buildBelowMinorPremise rlvl typeFormers (← inferType minor)
+      val := .app val arg
+    -- add indices and major premise
+    val := mkAppN val remaining
+
+    -- All paramaters of `.rec` besides the `minors` become parameters of `.below`
+    let below_params := params ++ typeFormers ++ remaining
+    let type ← mkForallFVars below_params (.sort rlvl)
+    val ← mkLambdaFVars below_params val
+
+    let name := if ibelow then mkIBelowName indName else mkBelowName indName
+    mkDefinitionValInferrringUnsafe name blvls type val .abbrev
+
+  addDecl (.defnDecl decl)
+  setReducibleAttribute decl.name
+  modifyEnv fun env => markAuxRecursor env decl.name
+  modifyEnv fun env => addProtected env decl.name
+
+def mkBelow (declName : Name) : MetaM Unit := mkBelowOrIBelow declName true
+def mkIBelow (declName : Name) : MetaM Unit := mkBelowOrIBelow declName false
+
+/--
+If `minorType` is the type of a minor premies of a recursor, such as
+```
+  (cons : (head : α) → (tail : List α) → (tail_hs : motive tail) → motive (head :: tail))
+```
+of `List.rec`, constructs the corresponding argument to `List.rec` in the construction
+of `.brecOn` definition; in this case
+```
+fun head tail tail_ih =>
+  ⟨F_1 (head :: tail) ⟨tail_ih, PUnit.unit⟩, ⟨tail_ih, PUnit.unit⟩⟩
+```
+of type
+```
+(head : α) → (tail : List α) →
+  PProd (motive tail) (List.below tail) →
+  PProd (motive (head :: tail)) (PProd (PProd (motive tail) (List.below tail)) PUnit)
+```
+The parameter `typeFormers` are the `motive`s.
+-/
+private def buildBRecOnMinorPremise (rlvl : Level) (typeFormers : Array Expr)
+    (belows : Array Expr) (fs : Array Expr) (minorType : Expr) : MetaM Expr :=
+  forallTelescope minorType fun minor_args minor_type => do
+    let rec go (prods : Array Expr) : List Expr → MetaM Expr
+      | [] => minor_type.withApp fun minor_type_fn minor_type_args => do
+          let b ← mkNProdMk rlvl prods
+          let .some ⟨idx, _⟩ := typeFormers.indexOf? minor_type_fn
+            | throwError m!"Did not find {minor_type} in {typeFormers}"
+          mkPProdMk (mkAppN fs[idx]! (minor_type_args.push b)) b
+      | arg::args => do
+        let argType ← inferType arg
+        forallTelescope argType fun arg_args arg_type => do
+          arg_type.withApp fun arg_type_fn arg_type_args => do
+            if let .some idx := typeFormers.indexOf? arg_type_fn then
+              let name ← arg.fvarId!.getUserName
+              let type' ← mkForallFVars arg_args
+                (← mkPProd arg_type (mkAppN belows[idx]! arg_type_args) )
+              withLocalDeclD name type' fun arg' => do
+                if arg_args.isEmpty then
+                  mkLambdaFVars #[arg'] (← go (prods.push arg') args)
+                else
+                  let r := mkAppN arg' arg_args
+                  let r₁ ← mkLambdaFVars arg_args (← mkPProdFst r)
+                  let r₂ ← mkLambdaFVars arg_args (← mkPProdSnd r)
+                  let r ← mkPProdMk r₁ r₂
+                  mkLambdaFVars #[arg'] (← go (prods.push r) args)
+            else
+              mkLambdaFVars #[arg] (← go prods args)
+    go #[] minor_args.toList
+
+/--
+Constructs the `.brecon` or `.binductionon` definition for a inductive predicate.
+
+For example for the `List` type, it constructs,
+```
+@[reducible] protected def List.brecOn.{u_1, u} : {α : Type u} → {motive : List α → Sort u_1} →
+  (t : List α) → ((t : List α) → List.below t → motive t) → motive t :=
+fun {α} {motive} t (F_1 : (t : List α) → List.below t → motive t) => (
+  @List.rec α (fun t => PProd (motive t) (@List.below α motive t))
+    ⟨F_1 [] PUnit.unit, PUnit.unit⟩
+    (fun head tail tail_ih => ⟨F_1 (head :: tail) ⟨tail_ih, PUnit.unit⟩, ⟨tail_ih, PUnit.unit⟩⟩)
+    t
+  ).1
+```
+and
+```
+@[reducible] protected def List.binductionOn.{u} : ∀ {α : Type u} {motive : List α → Prop}
+  (t : List α), (∀ (t : List α), List.ibelow t → motive t) → motive t :=
+fun {α} {motive} t F_1 => (
+  @List.rec α (fun t => And (motive t) (@List.ibelow α motive t))
+    ⟨F_1 [] True.intro, True.intro⟩
+    (fun head tail tail_ih => ⟨F_1 (head :: tail) ⟨tail_ih, True.intro⟩, ⟨tail_ih, True.intro⟩⟩)
+    t
+  ).1
+```
+-/
+def mkBRecOnOrBInductionOn (indName : Name) (ind : Bool) : MetaM Unit := do
+  let .inductInfo indVal ← getConstInfo indName | return
+  unless indVal.isRec do return
+  if ← isPropFormerType indVal.type then return
+  let recName := mkRecName indName
+  let .recInfo recVal ← getConstInfo recName | return
+  unless recVal.numMotives = indVal.all.length do
+    /-
+    The mutual declaration containing `declName` contains nested inductive datatypes.
+    We don't support this kind of declaration here yet. We probably never will :)
+    To support it, we will need to generate an auxiliary `below` for each nested inductive
+    type since their default `below` is not good here. For example, at
+    ```
+    inductive Term
+    | var : String -> Term
+    | app : String -> List Term -> Term
+    ```
+    The `List.below` is not useful since it will not allow us to recurse over the nested terms.
+    We need to generate another one using the auxiliary recursor `Term.rec_1` for `List Term`.
+    -/
+    return
+
+  let lvl::lvls := recVal.levelParams.map (Level.param ·)
+    | throwError "recursor {recName} has no levelParams"
+  let lvlParam := recVal.levelParams.head!
+  -- universe parameter names of brecOn/binductionOn
+  let blps := if ind then recVal.levelParams.tail!  else recVal.levelParams
+  -- universe arguments of below/ibelow
+  let blvls := if ind then lvls else lvl::lvls
+
+  let .some ⟨idx, _⟩ := indVal.all.toArray.indexOf? indName
+    | throwError m!"Did not find {indName} in {indVal.all}"
+
+  let .some ilvl ← typeFormerTypeLevel indVal.type
+    | throwError "type {indVal.type} of inductive {indVal.name} not a type former?"
+  -- universe level of the resultant type
+  let rlvl : Level :=
+    if ind then
+      0
+    else if indVal.isReflexive then
+      if let .max 1 lvl := ilvl then
+        mkLevelMax' (.succ lvl) lvl
+      else
+        mkLevelMax' (.succ lvl) ilvl
+    else
+      mkLevelMax' 1 lvl
+
+  let refType :=
+    if ind then
+      recVal.type.instantiateLevelParams [lvlParam] [0]
+    else if indVal.isReflexive then
+      recVal.type.instantiateLevelParams [lvlParam] [lvl.succ]
+    else
+      recVal.type
+
+  let decl ← forallTelescope refType fun refArgs _ => do
+    assert! refArgs.size == indVal.numParams + recVal.numMotives + recVal.numMinors + indVal.numIndices + 1
+    let params      : Array Expr := refArgs[:indVal.numParams]
+    let typeFormers : Array Expr := refArgs[indVal.numParams:indVal.numParams + recVal.numMotives]
+    let minors      : Array Expr := refArgs[indVal.numParams + recVal.numMotives:indVal.numParams + recVal.numMotives + recVal.numMinors]
+    let remaining   : Array Expr := refArgs[indVal.numParams + recVal.numMotives + recVal.numMinors:]
+
+    -- One `below` for each type former (same parameters)
+    let belows := indVal.all.toArray.map fun n =>
+      let belowName := if ind then mkIBelowName n else mkBelowName n
+      mkAppN (.const belowName blvls) (params ++ typeFormers)
+
+    -- create types of functionals (one for each type former)
+    --   (F_1 : (t : List α) → (f : List.below t) → motive t)
+    -- and bring parameters of that type into scope
+    let mut fDecls : Array (Name × (Array Expr -> MetaM Expr)) := #[]
+    for typeFormer in typeFormers, below in belows, i in [:typeFormers.size] do
+      let fType ← forallTelescope (← inferType typeFormer) fun targs _ => do
+        withLocalDeclD `f (mkAppN below targs) fun f =>
+          mkForallFVars (targs.push f) (mkAppN typeFormer targs)
+      let fName := .mkSimple s!"F_{i + 1}"
+      fDecls := fDecls.push (fName, fun _ => pure fType)
+    withLocalDeclsD fDecls fun fs => do
+      let mut val := .const recName (rlvl :: lvls)
+      -- add parameters
+      val := mkAppN val params
+      -- add type formers
+      for typeFormer in typeFormers, below in belows do
+        -- example: (motive := fun t => PProd (motive t) (@List.below α motive t))
+        let arg ← forallTelescope (← inferType typeFormer) fun targs _ => do
+          let cType := mkAppN typeFormer targs
+          let belowType := mkAppN below targs
+          let arg ← mkPProd cType belowType
+          mkLambdaFVars targs arg
+        val := .app val arg
+      -- add minor premises
+      for minor in minors do
+        let arg ← buildBRecOnMinorPremise rlvl typeFormers belows fs (← inferType minor)
+        val := .app val arg
+      -- add indices and major premise
+      val := mkAppN val remaining
+      -- project out first component
+      val ← mkPProdFst val
+
+      -- All paramaters of `.rec` besides the `minors` become parameters of `.bRecOn`, and the `fs`
+      let below_params := params ++ typeFormers ++ remaining ++ fs
+      let type ← mkForallFVars below_params (mkAppN typeFormers[idx]! remaining)
+      val ← mkLambdaFVars below_params val
+
+      let name := if ind then mkBInductionOnName indName else mkBRecOnName indName
+      mkDefinitionValInferrringUnsafe name blps type val .abbrev
+
+  addDecl (.defnDecl decl)
+  setReducibleAttribute decl.name
+  modifyEnv fun env => markAuxRecursor env decl.name
+  modifyEnv fun env => addProtected env decl.name
+
+def mkBRecOn (declName : Name) : MetaM Unit := mkBRecOnOrBInductionOn declName false
+def mkBInductionOn (declName : Name) : MetaM Unit := mkBRecOnOrBInductionOn declName true

src/Lean/Meta/IndPredBelow.lean

@@ -434,7 +434,7 @@ partial def mkBelowMatcher
   withExistingLocalDecls (lhss.foldl (init := []) fun s v => s ++ v.fvarDecls) do
     for lhs in lhss do
       trace[Meta.IndPredBelow.match] "{lhs.patterns.map (·.toMessageData)}"
-  let res ← Match.mkMatcher { matcherName, matchType, discrInfos := mkArray (mkMatcherInput.numDiscrs + 1) {}, lhss }
+  let res ← Match.mkMatcher (exceptionIfContainsSorry := true) { matcherName, matchType, discrInfos := mkArray (mkMatcherInput.numDiscrs + 1) {}, lhss }
   res.addMatcher
   -- if a wrong index is picked, the resulting matcher can be type-incorrect.
   -- we check here, so that errors can propagate higher up the call stack.

src/Lean/Meta/Match/Match.lean

@@ -830,8 +830,12 @@ Each `AltLHS` has a list of local declarations and a list of patterns.
 The number of patterns must be the same in each `AltLHS`.
 The generated matcher has the structure described at `MatcherInfo`. The motive argument is of the form
 `(motive : (a_1 : A_1) -> (a_2 : A_2[a_1]) -> ... -> (a_n : A_n[a_1, a_2, ... a_{n-1}]) -> Sort v)`
-where `v` is a universe parameter or 0 if `B[a_1, ..., a_n]` is a proposition. -/
-def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := withCleanLCtxFor input do
+where `v` is a universe parameter or 0 if `B[a_1, ..., a_n]` is a proposition.
+
+If `exceptionIfContainsSorry := true`, then `mkMatcher` throws an exception if the auxiliary
+declarations contains a `sorry`. We use this argument to workaround a bug at `IndPredBelow.mkBelowMatcher`.
+-/
+def mkMatcher (input : MkMatcherInput) (exceptionIfContainsSorry := false) : MetaM MatcherResult := withCleanLCtxFor input do
   let ⟨matcherName, matchType, discrInfos, lhss⟩ := input
   let numDiscrs := discrInfos.size
   let numEqs := getNumEqsFromDiscrInfos discrInfos
@@ -844,6 +848,11 @@ def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := withCleanLCtxFor
   let uElim ← getLevel matchTypeBody
   let uElimGen ← if uElim == levelZero then pure levelZero else mkFreshLevelMVar
   let mkMatcher (type val : Expr) (minors : Array (Expr × Nat)) (s : State) : MetaM MatcherResult := do
+    let val ← instantiateMVars val
+    let type ← instantiateMVars type
+    if exceptionIfContainsSorry then
+      if type.hasSorry || val.hasSorry then
+        throwError "failed to create auxiliary match declaration `{matcherName}`, it contains `sorry`"
     trace[Meta.Match.debug] "matcher value: {val}\ntype: {type}"
     trace[Meta.Match.debug] "minors num params: {minors.map (·.2)}"
     /- The option `bootstrap.gen_matcher_code` is a helper hack. It is useful, for example,
@@ -857,7 +866,6 @@ def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := withCleanLCtxFor
        | negSucc n => succ n
        ```
        which is defined **before** `Int.decLt` -/
-
     let (matcher, addMatcher) ← mkMatcherAuxDefinition matcherName type val
     trace[Meta.Match.debug] "matcher levels: {matcher.getAppFn.constLevels!}, uElim: {uElimGen}"
     let uElimPos? ← getUElimPos? matcher.getAppFn.constLevels! uElimGen

src/Lean/Meta/Offset.lean

@@ -7,6 +7,8 @@ prelude
 import Lean.Data.LBool
 import Lean.Meta.InferType
 import Lean.Meta.NatInstTesters
+import Lean.Meta.NatInstTesters
+import Lean.Util.SafeExponentiation
 
 namespace Lean.Meta
 
@@ -29,6 +31,10 @@ partial def evalNat (e : Expr) : OptionT MetaM Nat := do
   | .mvar ..             => visit e
   | _                    => failure
 where
+  evalPow (b n : Expr) : OptionT MetaM Nat := do
+    let n ← evalNat n
+    guard (← checkExponent n)
+    return (← evalNat b) ^ n
   visit e := do
     match_expr e with
     | OfNat.ofNat _ n i => guard (← isInstOfNatNat i); evalNat n
@@ -48,10 +54,10 @@ where
     | Nat.mod a b => return (← evalNat a) % (← evalNat b)
     | Mod.mod _ i a b => guard (← isInstModNat i); return (← evalNat a) % (← evalNat b)
     | HMod.hMod _ _ _ i a b => guard (← isInstHModNat i); return (← evalNat a) % (← evalNat b)
-    | Nat.pow a b => return (← evalNat a) ^ (← evalNat b)
-    | NatPow.pow _ i a b => guard (← isInstNatPowNat i); return (← evalNat a) ^ (← evalNat b)
-    | Pow.pow _ _ i a b => guard (← isInstPowNat i); return (← evalNat a) ^ (← evalNat b)
-    | HPow.hPow _ _ _ i a b => guard (← isInstHPowNat i); return (← evalNat a) ^ (← evalNat b)
+    | Nat.pow a b => evalPow a b
+    | NatPow.pow _ i a b => guard (← isInstNatPowNat i); evalPow a b
+    | Pow.pow _ _ i a b => guard (← isInstPowNat i); evalPow a b
+    | HPow.hPow _ _ _ i a b => guard (← isInstHPowNat i); evalPow a b
     | _ => failure
 
 /--

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean

@@ -82,6 +82,7 @@ builtin_dsimproc [simp, seval] reducePow ((_ : Int) ^ (_ : Nat)) := fun e => do
   let_expr HPow.hPow _ _ _ _ a b ← e | return .continue
   let some v₁ ← fromExpr? a | return .continue
   let some v₂ ← Nat.fromExpr? b | return .continue
+  unless (← checkExponent v₂) do return .continue
   return .done <| toExpr (v₁ ^ v₂)
 
 builtin_simproc [simp, seval] reduceLT  (( _ : Int) < _)  := reduceBinPred ``LT.lt 4 (. < .)

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Simproc
 import Init.Data.Nat.Simproc
+import Lean.Util.SafeExponentiation
 import Lean.Meta.LitValues
 import Lean.Meta.Offset
 import Lean.Meta.Tactic.Simp.Simproc
@@ -52,7 +53,13 @@ builtin_dsimproc [simp, seval] reduceMul ((_ * _ : Nat)) := reduceBin ``HMul.hMu
 builtin_dsimproc [simp, seval] reduceSub ((_ - _ : Nat)) := reduceBin ``HSub.hSub 6 (· - ·)
 builtin_dsimproc [simp, seval] reduceDiv ((_ / _ : Nat)) := reduceBin ``HDiv.hDiv 6 (· / ·)
 builtin_dsimproc [simp, seval] reduceMod ((_ % _ : Nat)) := reduceBin ``HMod.hMod 6 (· % ·)
-builtin_dsimproc [simp, seval] reducePow ((_ ^ _ : Nat)) := reduceBin ``HPow.hPow 6 (· ^ ·)
+
+builtin_dsimproc [simp, seval] reducePow ((_ ^ _ : Nat)) := fun e => do
+  let some n ← fromExpr? e.appFn!.appArg! | return .continue
+  let some m ← fromExpr? e.appArg! | return .continue
+  unless (← checkExponent m) do return .continue
+  return .done <| toExpr (n ^ m)
+
 builtin_dsimproc [simp, seval] reduceGcd (gcd _ _)       := reduceBin ``gcd 2 gcd
 
 builtin_simproc [simp, seval] reduceLT  (( _ : Nat) < _)  := reduceBinPred ``LT.lt 4 (. < .)

src/Lean/Meta/Tactic/Simp/Rewrite.lean

@@ -123,7 +123,14 @@ private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInf
           return none
         pure <| some proof
       let rhs := (← instantiateMVars type).appArg!
-      if e == rhs then
+      /-
+      We used to use `e == rhs` in the following test.
+      However, it include unnecessary proof steps when `e` and `rhs`
+      are equal after metavariables are instantiated.
+      We are hoping the following `instantiateMVars` should not be too expensive since
+      we seldom have assigned metavariables in goals.
+      -/
+      if (← instantiateMVars e) == rhs then
         return none
       if thm.perm then
         /-

src/Lean/Meta/WHNF.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Structure
 import Lean.Util.Recognizers
+import Lean.Util.SafeExponentiation
 import Lean.Meta.GetUnfoldableConst
 import Lean.Meta.FunInfo
 import Lean.Meta.Offset
@@ -885,6 +886,13 @@ def reduceBinNatOp (f : Nat → Nat → Nat) (a b : Expr) : MetaM (Option Expr)
   trace[Meta.isDefEq.whnf.reduceBinOp] "{a} op {b}"
   return mkRawNatLit <| f a b
 
+def reducePow (a b : Expr) : MetaM (Option Expr) :=
+  withNatValue a fun a =>
+  withNatValue b fun b => OptionT.run do
+  guard (← checkExponent b)
+  trace[Meta.isDefEq.whnf.reduceBinOp] "{a} ^ {b}"
+  return mkRawNatLit <| a ^ b
+
 def reduceBinNatPred (f : Nat → Nat → Bool) (a b : Expr) : MetaM (Option Expr) := do
   withNatValue a fun a =>
   withNatValue b fun b =>
@@ -904,7 +912,7 @@ def reduceNat? (e : Expr) : MetaM (Option Expr) :=
     | ``Nat.mul => reduceBinNatOp Nat.mul a1 a2
     | ``Nat.div => reduceBinNatOp Nat.div a1 a2
     | ``Nat.mod => reduceBinNatOp Nat.mod a1 a2
-    | ``Nat.pow => reduceBinNatOp Nat.pow a1 a2
+    | ``Nat.pow => reducePow a1 a2
     | ``Nat.gcd => reduceBinNatOp Nat.gcd a1 a2
     | ``Nat.beq => reduceBinNatPred Nat.beq a1 a2
     | ``Nat.ble => reduceBinNatPred Nat.ble a1 a2

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -45,6 +45,8 @@ structure Context where
   depth          : Nat := 0
 
 structure State where
+  /-- The number of `delab` steps so far. Used by `pp.maxSteps` to stop delaboration. -/
+  steps : Nat := 0
   /-- We attach `Elab.Info` at various locations in the `Syntax` output in order to convey
   its semantics. While the elaborator emits `InfoTree`s, here we have no real text location tree
   to traverse, so we use a flattened map. -/
@@ -262,10 +264,12 @@ def withBindingBodyUnusedName {α} (d : Syntax → DelabM α) : DelabM α := do
 inductive OmissionReason
   | deep
   | proof
+  | maxSteps
 
 def OmissionReason.toString : OmissionReason → String
   | deep => "Term omitted due to its depth (see option `pp.deepTerms`)."
   | proof => "Proof omitted (see option `pp.proofs`)."
+  | maxSteps => "Term omitted due to reaching the maximum number of steps allowed for pretty printing this expression (see option `pp.maxSteps`)."
 
 def addOmissionInfo (pos : Pos) (stx : Syntax) (e : Expr) (reason : OmissionReason) : DelabM Unit := do
   let info := Info.ofOmissionInfo <| ← mkOmissionInfo stx e
@@ -361,6 +365,11 @@ partial def delabFor : Name → Delab
 
 partial def delab : Delab := do
   checkSystem "delab"
+
+  if (← get).steps ≥ (← getPPOption getPPMaxSteps) then
+    return ← omission .maxSteps
+  modify fun s => {s with steps := s.steps + 1}
+
   let e ← getExpr
 
   if ← shouldOmitExpr e then

src/Lean/PrettyPrinter/Delaborator/Options.lean

@@ -8,6 +8,11 @@ import Lean.Data.Options
 
 namespace Lean
 
+register_builtin_option pp.maxSteps : Nat := {
+  defValue := 5000
+  group    := "pp"
+  descr    := "(pretty printer) maximum number of expressions to visit, after which terms will pretty print as `⋯`"
+}
 register_builtin_option pp.all : Bool := {
   defValue := false
   group    := "pp"
@@ -162,12 +167,12 @@ register_builtin_option pp.instanceTypes : Bool := {
   descr    := "(pretty printer) when printing explicit applications, show the types of inst-implicit arguments"
 }
 register_builtin_option pp.deepTerms : Bool := {
-  defValue := true
+  defValue := false
   group    := "pp"
   descr    := "(pretty printer) display deeply nested terms, replacing them with `⋯` if set to false"
 }
 register_builtin_option pp.deepTerms.threshold : Nat := {
-  defValue := 20
+  defValue := 50
   group    := "pp"
   descr    := "(pretty printer) when `pp.deepTerms` is false, the depth at which terms start being replaced with `⋯`"
 }
@@ -188,16 +193,6 @@ register_builtin_option pp.motives.all : Bool := {
 }
 -- TODO:
 /-
-register_builtin_option g_pp_max_depth : Nat := {
-  defValue := false
-  group    := "pp"
-  descr    := "(pretty printer) maximum expression depth, after that it will use ellipsis"
-}
-register_builtin_option g_pp_max_steps : Nat := {
-  defValue := false
-  group    := "pp"
-  descr    := "(pretty printer) maximum number of visited expressions, after that it will use ellipsis"
-}
 register_builtin_option g_pp_locals_full_names : Bool := {
   defValue := false
   group    := "pp"
@@ -225,6 +220,7 @@ register_builtin_option g_pp_compact_let : Bool := {
 }
 -/
 
+def getPPMaxSteps (o : Options) : Nat := o.get pp.maxSteps.name pp.maxSteps.defValue
 def getPPAll (o : Options) : Bool := o.get pp.all.name false
 def getPPFunBinderTypes (o : Options) : Bool := o.get pp.funBinderTypes.name (getPPAll o)
 def getPPPiBinderTypes (o : Options) : Bool := o.get pp.piBinderTypes.name pp.piBinderTypes.defValue

src/Lean/Util.lean

@@ -29,3 +29,4 @@ import Lean.Util.OccursCheck
 import Lean.Util.HasConstCache
 import Lean.Util.FileSetupInfo
 import Lean.Util.Heartbeats
+import Lean.Util.SafeExponentiation

src/Lean/Util/SafeExponentiation.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.CoreM
+
+namespace Lean
+
+register_builtin_option exponentiation.threshold : Nat := {
+  defValue := 256
+  descr    := "maximum value for \
+  which exponentiation operations are safe to evaluate. When an exponent \
+  is a value greater than this threshold, the exponentiation will not be evaluated, \
+  and a warning will be logged. This helps to prevent the system from becoming \
+  unresponsive due to excessively large computations."
+}
+
+/--
+Returns `true` if `n` is `≤ exponentiation.threshold`. Otherwise,
+reports a warning and returns `false`.
+This method ensures there is at most one warning message of this kind in the message log.
+-/
+def checkExponent (n : Nat) : CoreM Bool := do
+  let threshold := exponentiation.threshold.get (← getOptions)
+  if n > threshold then
+    if (← reportMessageKind `unsafe.exponentiation) then
+      logWarning s!"exponent {n} exceeds the threshold {threshold}, exponentiation operation was not evaluated, use `set_option {exponentiation.threshold.name} <num>` to set a new threshold"
+    return false
+  else
+    return true
+
+end Lean

src/Lean/Util/Trace.lean

@@ -164,7 +164,7 @@ register_builtin_option trace.profiler.threshold : Nat := {
     traces below threshold will not be activated"
 }
 
-register_builtin_option trace.profiler.useHearbeats : Bool := {
+register_builtin_option trace.profiler.useHeartbeats : Bool := {
   defValue := false
   group    := "profiler"
   descr    :=
@@ -190,7 +190,7 @@ invocations, which is the common case."
 
 @[inline] private def withStartStop [Monad m] [MonadLiftT BaseIO m] (opts : Options) (act : m α) :
     m (α × Float × Float) := do
-  if trace.profiler.useHearbeats.get opts then
+  if trace.profiler.useHeartbeats.get opts then
     let start ← IO.getNumHeartbeats
     let a ← act
     let stop ← IO.getNumHeartbeats
@@ -202,7 +202,7 @@ invocations, which is the common case."
     return (a, start.toFloat / 1000000000, stop.toFloat / 1000000000)
 
 @[inline] def trace.profiler.threshold.unitAdjusted (o : Options) : Float :=
-  if trace.profiler.useHearbeats.get o then
+  if trace.profiler.useHeartbeats.get o then
     (trace.profiler.threshold.get o).toFloat
   else
     -- milliseconds to seconds

src/kernel/environment.cpp

@@ -299,6 +299,12 @@ extern "C" LEAN_EXPORT object * lean_add_decl(object * env, size_t max_heartbeat
         });
 }
 
+extern "C" LEAN_EXPORT object * lean_add_decl_without_checking(object * env, object * decl) {
+    return catch_kernel_exceptions<environment>([&]() {
+            return environment(env).add(declaration(decl, true), false);
+        });
+}
+
 void environment::for_each_constant(std::function<void(constant_info const & d)> const & f) const {
     smap_foreach(cnstr_get(raw(), 1), [&](object *, object * v) {
             constant_info cinfo(v, true);

src/kernel/type_checker.cpp

@@ -595,6 +595,18 @@ template<typename F> optional<expr> type_checker::reduce_bin_nat_op(F const & f,
     return some_expr(mk_lit(literal(nat(f(v1.raw(), v2.raw())))));
 }
 
+#define ReducePowMaxExp 1<<24 // TODO: make it configurable
+
+optional<expr> type_checker::reduce_pow(expr const & e) {
+    expr arg1 = whnf(app_arg(app_fn(e)));
+    expr arg2 = whnf(app_arg(e));
+    if (!is_nat_lit_ext(arg2)) return none_expr();
+    nat v1 = get_nat_val(arg1);
+    nat v2 = get_nat_val(arg2);
+    if (v2 > nat(ReducePowMaxExp)) return none_expr();
+    return some_expr(mk_lit(literal(nat(nat_pow(v1.raw(), v2.raw())))));
+}
+
 template<typename F> optional<expr> type_checker::reduce_bin_nat_pred(F const & f, expr const & e) {
     expr arg1 = whnf(app_arg(app_fn(e)));
     if (!is_nat_lit_ext(arg1)) return none_expr();
@@ -622,7 +634,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_pow) return reduce_pow(e);
         if (f == *g_nat_gcd) return reduce_bin_nat_op(nat_gcd, 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);

src/kernel/type_checker.h

@@ -101,6 +101,7 @@ private:
 
     template<typename F> optional<expr> reduce_bin_nat_op(F const & f, expr const & e);
     template<typename F> optional<expr> reduce_bin_nat_pred(F const & f, expr const & e);
+    optional<expr> reduce_pow(expr const & e);
     optional<expr> reduce_nat(expr const & e);
 public:
     type_checker(state & st, local_ctx const & lctx, definition_safety ds = definition_safety::safe);

src/lake/Lake/Build/Executable.lean

@@ -13,10 +13,18 @@ The build function definition for a Lean executable.
 
 def LeanExe.recBuildExe (self : LeanExe) : FetchM (BuildJob FilePath) :=
   withRegisterJob s!"{self.name}" do
+  /-
+  Remark: We must build the root before we fetch the transitive imports
+  so that errors in the import block of transitive imports will not kill this
+  job before the root is built.
+  -/
+  let mut linkJobs := #[]
+  for facet in self.root.nativeFacets self.supportInterpreter do
+    linkJobs := linkJobs.push <| ← fetch <| self.root.facet facet.name
   let imports ← self.root.transImports.fetch
-  let mut linkJobs := #[← self.root.o.fetch]
-  for mod in imports do for facet in mod.nativeFacets self.supportInterpreter do
-    linkJobs := linkJobs.push <| ← fetch <| mod.facet facet.name
+  for mod in imports do
+    for facet in mod.nativeFacets self.supportInterpreter 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

src/lake/Lake/Build/Module.lean

@@ -94,7 +94,7 @@ Recursively build a module's dependencies, including:
 * Shared libraries (e.g., `extern_lib` targets or precompiled modules)
 * `extraDepTargets` of its library
 -/
-def Module.recBuildDeps (mod : Module) : FetchM (BuildJob (SearchPath × Array FilePath)) := do
+def Module.recBuildDeps (mod : Module) : FetchM (BuildJob (SearchPath × Array FilePath)) := ensureJob do
   let extraDepJob ← mod.lib.extraDep.fetch
 
   /-
@@ -102,18 +102,17 @@ def Module.recBuildDeps (mod : Module) : FetchM (BuildJob (SearchPath × Array F
   precompiled imports so that errors in the import block of transitive imports
   will not kill this job before the direct imports are built.
   -/
-  let directImports ← try mod.imports.fetch
-    catch errPos => return Job.error (← takeLogFrom errPos)
+  let directImports ← mod.imports.fetch
   let importJob ← BuildJob.mixArray <| ← directImports.mapM fun imp => do
     if imp.name = mod.name then
       logError s!"{mod.leanFile}: module imports itself"
     imp.olean.fetch
-  let precompileImports ← try mod.precompileImports.fetch
-    catch errPos => return Job.error (← takeLogFrom errPos)
+  let precompileImports ← if mod.shouldPrecompile then
+    mod.transImports.fetch else mod.precompileImports.fetch
   let modLibJobs ← precompileImports.mapM (·.dynlib.fetch)
-  let pkgs := precompileImports.foldl (·.insert ·.pkg)
-    OrdPackageSet.empty |>.insert mod.pkg |>.toArray
-  let (externJobs, libDirs) ← recBuildExternDynlibs pkgs
+  let pkgs := precompileImports.foldl (·.insert ·.pkg) OrdPackageSet.empty
+  let pkgs := if mod.shouldPrecompile then pkgs.insert mod.pkg else pkgs
+  let (externJobs, libDirs) ← recBuildExternDynlibs pkgs.toArray
   let externDynlibsJob ← BuildJob.collectArray externJobs
   let modDynlibsJob ← BuildJob.collectArray modLibJobs
 

src/lake/Lake/CLI/Init.lean

@@ -126,8 +126,7 @@ package {repr pkgName} where
   ]
   -- add any additional package configuration options here
 
-require mathlib from git
-  \"https://github.com/leanprover-community/mathlib4.git\"
+require \"leanprover-community\" / \"mathlib\"
 
 @[default_target]
 lean_lib {libRoot} where
@@ -143,7 +142,7 @@ pp.unicode.fun = true # pretty-prints `fun a ↦ b`
 
 [[require]]
 name = \"mathlib\"
-git = \"https://github.com/leanprover-community/mathlib4.git\"
+scope = \"leanprover-community\"
 
 [[lean_lib]]
 name = {repr libRoot}

src/lake/Lake/CLI/Main.lean

@@ -201,12 +201,12 @@ def verifyInstall (opts : LakeOptions) : ExceptT CliError MainM PUnit := do
 def parseScriptSpec (ws : Workspace) (spec : String) : Except CliError Script :=
   match spec.splitOn "/" with
   | [scriptName] =>
-    match ws.findScript? scriptName.toName with
+    match ws.findScript? (stringToLegalOrSimpleName scriptName) with
     | some script => return script
     | none => throw <| CliError.unknownScript spec
   | [pkg, scriptName] => do
     let pkg ← parsePackageSpec ws pkg
-    match pkg.scripts.find? scriptName.toName with
+    match pkg.scripts.find? (stringToLegalOrSimpleName scriptName) with
     | some script => return script
     | none => throw <| CliError.unknownScript spec
   | _ => throw <| CliError.invalidScriptSpec spec

src/lake/Lake/CLI/Translate/Lean.lean

@@ -163,16 +163,19 @@ protected def LeanExeConfig.mkSyntax
   `(leanExeDecl|$[$attrs?:attributes]? lean_exe $(mkIdent cfg.name):ident $[$declVal?]?)
 
 protected def Dependency.mkSyntax (cfg : Dependency) : RequireDecl := Unhygienic.run do
-  let src ←
-    match cfg.src with
+  let src? ← cfg.src?.mapM fun src =>
+    match src with
     | .path dir =>
       `(fromSource|$(quote dir):term)
     | .git url rev? subDir? =>
       `(fromSource|git $(quote url) $[@ $(rev?.map quote)]? $[/ $(subDir?.map quote)]?)
+  let ver? := cfg.version?.map quote
+  let scope? := if cfg.scope.isEmpty then none else some (quote cfg.scope)
   let opts? := if cfg.opts.isEmpty then none else some <| Unhygienic.run do
     cfg.opts.foldM (init := mkCIdent ``NameMap.empty) fun stx opt val =>
       `($stx |>.insert $(quote opt) $(quote val))
-  `(requireDecl|require $(mkIdent cfg.name):ident from $src $[with $opts?]?)
+  `(requireDecl|require $[$scope? /]? $(mkIdent cfg.name):ident $[@ $ver?]?
+    $[from $src?]? $[with $opts?]?)
 
 /-! ## Root Encoder -/
 

src/lake/Lake/CLI/Translate/Toml.lean

@@ -105,14 +105,20 @@ protected def LeanExeConfig.toToml (cfg : LeanExeConfig) (t : Table  := {}) : Ta
 instance : ToToml LeanExeConfig := ⟨(toToml ·.toToml)⟩
 
 protected def Dependency.toToml (dep : Dependency) (t : Table  := {}) : Table :=
-  let t := t.insert `name dep.name
+  let t := t
+    |>.insert `name dep.name
+    |>.insertD `scope dep.scope ""
+    |>.smartInsert `version dep.version?
   let t :=
-    match dep.src with
-    | .path dir => t.insert `path (toToml dir)
-    | .git url rev subDir? =>
-      t.insert `git url
-      |>.smartInsert `rev rev
-      |>.smartInsert `subDir subDir?
+    if let some src := dep.src? then
+      match src with
+      | .path dir => t.insert `path (toToml dir)
+      | .git url rev subDir? =>
+        t.insert `git url
+        |>.smartInsert `rev rev
+        |>.smartInsert `subDir subDir?
+    else
+      t
   t.smartInsert `options <| dep.opts.fold (·.insert · ·) Table.empty
 
 instance : ToToml Dependency := ⟨(toToml ·.toToml)⟩

src/lake/Lake/Config/Dependency.lean

@@ -41,13 +41,27 @@ structure Dependency where
   -/
   name : Name
   /--
+  An additional qualifier used to distinguish packages of the same
+  name in a Lake registry. On Reservoir, this is the package owner.
+  -/
+  scope : String
+  /--
+  The target version of the dependency.
+  A Git revision can be specified with the syntax `git#<rev>`.
+  -/
+  version? : Option String
+  /--
   The source of a dependency.
+  If none, looks up the dependency in the default registry (e.g., Reservoir).
   See the documentation of `DependencySrc` for supported sources.
   -/
-  src  : DependencySrc
+  src?  : Option DependencySrc
   /--
   Arguments to pass to the dependency's package configuration.
   -/
-  opts : NameMap String := {}
+  opts : NameMap String
+  deriving Inhabited
 
-deriving Inhabited
+/-- The full name of a dependency (i.e., `<scope>/<name>`)-/
+def Dependency.fullName (dep : Dependency) : String :=
+  s!"{dep.scope}/{dep.name.toString}"

src/lake/Lake/Config/Env.lean

@@ -25,6 +25,8 @@ structure Env where
   lean : LeanInstall
   /-- The Elan installation (if any) of the environment. -/
   elan? : Option ElanInstall
+  /-- The Reservoir API endpoint URL (e.g., `https://reservoir.lean-lang.org/api`). -/
+  reservoirApiUrl : String
   /-- Overrides the detected Lean's githash as the string Lake uses for Lean traces. -/
   githashOverride : String
   /-- A name-to-URL mapping of URL overrides for the named packages. -/
@@ -44,10 +46,12 @@ structure Env where
 namespace Env
 
 /-- Compute an `Lake.Env` object from the given installs and set environment variables. -/
-def compute (lake : LakeInstall) (lean : LeanInstall) (elan? : Option ElanInstall) : EIO String Env :=
+def compute (lake : LakeInstall) (lean : LeanInstall) (elan? : Option ElanInstall) : EIO String Env := do
+  let reservoirBaseUrl ← getUrlD "RESERVOIR_API_BASE_URL" "https://reservoir.lean-lang.org/api"
   return {
     lake, lean, elan?,
     pkgUrlMap := ← computePkgUrlMap
+    reservoirApiUrl := ← getUrlD "RESERVOIR_API_URL" s!"{reservoirBaseUrl}/v1"
     githashOverride := (← IO.getEnv "LEAN_GITHASH").getD ""
     initToolchain := (← IO.getEnv "ELAN_TOOLCHAIN").getD ""
     initLeanPath := ← getSearchPath "LEAN_PATH",
@@ -61,6 +65,11 @@ where
     match Json.parse urlMapStr |>.bind fromJson? with
     | .ok urlMap => return urlMap
     | .error e => throw s!"'LAKE_PKG_URL_MAP' has invalid JSON: {e}"
+  @[macro_inline] getUrlD var default := do
+    if let some url ← IO.getEnv var then
+      return if url.back == '/' then url.dropRight 1 else url
+    else
+       return default
 
 /--
 The string Lake uses to identify Lean in traces.

src/lake/Lake/DSL/Require.lean

@@ -59,16 +59,26 @@ syntax fromClause :=
 syntax withClause :=
   " with " term
 
+/--
+The version of the package to lookup in Lake's package index.
+A Git revision can be specified via `"git#<rev>"`.
+-/
+syntax verSpec :=
+  " @ " term:max
+
+syntax depName :=
+  atomic(str " / ")? identOrStr
+
 syntax depSpec :=
-  identOrStr fromClause (withClause)?
+  depName (verSpec)? (fromClause)? (withClause)?
 
 @[inline] private def quoteOptTerm [Monad m] [MonadQuotation m] (term? : Option Term) : m Term :=
   if let some term := term? then withRef term `(some $term) else `(none)
 
 def expandDepSpec (stx : TSyntax ``depSpec) (doc? : Option DocComment) : MacroM Command := do
-  let `(depSpec| $nameStx from $src $[with $opts?]?) := stx
+  let `(depSpec| $fullNameStx $[@ $ver?]? $[from $src?]? $[with $opts?]?) := stx
     | Macro.throwErrorAt stx "ill-formed require syntax"
-  let src ←
+  let src? ← src?.mapM fun src =>
     match src with
     | `(fromSource|git%$tk $url $[@ $rev?]? $[/ $subDir?]?) => withRef tk do
       let rev ← quoteOptTerm rev?
@@ -77,10 +87,18 @@ def expandDepSpec (stx : TSyntax ``depSpec) (doc? : Option DocComment) : MacroM
     | `(fromSource|$path:term) => withRef src do
       ``(DependencySrc.path $path)
     | _ => Macro.throwErrorAt src "ill-formed from syntax"
+  let `(depName|$[$scope? /]? $nameStx) := fullNameStx
+    | Macro.throwErrorAt fullNameStx "ill-formed name syntax"
+  let scope :=
+    match scope? with
+    | some scope => scope
+    | none => Syntax.mkStrLit "" (.fromRef fullNameStx)
   let name := expandIdentOrStrAsIdent nameStx
   `($[$doc?:docComment]? @[package_dep] def $name : $(mkCIdent ``Dependency) := {
     name :=  $(quote name.getId),
-    src := $src,
+    scope := $scope,
+    version? := $(← quoteOptTerm ver?),
+    src? := $(← quoteOptTerm src?),
     opts := $(opts?.getD <| ← `({})),
   })
 
@@ -88,13 +106,20 @@ def expandDepSpec (stx : TSyntax ``depSpec) (doc? : Option DocComment) : MacroM
 Adds a new package dependency to the workspace. The general syntax is:
 
 ```
-require <pkg-name> from <source> [with <options>]
+require ["<scope>" /] <pkg-name> [@ <version>]
+  [from <source>] [with <options>]
 ```
 
 The `from` clause tells Lake where to locate the dependency.
 See the `fromClause` syntax documentation (e.g., hover over it) to see
 the different forms this clause can take.
 
+Without a `from` clause, Lake will lookup the package in the default
+registry (i.e., Reservoir) and use the information there to download the
+package at the specified `version`. The optional `scope` is used to
+disambiguate which package with `pkg-name` to lookup. In Reservoir, this scope
+is the package owner (e.g., `leanprover` of `@leanprover/doc-gen4`).
+
 The `with` clause specifies a `NameMap String` of Lake options
 used to configure the dependency. This is equivalent to passing `-K`
 options to the dependency on the command line.

src/lake/Lake/DSL/Script.lean

@@ -15,7 +15,7 @@ namespace Lake.DSL
 open Lean Parser Command
 
 syntax scriptDeclSpec :=
-  ident (ppSpace simpleBinder)? (declValSimple <|> declValDo)
+  identOrStr (ppSpace simpleBinder)? (declValSimple <|> declValDo)
 
 /--
 Define a new Lake script for the package.
@@ -37,9 +37,10 @@ scoped syntax (name := scriptDecl)
 
 @[macro scriptDecl]
 def expandScriptDecl : Macro
-| `($[$doc?]? $[$attrs?]? script%$kw $id:ident $[$args?]? do $seq $[$wds?:whereDecls]?) => do
-  `($[$doc?]? $[$attrs?]? script%$kw  $id:ident $[$args?]? := do $seq $[$wds?:whereDecls]?)
-| `($[$doc?]? $[$attrs?]? script%$kw  $id:ident $[$args?]? := $defn $[$wds?:whereDecls]?) => withRef kw do
+| `($[$doc?]? $[$attrs?]? script%$kw $name $[$args?]? do $seq $[$wds?:whereDecls]?) => do
+  `($[$doc?]? $[$attrs?]? script%$kw $name $[$args?]? := do $seq $[$wds?:whereDecls]?)
+| `($[$doc?]? $[$attrs?]? script%$kw $name $[$args?]? := $defn $[$wds?:whereDecls]?) => withRef kw do
+  let id := expandIdentOrStrAsIdent name
   let args ← expandOptSimpleBinder args?
   let attrs := #[← `(Term.attrInstance| «script»)] ++ expandAttrs attrs?
   `($[$doc?]? @[$attrs,*] def $id : ScriptFn := fun $args => $defn $[$wds?:whereDecls]?)

src/lake/Lake/Load/Manifest.lean

@@ -47,8 +47,9 @@ That is, Lake ignores the `-` suffix.
 
 **v1.x.x** (versioned by a string)
 - `"1.0.0"`: Switches to a semantic versioning scheme
+- `"1.1.0"`: Add optional `scope` package entry field
 -/
-@[inline] def Manifest.version : LeanVer := v!"1.0.0"
+@[inline] def Manifest.version : LeanVer := v!"1.1.0"
 
 /-- Manifest version `0.6.0` package entry. For backwards compatibility. -/
 inductive PackageEntryV6
@@ -79,6 +80,7 @@ inductive PackageEntrySrc
 /-- An entry for a package stored in the manifest. -/
 structure PackageEntry where
   name : Name
+  scope : String := ""
   inherited : Bool
   configFile : FilePath := defaultConfigFile
   manifestFile? : Option FilePath := none
@@ -90,6 +92,7 @@ namespace PackageEntry
 protected def toJson (entry : PackageEntry) : Json :=
   let fields := [
     ("name", toJson entry.name),
+    ("scope", toJson entry.scope),
     ("configFile" , toJson entry.configFile),
     ("manifestFile", toJson entry.manifestFile?),
     ("inherited", toJson entry.inherited),
@@ -114,6 +117,7 @@ instance : ToJson PackageEntry := ⟨PackageEntry.toJson⟩
 protected def fromJson? (json : Json) : Except String PackageEntry := do
   let obj ← JsonObject.fromJson? json |>.mapError (s!"package entry: {·}")
   let name ← obj.get "name" |>.mapError (s!"package entry: {·}")
+  let scope ← obj.getD "scope" ""
   try
     let type ← obj.get "type"
     let inherited ← obj.get "inherited"
@@ -133,7 +137,7 @@ protected def fromJson? (json : Json) : Except String PackageEntry := do
       | _ =>
         throw s!"unknown package entry type '{type}'"
     return {
-      name, inherited,
+      name, scope, inherited,
       configFile, manifestFile? := manifestFile, src
       : PackageEntry
     }

src/lake/Lake/Load/Materialize.lean

@@ -7,6 +7,7 @@ import Lake.Util.Git
 import Lake.Load.Manifest
 import Lake.Config.Dependency
 import Lake.Config.Package
+import Lake.Reservoir
 
 open System Lean
 
@@ -101,30 +102,52 @@ For Git dependencies, updates it to the latest input revision.
 def Dependency.materialize
   (dep : Dependency) (inherited : Bool)
   (lakeEnv : Env) (wsDir relPkgsDir relParentDir : FilePath)
-: LogIO MaterializedDep :=
-  match dep.src with
-  | .path dir =>
-    let relPkgDir := relParentDir / dir
-    return {
-      relPkgDir
-      remoteUrl? := none
-      manifestEntry := mkEntry <| .path relPkgDir
-    }
-  | .git url inputRev? subDir? => do
-    let sname := dep.name.toString (escape := false)
-    let relGitDir := relPkgsDir / sname
-    let repo := GitRepo.mk (wsDir / relGitDir)
-    let materializeUrl := lakeEnv.pkgUrlMap.find? dep.name |>.getD url
-    materializeGitRepo sname repo materializeUrl inputRev?
-    let rev ← repo.getHeadRevision
-    let relPkgDir := match subDir? with | .some subDir => relGitDir / subDir | .none => relGitDir
-    return {
-      relPkgDir
-      remoteUrl? := Git.filterUrl? url
-      manifestEntry := mkEntry <| .git url rev inputRev? subDir?
-    }
+: LogIO MaterializedDep := do
+  if let some src := dep.src? then
+    match src with
+    | .path dir =>
+      let relPkgDir := relParentDir / dir
+      return {
+        relPkgDir
+        remoteUrl? := none
+        manifestEntry := mkEntry <| .path relPkgDir
+      }
+    | .git url inputRev? subDir? => do
+      let sname := dep.name.toString (escape := false)
+      let repoUrl? := Git.filterUrl? url
+      materializeGit sname (relPkgsDir / sname) url repoUrl? inputRev? subDir?
+  else
+    if dep.scope.isEmpty then
+      error s!"{dep.name}: ill-formed dependency: \
+        dependency is missing a source and is missing a scope for Reservoir"
+    let verRev? ← dep.version?.mapM fun ver =>
+      if ver.startsWith "git#" then
+        return ver.drop 4
+      else
+        error s!"{dep.name} unsupported dependency version format '{ver}' (should be \"git#>rev>\")"
+    let depName := dep.name.toString (escape := false)
+    let some pkg ← fetchReservoirPkg? lakeEnv dep.scope depName
+      | error s!"{dep.scope}/{depName}: could not materialize package: \
+        dependency has no explicit source and was not found on Reservoir"
+    let relPkgDir := relPkgsDir / pkg.name
+    match pkg.gitSrc? with
+    | some (.git _ url githubUrl? defaultBranch? subDir?) =>
+      materializeGit pkg.fullName relPkgDir url githubUrl? (verRev? <|> defaultBranch?) subDir?
+    | _ => error s!"{pkg.fullName}: Git source not found on Reservoir"
 where
-  mkEntry src : PackageEntry := {name := dep.name, inherited, src}
+  mkEntry src : PackageEntry :=
+    {name := dep.name, scope := dep.scope, inherited, src}
+  materializeGit name relPkgDir gitUrl remoteUrl? inputRev? subDir? : LogIO MaterializedDep := do
+    let repo := GitRepo.mk (wsDir / relPkgDir)
+    let gitUrl := lakeEnv.pkgUrlMap.find? dep.name |>.getD gitUrl
+    materializeGitRepo name repo gitUrl inputRev?
+    let rev ← repo.getHeadRevision
+    let relPkgDir := if let some subDir := subDir? then relPkgDir / subDir else relPkgDir
+    return {
+      relPkgDir
+      remoteUrl? := remoteUrl?
+      manifestEntry := mkEntry <| .git gitUrl rev inputRev? subDir?
+    }
 
 /--
 Materializes a manifest package entry, cloning and/or checking it out as necessary.

src/lake/Lake/Load/Resolve.lean

@@ -265,8 +265,9 @@ def validateManifest
       logWarning <|
         s!"manifest out of date: {what} of dependency '{dep.name}' changed; \
         use `lake update {dep.name}` to update it"
-    if let .some entry := pkgEntries.find? dep.name then
-    match dep.src, entry.src with
+    let some src := dep.src? | return
+    let some entry := pkgEntries.find? dep.name | return
+    match src, entry.src with
     | .git (url := url) (rev := rev) .., .git (url := url') (inputRev? := rev')  .. =>
       if url ≠ url' then warnOutOfDate "git url"
       if rev ≠ rev' then warnOutOfDate "git revision"

src/lake/Lake/Load/Toml.lean

@@ -235,22 +235,31 @@ instance : DecodeToml DependencySrc := ⟨fun v => do DependencySrc.decodeToml (
 
 protected def Dependency.decodeToml (t : Table) (ref := Syntax.missing) : Except (Array DecodeError) Dependency := ensureDecode do
   let name  ← stringToLegalOrSimpleName <$> t.tryDecode `name ref
-  let src : DependencySrc ← id do
+  let rev? ← t.tryDecode? `rev
+  let src? : Option DependencySrc ← id do
     if let some dir ← t.tryDecode? `path then
-      return .path dir
+      return some <| .path dir
     else if let some g := t.find? `git then
       match g with
       | .string _ url =>
-        return .git url (← t.tryDecode? `rev) (← t.tryDecode? `subDir)
+        return some <| .git url rev? (← t.tryDecode? `subDir)
       | .table ref t =>
-        return .git (← t.tryDecode `url ref) (← t.tryDecode? `rev) (← t.tryDecode? `subDir)
+        return some <| .git (← t.tryDecode `url ref) rev? (← t.tryDecode? `subDir)
       | _ =>
         modify (·.push <| .mk g.ref "expected string or table")
         return default
     else
-      t.tryDecode `source ref
+      t.tryDecode? `source
+  let scope ← t.tryDecodeD `scope ""
+  let version? ← id do
+    if let some ver ← t.tryDecode? `version then
+      return some ver
+    else if let some rev := rev? then
+      return if src?.isSome then none else some s!"git#{rev}"
+    else
+      return none
   let opts ← t.tryDecodeD `options {}
-  return {name, src, opts}
+  return {name, scope, version?, src?, opts}
 
 instance : DecodeToml Dependency := ⟨fun v => do Dependency.decodeToml (← v.decodeTable) v.ref⟩
 

src/lake/Lake/Reservoir.lean

@@ -0,0 +1,203 @@
+/-
+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.Log
+import Lake.Util.Proc
+import Lake.Util.JsonObject
+import Lake.Config.Env
+
+/-! # Package Registries
+
+This module contains definitions for fetching Lake package information from
+a online registry (e.g., Reservoir).
+-/
+
+open System Lean
+
+namespace Lake
+
+/--
+Package source information from a Lake registry (e.g., Reservoir).
+Only contains the subset of fields useful to Lake.
+-/
+inductive RegistrySrc
+| git (data : JsonObject) (url : String)
+  (githubUrl? defaultBranch? : Option String) (subDir? : Option FilePath)
+| other (data : JsonObject)
+deriving Inhabited
+
+namespace RegistrySrc
+
+def isGit (src : RegistrySrc) : Bool :=
+  match src with
+  | .git  .. => true
+  | .other .. => false
+
+def data (src : RegistrySrc) : JsonObject :=
+  match src with
+  | .git (data := data) .. => data
+  | .other data => data
+
+protected def toJson (src : RegistrySrc) : Json :=
+  src.data
+
+instance : ToJson RegistrySrc := ⟨RegistrySrc.toJson⟩
+
+protected def fromJson? (val : Json) : Except String RegistrySrc := do
+  try
+    let obj ← JsonObject.fromJson? val
+    if let some url ← obj.get? "gitUrl" then
+      let githubUrl? ← (← obj.get? "host").bindM fun host =>
+        if host == "github" then obj.get? "repoUrl" else pure none
+      let defaultBranch? ← obj.get? "defaultBranch"
+      let subDir? ← obj.get? "subDir"
+      return .git obj url githubUrl? defaultBranch? subDir?
+    else
+      return .other obj
+  catch e =>
+    throw s!"invalid registry source: {e}"
+
+instance : FromJson RegistrySrc := ⟨RegistrySrc.fromJson?⟩
+
+end RegistrySrc
+
+/--
+Package metadata from a Lake registry (e.g., Reservoir).
+Only contains the subset of fields useful to Lake.
+-/
+structure RegistryPkg where
+  name : String
+  fullName : String
+  sources : Array RegistrySrc
+  data : Json
+  deriving Inhabited
+
+namespace RegistryPkg
+
+def gitSrc? (pkg : RegistryPkg) : Option RegistrySrc :=
+  pkg.sources.find? (·.isGit)
+
+protected def toJson (src : RegistryPkg) : Json :=
+  src.data
+
+instance : ToJson RegistryPkg := ⟨RegistryPkg.toJson⟩
+
+protected def fromJson? (val : Json) : Except String RegistryPkg := do
+  try
+    let obj ← JsonObject.fromJson? val
+    let name ← obj.get "name"
+    let fullName ← obj.get "fullName"
+    let sources ← (← obj.getD "sources" #[]).mapM fromJson?
+    return {data := obj, name, fullName, sources}
+  catch e =>
+    throw s!"invalid registry package: {e}"
+
+instance : FromJson RegistryPkg := ⟨RegistryPkg.fromJson?⟩
+
+end RegistryPkg
+
+def hexEncodeByte (b : UInt8) : Char :=
+  if b = 0 then '0' else
+  if b = 1 then '1' else
+  if b = 2 then '2' else
+  if b = 3 then '3' else
+  if b = 4 then '4' else
+  if b = 5 then '5' else
+  if b = 6 then '6' else
+  if b = 7 then '7' else
+  if b = 8 then '8' else
+  if b = 9 then '9' else
+  if b = 0xa then 'A' else
+  if b = 0xb then 'B' else
+  if b = 0xc then 'C' else
+  if b = 0xd then 'D' else
+  if b = 0xe then 'E' else
+  if b = 0xf then 'F' else
+  '*'
+
+/-- Encode a byte as a URI escape code (e.g., `%20`). -/
+def uriEscapeByte (b : UInt8) (s := "") : String :=
+  s.push '%' |>.push (hexEncodeByte <| b >>> 4) |>.push (hexEncodeByte <| b &&& 0xF)
+
+@[specialize] def utf8EncodeCharM [Monad m] (c : Char) (f : σ → UInt8 → m σ) (init : σ) : m σ := do
+  let v := c.val
+  let s ← f init <| v.toUInt8 &&& 0x3f ||| 0x80
+  if v ≤ 0x7f then return s
+  let s ← f s <| (v >>>  6).toUInt8 &&& 0x1f ||| 0xc0
+  if v ≤ 0x7ff then return s
+  let s ← f s <| (v >>> 12).toUInt8 &&& 0x0f ||| 0xe0
+  if v ≤ 0xffff then return s
+  f s <| (v >>> 18).toUInt8 &&& 0x07 ||| 0xf0
+
+/-- Encode a character as a sequence of URI escape codes representing its UTF8 encoding. -/
+def uriEscapeChar (c : Char) (s := "") : String :=
+  Id.run <| utf8EncodeCharM c (init := s) fun s b => uriEscapeByte b s
+
+/-- A URI unreserved mark as specified in [RFC2396](https://datatracker.ietf.org/doc/html/rfc2396#section-2.3). -/
+def isUriUnreservedMark (c : Char)  : Bool :=
+  c matches '-' | '_' | '.' | '!' | '~' | '*' | '\'' | '(' | ')'
+
+/-- Encodes anything but a URI unreserved character as a URI escape sequences. -/
+def uriEncodeChar (c : Char) (s := "") : String :=
+  if c.isAlphanum || isUriUnreservedMark c then
+    s.push c
+  else
+    uriEscapeChar c s
+
+/-- Encodes a string as an ASCII URI component, escaping special characters (and unicode). -/
+def uriEncode (s : String) : String :=
+  s.foldl (init := "") fun s c => uriEncodeChar c s
+
+def getUrl (url : String) (headers : Array String := #[]) : LogIO String := do
+  let args := #["-s", "-L"]
+  let args := headers.foldl (init := args) (· ++ #["-H", ·])
+  captureProc {cmd := "curl", args := args.push url}
+
+/-- A Reservoir API response object. -/
+inductive ReservoirResp (α : Type u)
+| data (a : α)
+| error (status : Nat) (message : String)
+
+protected def ReservoirResp.fromJson? [FromJson α] (val : Json) : Except String (ReservoirResp α) := do
+  let obj ← JsonObject.fromJson? val
+  if let some (err : JsonObject) ← obj.get? "error" then
+    let status ← err.get "status"
+    let message ← err.get "message"
+    return .error status message
+  else
+    .data <$> fromJson? val
+
+instance [FromJson α] : FromJson (ReservoirResp α) := ⟨ReservoirResp.fromJson?⟩
+
+def fetchReservoirPkg? (lakeEnv : Lake.Env) (owner pkg : String) : LogIO (Option RegistryPkg) := do
+  let url := s!"{lakeEnv.reservoirApiUrl}/packages/{uriEncode owner}/{uriEncode pkg}"
+  let out ←
+    try
+      getUrl url #[
+        "X-Reservoir-Api-Version:1.0.0",
+        "X-Lake-Registry-Api-Version:0.1.0"
+      ]
+    catch _ =>
+      logError s!"{owner}/{pkg}: Reservoir lookup failed"
+      return none
+  match Json.parse out >>= fromJson? with
+  | .ok json =>
+    match fromJson? json with
+    | .ok (resp : ReservoirResp RegistryPkg) =>
+      match resp with
+      | .data pkg =>
+        return pkg
+      | .error status msg =>
+        if status == 404 then
+          return none
+        else
+          logError s!"{owner}/{pkg}: Reservoir lookup failed: {msg}"
+          return none
+    | .error e =>
+      logError s!"{owner}/{pkg}: Reservoir lookup failed; server returned unsupported JSON: {e}"
+      return none
+  | .error e =>
+    logError s!"{owner}/{pkg}: Reservoir lookup failed; server returned invalid JSON: {e}"
+    return none

src/lake/Lake/Util/JsonObject.lean

@@ -26,6 +26,7 @@ namespace JsonObject
 @[inline] protected def toJson (obj : JsonObject) : Json :=
   .obj obj
 
+instance : Coe JsonObject Json := ⟨Json.obj⟩
 instance : ToJson JsonObject := ⟨JsonObject.toJson⟩
 
 @[inline] protected def fromJson? (json : Json) : Except String JsonObject :=
@@ -33,8 +34,14 @@ instance : ToJson JsonObject := ⟨JsonObject.toJson⟩
 
 instance : FromJson JsonObject := ⟨JsonObject.fromJson?⟩
 
-@[inline] nonrec def erase (obj : JsonObject) (prop : String) : JsonObject :=
-  obj.erase compare prop
+@[inline] nonrec def insert [ToJson α] (obj : JsonObject) (prop : String) (val : α) : JsonObject :=
+  obj.insert compare prop (toJson val)
+
+@[inline] def insertSome [ToJson α] (obj : JsonObject) (prop : String) (val? : Option α) : JsonObject :=
+  if let some val := val? then obj.insert prop val else obj
+
+nonrec def erase (obj : JsonObject) (prop : String) : JsonObject :=
+  inline <| obj.erase compare prop
 
 @[inline] def getJson? (obj : JsonObject) (prop : String) : Option Json :=
   obj.find compare prop
@@ -49,5 +56,5 @@ instance : FromJson JsonObject := ⟨JsonObject.fromJson?⟩
   | none => pure none
   | some val => fromJson? val |>.mapError (s!"{prop}: {·}")
 
-@[inline] def getD  [FromJson α] (obj : JsonObject) (prop : String) (default : α) : Except String α :=
-  (Option.getD · default) <$> obj.get? prop
+@[macro_inline] def getD [FromJson α] (obj : JsonObject) (prop : String) (default : α) : Except String α := do
+  return (← obj.get? prop).getD default

src/lake/README.md

@@ -323,13 +323,12 @@ In all of these, the object parameter and its type specifier are optional and th
 
 ## Adding Dependencies
 
-Lake packages can have dependencies. Dependencies are other Lake packages the current package needs in order to function. They can be sourced directly from a local folder (e.g., a subdirectory of the package) or come from remote Git repositories. For example, one can depend on [mathlib](https://github.com/leanprover-community/mathlib4) like so:
+Lake packages can have dependencies. Dependencies are other Lake packages the current package needs in order to function. They can be sourced directly from a local folder (e.g., a subdirectory of the package) or come from remote Git repositories. For example, one can depend on [mathlib](https://reservoir.lean-lang.org/@leanprover-community/mathlib) like so:
 
 ```lean
 package hello
 
-require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git"
+require "leanprover-community" / "mathlib"
 ```
 
 The next run of `lake build` (or refreshing dependencies in an editor like VSCode) will clone the mathlib repository and build it. Information on the specific revision cloned will then be saved to `lake-manifest.json` to enable reproducibility (i.e., ensure the same version of mathlib is used by future builds). To update `mathlib` after this, you will need to run `lake update` -- other commands do not update resolved dependencies.
@@ -343,10 +342,13 @@ For theorem proving packages which depend on `mathlib`, you can also run `lake n
 The `require` command in Lean Lake configuration follows the general syntax:
 
 ```lean
-require <pkg-name> from <source> [with <options>]
+require ["<scope>" /] <pkg-name> [@ <version>]
+  [from <source>] [with <options>]
 ```
 
 The `from` clause tells Lake where to locate the dependency.
+Without a `from` clause, Lake will lookup the package in the default registry (i.e., [Reservoir](https://reservoir.lean-lang.org/@lean-dojo/LeanCopilot)) and use the information there to download the package at the specified `version`. The optional `scope` is used to disambiguate which package with `pkg-name` to lookup. In Reservoir, this scope is the package owner (e.g., `leanprover` of [@leanprover/doc-gen4](https://reservoir.lean-lang.org/@leanprover/doc-gen4)).
+
 The `with` clause specifies a `NameMap String` of Lake options used to configure the dependency. This is equivalent to passing `-K` options to the dependency on the command line.
 
 ## Supported Sources
@@ -374,11 +376,17 @@ Lake clones the Git repository available at the specified fixed Git `url`, and c
 To `require` a package in a TOML configuration, the parallel syntax for the above examples is:
 
 ```toml
+# A Reservoir dependency
+[[require]]
+name = "<pkg-name>"
+scope = "<scope>"
+version = "<version>"
+options = {<options>}
+
 # A path dependency
 [[require]]
 name = "<pkg-name>"
 path = "<path>"
-options = {<options>}
 
 # A Git dependency
 [[require]]
@@ -386,7 +394,6 @@ name = "<pkg-name>"
 git = "<url>"
 rev = "<rev>"
 subDir = "<subDir>"
-options = {<options>}
 ```
 
 ## GitHub Release Builds

src/lake/examples/deps/bar/lake-manifest.expected.json

@@ -1,25 +1,29 @@
-{"version": "1.0.0",
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"type": "path",
+   "scope": "",
    "name": "root",
    "manifestFile": "lake-manifest.json",
    "inherited": true,
    "dir": "./../foo/../a/../root",
    "configFile": "lakefile.lean"},
   {"type": "path",
+   "scope": "",
    "name": "a",
    "manifestFile": "lake-manifest.json",
    "inherited": true,
    "dir": "./../foo/../a",
    "configFile": "lakefile.lean"},
   {"type": "path",
+   "scope": "",
    "name": "b",
    "manifestFile": "lake-manifest.json",
    "inherited": true,
    "dir": "./../foo/../b",
    "configFile": "lakefile.lean"},
   {"type": "path",
+   "scope": "",
    "name": "foo",
    "manifestFile": "lake-manifest.json",
    "inherited": false,

src/lake/examples/ffi/app/lakefile.lean

@@ -9,4 +9,5 @@ require ffi from ".."/"lib"
 lean_exe app where
   root := `Main
 
-lean_lib Test
+lean_lib Test where
+  precompileModules := true

src/lake/examples/ffi/lib/lakefile.lean

@@ -1,14 +1,13 @@
 import Lake
 open System Lake DSL
 
-package ffi {
+package ffi where
   srcDir := "lean"
-  precompileModules := true
-}
 
 lean_lib FFI
 
-@[default_target] lean_exe test where
+@[default_target]
+lean_exe test where
   root := `Main
 
 target ffi.o pkg : FilePath := do

src/lake/examples/ffi/package.sh

@@ -1,10 +0,0 @@
-set -ex
-
-cd app
-${LAKE:-../../../.lake/build/bin/lake} build -v -U
-cd ..
-
-
-cd lib
-${LAKE:-../../../.lake/build/bin/lake} build -v
-cd ..

src/lake/examples/ffi/test.sh

@@ -1,8 +1,18 @@
-set -ex
+#!/usr/bin/env bash
+set -euxo pipefail
+
+LAKE=${LAKE:-../../.lake/build/bin/lake}
 
 ./clean.sh
-./package.sh
+
+# Tests that a non-precmpiled build does not load anything as a dynlib
+# https://github.com/leanprover/lean4/issues/4565
+$LAKE -d app build -v | (grep --color load-dynlib && exit 1 || true)
+$LAKE -d lib build -v | (grep --color load-dynlib && exit 1 || true)
+
 ./app/.lake/build/bin/app
 ./lib/.lake/build/bin/test
 
-${LAKE:-../../.lake/build/bin/lake} -d app build -v Test
+# Tests the successful precompilation of an `extern_lib`
+# Also tests a module with `precompileModules` always precompiles its imports
+$LAKE -d app build Test

src/lake/examples/scripts/expected.out

@@ -1,5 +1,5 @@
 dep/hello
-scripts/dismiss
+scripts/say-goodbye
 scripts/greet
 Hello, world!
 Hello, me!
@@ -13,10 +13,11 @@ Greet the entity with the given name. Otherwise, greet the whole world.
 
 Hello from Dep!
 Hello from Dep!
+Goodbye!
 error: unknown script nonexistant
 error: unknown script nonexistant
 dep/hello
-scripts/dismiss
+scripts/say-goodbye
 scripts/greet
 Hello, world!
 Goodbye!

src/lake/examples/scripts/lakefile.lean

@@ -21,6 +21,6 @@ script greet (args) do
   return 0
 
 @[default_script]
-script dismiss do
+script "say-goodbye" do
   IO.println "Goodbye!"
   return 0

src/lake/examples/scripts/test.sh

@@ -15,8 +15,11 @@ $LAKE script run greet --me | tee -a produced.out
 $LAKE script doc greet | tee -a produced.out
 $LAKE script run hello | tee -a produced.out
 $LAKE script run dep/hello | tee -a produced.out
-($LAKE script run nonexistant 2>&1 | tee -a produced.out) && false || true
-($LAKE script doc nonexistant 2>&1 | tee -a produced.out) && false || true
+# Test that non-indentifier names work
+# https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Running.20.60lake.60.20scripts.20from.20the.20command.20line/near/446944450
+$LAKE script run say-goodbye | tee -a produced.out
+($LAKE script run nonexistant 2>&1 | tee -a produced.out) && exit 1 || true
+($LAKE script doc nonexistant 2>&1 | tee -a produced.out) && exit 1 || true
 $LAKE scripts | tee -a produced.out
 $LAKE run | tee -a produced.out
 

src/lake/tests/badImport/.gitignore

@@ -1 +1 @@
-Lib/Y.lean
+Lib/Bogus.lean

src/lake/tests/badImport/Etc.lean

@@ -0,0 +1,2 @@
+-- Module used to test that a build continues after an import error
+import Bogus

src/lake/tests/badImport/Lib/A.lean

@@ -1 +0,0 @@
-import Lib.A

src/lake/tests/badImport/Lib/B.lean

@@ -1 +1,2 @@
-import Lib.Y
+-- Import a missing module within a Lake library
+import Lib.Bogus

src/lake/tests/badImport/Lib/B1.lean

@@ -0,0 +1,2 @@
+-- Import a module with a bad import
+import Lib.B

src/lake/tests/badImport/Lib/C.lean

@@ -1 +0,0 @@
-import Lib.A

src/lake/tests/badImport/Lib/S.lean

@@ -0,0 +1,2 @@
+-- Module which imports itself
+import Lib.S

src/lake/tests/badImport/Lib/U.lean

@@ -0,0 +1,2 @@
+-- Import a missing module outside any package known to Lake
+import Bogus

src/lake/tests/badImport/X.lean

@@ -1 +1,2 @@
-import Y
+-- From an executable, import a missing module within a Lake library
+import Lib.Bogus

src/lake/tests/badImport/X1.lean

@@ -0,0 +1,2 @@
+-- From an executable, import a module which contains a bad import
+import Lib.B

src/lake/tests/badImport/clean.sh

@@ -1 +1 @@
-rm -rf .lake lake-manifest.json Lib/Y.lean
+rm -rf .lake lake-manifest.json Lib/Bogus.lean

src/lake/tests/badImport/lakefile.lean

@@ -3,5 +3,8 @@ open Lake DSL
 
 package test
 
-lean_lib X
 lean_lib Lib
+lean_lib Etc
+
+lean_exe X
+lean_exe X1

src/lake/tests/badImport/test.sh

@@ -12,22 +12,29 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 # https://github.com/leanprover/lean4/issues/3351
 # https://github.com/leanprover/lean4/issues/3809
 
+# Test a module with a bad import does not kill the whole build
+($LAKE build Lib.U Etc 2>&1 && exit 1 || true) | grep --color -F "Building Etc"
 # Test importing a nmissing module from outside the workspace
-($LAKE build +X 2>&1 && exit 1 || true) | grep --color -F "X.lean:1:0: unknown module prefix 'Y'"
-$LAKE setup-file ./X.lean Y # Lake ignores the file (the server will error)
+($LAKE build +Lib.U 2>&1 && exit 1 || true) | grep --color -F "U.lean:2:0: unknown module prefix 'Bogus'"
+$LAKE setup-file . Bogus # Lake ignores the file (the server will error)
 # Test importing onself
-($LAKE build +Lib.A 2>&1 && exit 1 || true) | grep --color -F "A.lean: module imports itself"
-($LAKE setup-file ./Lib/A.lean Lib.A 2>&1 && exit 1 || true) | grep --color -F "A.lean: module imports itself"
+($LAKE build +Lib.S 2>&1 && exit 1 || true) | grep --color -F "S.lean: module imports itself"
+($LAKE setup-file ./Lib/S.lean Lib.S 2>&1 && exit 1 || true) | grep --color -F "S.lean: module imports itself"
 # Test importing a missing module from within the workspace
-($LAKE build +Lib.B 2>&1 && exit 1 || true) | grep --color -F "B.lean: bad import 'Lib.Y'"
-($LAKE setup-file X.lean Lib.B 2>&1 && exit 1 || true) | grep --color "B.lean: bad import 'Lib.Y'"
+($LAKE build +Lib.B 2>&1 && exit 1 || true) | grep --color -F "B.lean: bad import 'Lib.Bogus'"
+($LAKE setup-file ./Lib/B.lean Lib.Bogus 2>&1 && exit 1 || true) | grep --color "B.lean: bad import 'Lib.Bogus'"
 # Test a vanishing import within the workspace (lean4#3551)
-touch Lib/Y.lean
+touch Lib/Bogus.lean
 $LAKE build +Lib.B
-rm Lib/Y.lean
-($LAKE build +Lib.B 2>&1 && exit 1 || true) | grep --color -F "B.lean: bad import 'Lib.Y'"
-($LAKE setup-file ./X.lean Lib.B 2>&1 && exit 1 || true) | grep --color "B.lean: bad import 'Lib.Y'"
-# Test a module C which imports another module A which contains a bad import
-($LAKE build +Lib.C 2>&1 && exit 1 || true) | grep --color -F "C.lean: bad import 'Lib.A'"
-($LAKE setup-file Lib/C.lean Lib.A 2>&1 && exit 1 || true) | grep --color -F "C.lean: bad import 'Lib.A'"
-
+rm Lib/Bogus.lean
+($LAKE build +Lib.B 2>&1 && exit 1 || true) | grep --color -F "B.lean: bad import 'Lib.Bogus'"
+($LAKE setup-file . Lib.B 2>&1 && exit 1 || true) | grep --color "B.lean: bad import 'Lib.Bogus'"
+# Test a module which imports a module containing a bad import
+($LAKE build +Lib.B1 2>&1 && exit 1 || true) | grep --color -F "B1.lean: bad import 'Lib.B'"
+($LAKE setup-file ./Lib/B1.lean Lib.B 2>&1 && exit 1 || true) | grep --color -F "B1.lean: bad import 'Lib.B'"
+# Test an executable with a bad import does not kill the whole build
+($LAKE build X Etc 2>&1 && exit 1 || true) | grep --color -F "Building Etc"
+# Test an executable which imports a missing module from within the workspace
+($LAKE build X 2>&1 && exit 1 || true) | grep --color -F "X.lean: bad import 'Lib.Bogus'"
+# Test a executable which imports a module containing a bad import
+($LAKE build X1 2>&1 && exit 1 || true) | grep --color -F "B.lean: bad import 'Lib.Bogus'"

src/lake/tests/manifest/lake-manifest-v1.1.0.json

@@ -0,0 +1,22 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"type": "path",
+   "scope": "",
+   "name": "foo",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "./foo",
+   "configFile": "lakefile.lean"},
+  {"url": "bar",
+   "type": "git",
+   "subDir": null,
+   "scope": "foo",
+   "rev": "0538596b94a0510f55dc820cabd3bde41ad93c3e",
+   "name": "bar",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "«foo-bar»",
+ "lakeDir": ".lake"}

src/lake/tests/manifest/lakefile.lean

@@ -1,7 +1,7 @@
 import Lake
 open Lake DSL
 
-package «foo-bar»
+package "foo-bar"
 
 require foo from "foo"
-require bar from git "bar"
+require "foo" / bar from git "bar"

src/lake/tests/manifest/test.sh

@@ -25,7 +25,7 @@ git commit -m "initial commit"
 GIT_REV=`git rev-parse HEAD`
 popd
 
-LATEST_VER=v1.0.0
+LATEST_VER=v1.1.0
 LOCKED_REV='0538596b94a0510f55dc820cabd3bde41ad93c3e'
 
 # Test an update produces the expected manifest of the latest version
@@ -66,3 +66,4 @@ test_manifest v5
 test_manifest v6
 test_manifest v7
 test_manifest v1.0.0
+test_manifest v1.1.0

src/lake/tests/online/bogus-dep.toml

@@ -0,0 +1,5 @@
+name = "test"
+
+[[require]]
+name = "bogus"
+scope = "bogus"

src/lake/tests/online/clean.sh

@@ -0,0 +1 @@
+rm -rf .lake lake-manifest.json

src/lake/tests/online/lakefile.lean

@@ -0,0 +1,6 @@
+import Lake
+open Lake DSL
+
+package test
+
+require "leanprover" / "doc-gen4"

src/lake/tests/online/lakefile.toml

@@ -0,0 +1,6 @@
+name = "test"
+
+[[require]]
+name = "doc-gen4"
+scope = "leanprover"
+rev = "main"

src/lake/tests/online/test.sh

@@ -0,0 +1,19 @@
+#!/usr/bin/env bash
+set -exo pipefail
+
+LAKE=${LAKE:-../../.lake/build/bin/lake}
+
+./clean.sh
+# Tests requiring a package not in the index
+($LAKE update -f bogus-dep.toml 2>&1 && exit || true) |
+  grep --color "error: bogus/bogus: could not materialize package: dependency has no explicit source and was not found on Reservoir"
+
+./clean.sh
+$LAKE update -f lakefile.lean -v
+test -d .lake/packages/doc-gen4
+$LAKE resolve-deps -f lakefile.lean # validate manifest
+
+./clean.sh
+$LAKE update -f lakefile.toml -v
+test -d .lake/packages/doc-gen4
+$LAKE resolve-deps -f lakefile.toml # validate manifest

src/lake/tests/translateConfig/out.expected.lean

@@ -9,6 +9,8 @@ package test where
   lintDriver := "b"
   platformIndependent := true
 
+require "foo" / baz @ "git#abcdef"
+
 require foo from "-" with Lake.NameMap.empty |>.insert `foo "bar"
 
 require bar from git "https://example.com"@"abc"/"sub/dir"

src/lake/tests/translateConfig/out.expected.toml

@@ -6,6 +6,11 @@ defaultTargets = ["A"]
 [leanOptions]
 pp.unicode.fun = true
 
+[[require]]
+name = "baz"
+scope = "foo"
+version = "git#abcdef"
+
 [[require]]
 name = "foo"
 path = "dir"

src/lake/tests/translateConfig/source.lean

@@ -32,6 +32,7 @@ package test where
   leanOptions := #[⟨`pp.unicode.fun, true⟩]
   lintDriver := "b"
 
+require "foo" / "baz" @ "git#abcdef"
 require foo from "dir" with NameMap.empty.insert `foo "bar"
 require bar from git "https://example.com" @ "abc" / "sub" / "dir"