chore: bump toolchain to v4.32.0-rc1 (#885)

Author: Garmelon

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "20b8493528eed2fac9827ce18d41c475f0e1c50a",
+   "rev": "ae95e7e7d01c072421732d0b84cf63ff903f4f0e",
    "name": "illuminate",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc",
+   "rev": "f3f26cc72646205ca167117487c008ee1dafe816",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.31.0
+leanprover/lean4:v4.32.0-rc1

src/verso-manual/VersoManual/Docstring.lean

@@ -583,20 +583,19 @@ def inheritance.descr : BlockDescr where
     open Verso.Output Html in do
       let .ok (name, parents) := FromJson.fromJson? (α := Name × Array Block.Docstring.ParentInfo) info
         | do reportError "Failed to deserialize docstring structure inheritance data while generating HTML"; pure .empty
-      let parentRow ← do
-        if parents.isEmpty then pure .empty
-        else pure {{
-            <ul class="extends">
-              {{← parents.mapM fun parent => do
-                let filterId := s!"{parent.index}-{parent.name}-{name}"
-                pure {{
-                  <li>
-                    <input type="checkbox" id={{filterId}} data-parent-idx={{toString parent.index}}/>
-                    <label for={{filterId}}><code class="hl lean inline">{{← parent.parent.toHtml (g := Manual)}}</code></label>
-                  </li>}}
-              }}
-            </ul>
-          }}
+      if parents.isEmpty then pure .empty
+      else pure {{
+          <ul class="extends">
+            {{← parents.mapM fun parent => do
+              let filterId := s!"{parent.index}-{parent.name}-{name}"
+              pure {{
+                <li>
+                  <input type="checkbox" id={{filterId}} data-parent-idx={{toString parent.index}}/>
+                  <label for={{filterId}}><code class="hl lean inline">{{← parent.parent.toHtml (g := Manual)}}</code></label>
+                </li>}}
+            }}
+          </ul>
+        }}
 
 open Block.Docstring (Visibility) in
 @[block_extension Block.fieldSignature]

src/verso/Verso/Doc/ArgParse.lean

@@ -473,7 +473,7 @@ partial def parseArgs : ArgParse m α → ExceptT (Array Doc.Arg × Exception) (
           | true => some val
           | false => val
       | .error e => throwThe (Array Doc.Arg × Exception) e
-    else match optional with
+    else match (dependent := true) optional with
       | true => Pure.pure none
       | false => throwThe (Array Doc.Arg × Exception) ((← get).remaining, .error (← getRef) m!"Named argument '{x}' ({vp.description}) not found")
   | .anyNamed x vp doc? => do

src/verso/Verso/Doc/Elab/Block.lean

@@ -36,7 +36,7 @@ public partial def elabBlock (block : TSyntax `block) : DocElabM (TSyntax `term)
     ``(sorryAx (Block _) (synthetic := true))
   | stx@(.node _ kind _) =>
     let env ← getEnv
-    let result ← match (← liftMacroM (expandMacroImpl? env stx)) with
+    match (← liftMacroM (expandMacroImpl? env stx)) with
     | some (_decl, stxNew?) => -- TODO terminfo here? Right now, we suppress most uses of it.
       let stxNew ← liftMacroM <| liftExcept stxNew?
       withMacroExpansionInfo stx stxNew <|

src/verso/Verso/Doc/Elab/Inline.lean

@@ -28,7 +28,7 @@ public partial def elabInline (inline : TSyntax `inline) : DocElabM (TSyntax `te
     ``(sorryAx (Inline _) (synthetic := true))
   | stx@(.node _ kind _) =>
     let env ← getEnv
-    let result ← match (← liftMacroM (expandMacroImpl? env stx)) with
+    match (← liftMacroM (expandMacroImpl? env stx)) with
     | some (_decl, stxNew?) => -- TODO terminfo here? Right now, we suppress most uses of it.
       let stxNew ← liftMacroM <| liftExcept stxNew?
       withMacroExpansionInfo stx stxNew <|

test-projects/literate-config/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.31.0
+leanprover/lean4:v4.32.0-rc1

test-projects/literate-multi-root/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.31.0
+leanprover/lean4:v4.32.0-rc1