chore: target nightly-2026-08-21 and port to exception stacks

The tuple refactor (leanprover/lean4#14836) replaces the bespoke
exception postcondition types. In the vcgen documents, EPost.Nil
becomes EStack⟨⟩, EPost.Nil.mk becomes (), and the Result monad
carries a bare Error → Prop exception postcondition, so epost e
replaces epost.head e and the head-projection step leaves the
monotonicity proof. The push helpers for transformers are
PredTrans.pushExceptT and PredTrans.pushOptionT.

The EStack⟨…⟩ and estack⟨…⟩ notations get a syntax block in the
exception postcondition section.

The recorded Lake transcripts gain the new lint option --checks and
the package configuration field checks.

Verified with ./generate-html.sh on nightly-2026-08-21.

Author: sgraf812

Manual/BuildTools/Lake.lean

@@ -763,6 +763,7 @@ root = "Tests"
       libPrefixOnWindows := false,
       allowImportAll := false,
       builtinLint? := none,
+      checks := #[],
       fixedToolchain := false},
   configFile := FilePath.mk "lakefile",
   relConfigFile := FilePath.mk "lakefile",
@@ -927,6 +928,7 @@ lean_exe «my-package-tests» where
       libPrefixOnWindows := false,
       allowImportAll := false,
       builtinLint? := none,
+      checks := #[],
       fixedToolchain := false},
   configFile := FilePath.mk "lakefile.lean",
   relConfigFile := FilePath.mk "lakefile.lean",
@@ -1131,6 +1133,7 @@ root = "Lint"
       libPrefixOnWindows := false,
       allowImportAll := false,
       builtinLint? := none,
+      checks := #[],
       fixedToolchain := false},
   configFile := FilePath.mk "lakefile",
   relConfigFile := FilePath.mk "lakefile",
@@ -1296,6 +1299,7 @@ lean_exe «my-package-lint» where
       libPrefixOnWindows := false,
       allowImportAll := false,
       builtinLint? := none,
+      checks := #[],
       fixedToolchain := false},
   configFile := FilePath.mk "lakefile.lean",
   relConfigFile := FilePath.mk "lakefile.lean",

Manual/BuildTools/Lake/CLI.lean

@@ -895,6 +895,9 @@ OPTIONS:
   --code-quality        records each linter warning as a code quality check result
                         and runs the registered code quality checks.
                         Setting this flag will skip lint driver.
+  --checks <mods>       comma-separated list of workspace modules providing
+                        package code quality checks; they are imported
+                        alongside each linted module (implies --code-quality)
 
 A lint driver can be configured by either setting the `lintDriver` package
 configuration option or by tagging a script or executable `@[lint_driver]`.

Manual/BuildTools/Lake/Config.lean

@@ -193,6 +193,7 @@ name = "example-package"
       libPrefixOnWindows := false,
       allowImportAll := false,
       builtinLint? := none,
+      checks := #[],
       fixedToolchain := false},
   configFile := FilePath.mk "lakefile",
   relConfigFile := FilePath.mk "lakefile",
@@ -284,6 +285,7 @@ name = "Sorting"
       libPrefixOnWindows := false,
       allowImportAll := false,
       builtinLint? := none,
+      checks := #[],
       fixedToolchain := false},
   configFile := FilePath.mk "lakefile",
   relConfigFile := FilePath.mk "lakefile",

Manual/VCGen.lean

@@ -165,9 +165,14 @@ Since unit and pair types come with {name}`Assertion` instances, such exception
 The {name}`WP` translation turns monad transformer stacks turn into exception postcondition stacks.
 The notation `EStack⟨e₁, e₂, ...⟩` abbreviates the type of exception postcondition stack `e₁ × (e₂ × (... × Unit))`, and the notation `estack⟨v₁, v₂, ...⟩` builds a value `(v₁, v₂, ..., ())` of such a stack.
 
+:::syntax term (title := "Exception Postcondition Stacks") (namespace := Std.WP)
 ```grammar
-Insert this, Claude!
+EStack⟨$_,*⟩
 ```
+```grammar
+estack⟨$_,*⟩
+```
+:::
 
 {TODO}[I think the partial vs. total correctness discussion should maybe happen after we have actually introduced Triple? It discusses its syntax.]
 
@@ -209,15 +214,15 @@ The {name}`bind` operator composes predicate transformers.
 
 {docstring Lean.Order.instMonadPredTrans}
 
-The helper operators {name}`Lean.Order.pushArg`, {name}`PredTrans.pushExcept`, and {name}`PredTrans.pushOption` modify a predicate transformer by adding a standard side effect.
+The helper operators {name}`Lean.Order.pushArg`, {name}`PredTrans.pushExceptT`, and {name}`PredTrans.pushOptionT` modify a predicate transformer by adding a standard side effect.
 They are used to implement the {name}`WP` instances for transformers such as {name}`StateT`, {name}`ExceptT`, and {name}`OptionT`; they can also be used to implement monads that can be thought of in terms of one of these.
 For example, {name}`Lean.Order.pushArg` is typically used for state monads, but can also be used to implement a reader monad's instance, treating the reader's value as read-only state.
 
 {docstring Lean.Order.pushArg}
 
-{docstring PredTrans.pushExcept}
+{docstring PredTrans.pushExceptT}
 
-{docstring PredTrans.pushOption}
+{docstring PredTrans.pushOptionT}
 
 ### Weakest Preconditions
 
@@ -291,7 +296,7 @@ The {name}`WP` interpretation of {name}`Identity` is a plain definition marked {
 {TODO}[It is a wart of `vcgen` that we cannot declare the WP instance below. I'll think about fixing it by canonicalizing `WPMonad.toWP` to the `WP` instance, but not in time for 4.35. Let's maybe leave an "under construction" sign for the reader.]
 ```lean
 @[instance_reducible] def Identity.wpInst :
-    WP (Identity α) α Prop EPost.Nil where
+    WP (Identity α) α Prop EStack⟨⟩ where
   wpTrans x := ⟨fun post _ => post x.run⟩
   wp_trans_monotone x := fun _ _ _ _ _ hpost => hpost x.run
 
@@ -303,7 +308,7 @@ This interpretation alone suffices to state weakest preconditions and to prove a
 ```lean +error (name := noInst)
 theorem Identity.of_run_eq_wp' {x : α} {prog : Identity α}
     (h : Identity.run prog = x) (P : α → Prop)
-    (hwp : wp prog P EPost.Nil.mk) : P x := by
+    (hwp : wp prog P ()) : P x := by
   simp_all [wp, WP.wpTrans, ← h]
 
 theorem rev_correct_bad {xs : List α} :
@@ -321,7 +326,7 @@ No spec applicable to program (forIn xs [] fun x __s => pure (ForInStep.yield (x
 ```
 The issue can be resolved by defining a {name}`WPMonad` instance whose {name}`WPMonad.toWP` field carries the interpretation:
 ```lean
-instance : WPMonad Identity Prop EPost.Nil where
+instance : WPMonad Identity Prop EStack⟨⟩ where
   toWP _ := Identity.wpInst
   pure_le_wp_pure x post epost := PartialOrder.rel_refl
   bind_le_wp_bind x f post epost := PartialOrder.rel_refl
@@ -330,7 +335,7 @@ With this instance, and a suitable invariant, {tactic}`vcgen` and the {tactic}`g
 ```lean
 theorem Identity.of_run_eq_wp {x : α} {prog : Identity α}
     (h : Identity.run prog = x) (P : α → Prop)
-    (hwp : wp prog P EPost.Nil.mk) : P x := by
+    (hwp : wp prog P ()) : P x := by
   simp_all [wp, WP.wpTrans, ← h]
 
 theorem rev_correct {xs : List α} :
@@ -451,7 +456,7 @@ The assertion in the precondition is a function because the assertion type of {l
 :::
 ```lean -show -keep
 -- Test preceding examples' claims
-#synth WP (StateM Nat Unit) Unit (Nat → Prop) EPost.Nil
+#synth WP (StateM Nat Unit) Unit (Nat → Prop) EStack⟨⟩
 ```
 
 ## Invariant Specifications
@@ -608,12 +613,12 @@ This operator was designed to model state monads, but {name}`LogM` can be seen a
 This appending is visible in the body of the instance, where the initial state and the log that resulted from the action are appended:
 ```lean
 @[instance_reducible]
-def LogM.instWP : WP (LogM β α) α (Array β → Prop) EPost.Nil where
+def LogM.instWP : WP (LogM β α) α (Array β → Prop) EStack⟨⟩ where
   wpTrans | { log, value } => pushArg (fun s => pure (value, s ++ log))
   wp_trans_monotone x := fun _ _ _ _ _ hpost s =>
     hpost x.value (s ++ x.log)
 
-instance : WPMonad (LogM β) (Array β → Prop) EPost.Nil where
+instance : WPMonad (LogM β) (Array β → Prop) EStack⟨⟩ where
   toWP _ := LogM.instWP
   pure_le_wp_pure x post epost := by simp [wp, WP.wpTrans, pure]
   bind_le_wp_bind x f post epost := by simp [wp, WP.wpTrans, bind]
@@ -626,7 +631,7 @@ Semantically, the empty array is the correct choice so as to not place items in
 theorem LogM.of_run_eq_wp {α : Type u} {β : Type v}
     {x : α × Array β} {prog : LogM β α}
     (h : LogM.run prog = x) (P : α × Array β → Prop)
-    (hwp : wp prog (fun v l => P (v, l)) EPost.Nil.mk #[]) : P x := by
+    (hwp : wp prog (fun v l => P (v, l)) () #[]) : P x := by
   rw [← h]
   simp [wp, WP.wpTrans] at hwp
   exact hwp

Tutorial/VCGen.lean

@@ -768,7 +768,7 @@ variable {m : Type u → Type v} [Monad m] {Pred EPred : Type} [Assertion Pred]
 ```
 
 A {lean}`StateT σ` layer turns the assertion type `Pred` into `σ → Pred` and leaves the exception postcondition type unchanged.
-An {lean}`ExceptT ε` layer leaves the assertion type unchanged and turns the exception postcondition type `EPred` into {lean}`EPost.Cons (ε → Pred) EPred`, adding one exception branch of type `ε → Pred`.
+An {lean}`ExceptT ε` layer leaves the assertion type unchanged and turns the exception postcondition type `EPred` into {lean}`(ε → Pred) × EPred`, adding one exception branch of type `ε → Pred`.
 The {name}`WP` instance for {lean}`EStateM ε σ` uses assertions of type `σ → Prop` and exception postconditions of type `ε → σ → Prop`, mirroring the single exception branch of the equivalent transformer stack {lean}`ExceptT ε (StateM σ)`.
 :::
 
@@ -836,8 +836,8 @@ Supporting this monad in {tactic}`vcgen` is a matter of:
 universe u v
 variable {α : Type u} {v : α} {e : Error}
 ```
-The {name}`WPMonad` instance for {name}`Result` picks the assertion type {lean}`Prop` because there are no state-like effects, and the exception postcondition type {lean}`EPost⟨Error → Prop⟩` because there is a single exception of type {lean}`Error`.
-Its {name}`WP` interpretation translates a program in {lean}`Result α` to a predicate transformer in {lean}`PredTrans Prop EPost⟨Error → Prop⟩ α`.
+The {name}`WPMonad` instance for {name}`Result` picks the assertion type {lean}`Prop` because there are no state-like effects, and the exception postcondition type {lean}`Error → Prop` because there is a single exception of type {lean}`Error`.
+Its {name}`WP` interpretation translates a program in {lean}`Result α` to a predicate transformer in {lean}`PredTrans Prop (Error → Prop) α`.
 That is, a function mapping a postcondition and an exception postcondition to the weakest precondition.
 Each case of {name}`Result` determines the precondition directly:
 * {lean}`Result.ok v` yields the success postcondition at {lean}`v`.
@@ -850,16 +850,15 @@ For {name}`WPMonad.bind_le_wp_bind`, a case split on the program exposes the {ke
 ::::
 ```lean
 instance Result.instWPMonad :
-    WPMonad Result Prop EPost⟨Error → Prop⟩ where
+    WPMonad Result Prop (Error → Prop) where
   toWP α := {
     wpTrans x := ⟨fun post epost =>
       match x with
       | .ok v => post v
-      | .fail e => epost.head e
+      | .fail e => epost e
       | .div => False⟩
     wp_trans_monotone x := by
       intro post post' epost epost' hepost hpost
-      have hhead := EPost.Cons.le_head hepost
       cases x <;> simp_all [PartialOrder.rel]
   }
   pure_le_wp_pure x post epost := PartialOrder.rel_refl
@@ -873,7 +872,7 @@ Finally, we also prove an adequacy lemma similar to {name}`Except.of_eq_wp` for
 ```lean
 theorem Result.of_eq_wp {α} {x prog : Result α}
     (h : prog = x) (P : Result α → Prop)
-    (hwp : wp prog (fun a => P (.ok a)) epost⟨fun e => P (.fail e)⟩) :
+    (hwp : wp prog (fun a => P (.ok a)) (fun e => P (.fail e))) :
       P x := by
   subst h
   match prog with
@@ -911,8 +910,8 @@ There are two relevant specification lemmas to register:
 ```lean
 @[spec]
 theorem Result.throw_spec {α} {post : α → Prop}
-    {epost : EPost⟨Error → Prop⟩} (e : Error) :
-    ⦃epost.head e⦄ throw (m := Result) (α := α) e ⦃post; epost⦄ :=
+    {epost : Error → Prop} (e : Error) :
+    ⦃epost e⦄ throw (m := Result) (α := α) e ⦃post; epost⦄ :=
   ⟨PartialOrder.rel_refl⟩
 
 @[spec]

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2026-08-19
+leanprover/lean4:nightly-2026-08-21