chore: bump toolchain to v4.31.0 (#865)

Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>

Author: Garmelon

Manual/Meta/Example.lean

@@ -28,7 +28,7 @@ def Block.example (descriptionString : String) (name : Option String) (opened :
 abbrev ExampleBlockJson := String × Option String × Bool × Option Tag × Option String
 
 structure ExampleConfig where
-  description : FileMap × TSyntaxArray `inline
+  description : TSyntaxArray `inline
   /-- Name for refs -/
   tag : Option String := none
   keep : Bool := false
@@ -110,12 +110,10 @@ def examples : Domain := {}
 @[directive]
 def «example» : DirectiveExpanderOf ExampleConfig
   | cfg, contents => do
-    let description ←
-      DocElabM.withFileMap cfg.description.1 <|
-      cfg.description.2.mapM elabInline
-    let descriptionString := inlinesToString (← getEnv) cfg.description.2
-    PointOfInterest.save (← getRef) (inlinesToString (← getEnv) cfg.description.2)
-      (selectionRange := mkNullNode cfg.description.2)
+    let description ← cfg.description.mapM elabInline
+    let descriptionString := inlinesToString (← getEnv) cfg.description
+    PointOfInterest.save (← getRef) (inlinesToString (← getEnv) cfg.description)
+      (selectionSyntax? := some <| mkNullNode cfg.description)
       (kind := Lsp.SymbolKind.interface)
       (detail? := some "Example")
 

Manual/Meta/Figure.lean

@@ -24,7 +24,7 @@ def Block.figure (captionString : String) (name : Option String) : Block where
   data := ToJson.toJson (captionString, name, (none : Option Tag))
 
 structure FigureConfig where
-  caption : FileMap × TSyntaxArray `inline
+  caption : TSyntaxArray `inline
   /-- Name for refs -/
   tag : Option String := none
 
@@ -37,15 +37,14 @@ def figure : DirectiveExpander
   | args, contents => do
     let cfg ← FigureConfig.parse.run args
 
-    PointOfInterest.save (← getRef) (inlinesToString (← getEnv) cfg.caption.2)
-      (selectionRange := mkNullNode cfg.caption.2)
+    PointOfInterest.save (← getRef) (inlinesToString (← getEnv) cfg.caption)
+      (selectionSyntax? := some <| mkNullNode cfg.caption)
       (kind := Lsp.SymbolKind.interface)
       (detail? := some "Figure")
 
-    let caption ← DocElabM.withFileMap cfg.caption.1 <|
-      cfg.caption.2.mapM elabInline
+    let caption ← cfg.caption.mapM elabInline
 
-    let captionString := inlinesToString (← getEnv) cfg.caption.2
+    let captionString := inlinesToString (← getEnv) cfg.caption
 
     let blocks ← contents.mapM elabBlock
     -- Figures are represented using the first block to hold the caption. Storing it in the JSON

Manual/Meta/Markdown.lean

@@ -30,8 +30,11 @@ def Block.noVale.descr : BlockDescr where
 
 /-- Closes the last-opened section, throwing an error on failure. -/
 def closeEnclosingSection : PartElabM Unit := do
-  -- We use `default` as the source position because the Markdown doesn't have one
-  if let some ctxt' := (← getThe PartElabM.State).partContext.close default then
+  -- Markdown headers carry no source extent of their own, so end the section at the end of the
+  -- current reference. This keeps each part's range valid (the selection stays within
+  -- `[rangeStart, endPos]`) for the TOC range conversion.
+  let endPos := (← getRef).getTailPos?.getD default
+  if let some ctxt' := (← getThe PartElabM.State).partContext.close endPos then
     modifyThe PartElabM.State fun st => {st with partContext := ctxt'}
   else
     throwError m!"Failed to close the last-opened explanation part"
@@ -51,7 +54,7 @@ def markdown : PartCommand
        logErrorAt arg m!"No arguments expected{h}"
      let some ast := MD4Lean.parse txt.getString
        | throwError "Failed to parse body of markdown code block"
-     let mut currentHeaderLevels : Markdown.HeaderMapping := default
+     let mut currentHeaderLevels : Markdown.HeaderMapping := {}
      for block in ast.blocks do
        currentHeaderLevels ← Markdown.addPartFromMarkdown block currentHeaderLevels
      closeEnclosingSections currentHeaderLevels

Manual/Meta/Syntax.lean

@@ -81,7 +81,7 @@ structure FreeSyntaxConfig where
   name : Name
   «open» : Bool := true
   label : Option String := none
-  title : (FileMap × TSyntaxArray `inline)
+  title : TSyntaxArray `inline
 
 def FreeSyntaxConfig.getLabel (config : FreeSyntaxConfig) : String :=
   config.label.getD <|
@@ -830,7 +830,7 @@ where
       return bar ++ .nest 2 (← production which stx |>.run' {})
 
 def testGetBnf (config : FreeSyntaxConfig) (isFirst : Bool) (stxs : List Syntax) : TermElabM String := do
-  let (tagged, _) ← getBnf config isFirst stxs |>.run ⟨default, default, default, default⟩ {} {partContext := ⟨⟨default, default, default, default, default⟩, default⟩}
+  let (tagged, _) ← getBnf config isFirst stxs |>.run ⟨default, default, default, default⟩ {} {partContext := ⟨⟨default, default, default, default, default, default⟩, default⟩}
   pure tagged.stripTags
 
 namespace Tests
@@ -841,7 +841,7 @@ def selectedParser : Parser := leading_parser
 
 
 elab "#test_syntax" arg:selectedParser : command => do
-  let bnf ← Command.liftTermElabM (testGetBnf {name := (TSyntax.mk arg.raw[0]).getId, title := (FileMap.ofString "", #[])} true [arg.raw[2]])
+  let bnf ← Command.liftTermElabM (testGetBnf { name := (TSyntax.mk arg.raw[0]).getId, title := #[] } true [arg.raw[2]])
   logInfo bnf
 
 /--
@@ -867,7 +867,7 @@ info: term ::= ...
 
 
 elab "#test_free_syntax" x:ident arg:free_syntaxes : command => do
-  let bnf ← Command.liftTermElabM (testGetBnf {name := x.getId, title := (FileMap.ofString "", #[])} true (FreeSyntax.decodeMany arg |>.map FreeSyntax.decode))
+  let bnf ← Command.liftTermElabM (testGetBnf { name := x.getId, title := #[] } true (FreeSyntax.decodeMany arg |>.map FreeSyntax.decode))
   logInfo bnf
 
 /--
@@ -1084,12 +1084,10 @@ def «syntax» : DirectiveExpander
   | args, blocks => do
     let config ← SyntaxConfig.parse.run args
 
-    let title ← do
-      let (fm, t) := config.title
-      DocElabM.withFileMap fm <| t.mapM elabInline
+    let title ← config.title.mapM elabInline
 
     let env ← getEnv
-    let titleString := inlinesToString env (config.title.snd)
+    let titleString := inlinesToString env (config.title)
 
     let mut content := #[]
     let mut firstGrammar := true
@@ -1102,8 +1100,7 @@ def «syntax» : DirectiveExpander
       | _ =>
         content := content.push <| ← elabBlock b
 
-    Doc.PointOfInterest.save (← getRef) titleString
-      (selectionRange := (← getRef)[0])
+    Doc.PointOfInterest.save (← getRef) titleString (selectionSyntax? := some (← getRef)[0])
 
     pure #[← `(Block.other {Block.syntax with data := ToJson.toJson (α := Option String × Name × String × Option Tag × Array Name) ($(quote titleString), $(quote config.name), $(quote config.getLabel), none, $(quote config.aliases.toArray))} #[Block.para #[$(title),*], $content,*])]
 where
@@ -1161,11 +1158,9 @@ def freeSyntax : DirectiveExpander
   | args, blocks => do
     let config ← FreeSyntaxConfig.parse.run args
 
-    let title ← do
-      let (fm, t) := config.title
-      DocElabM.withFileMap fm <| t.mapM elabInline
+    let title ← config.title.mapM elabInline
     let env ← getEnv
-    let titleString := inlinesToString env config.title.snd
+    let titleString := inlinesToString env config.title
 
     let mut content := #[]
     let mut firstGrammar := true

Manual/Releases/v4_31_0.lean

@@ -14,17 +14,12 @@ open Verso.Genre.Manual
 open Verso.Genre.Manual.InlineLean
 open Lean.MessageSeverity
 
-#doc (Manual) "Lean 4.31.0-rc2 (2026-06-04)" =>
+#doc (Manual) "Lean 4.31.0 (2026-06-13)" =>
 %%%
 tag := "release-v4.31.0"
 file := "v4.31.0"
 %%%
 
-:::warn
-These release notes describe a _release candidate_, not the final release.
-They may be incomplete and are subject to change.
-:::
-
 For this release, 305 changes landed.
 In addition to the 105 feature additions,
 and 102 fixes listed below,

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "4c6b02ee232211811f9ad1c148ac336122e256d7",
+   "rev": "113c54a466d14d1cd1e615103aefd27ffef19b12",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c7a8de81e102ee2a42a7395f98d1ed12a861a43b",
+   "rev": "20b8493528eed2fac9827ce18d41c475f0e1c50a",
    "name": "illuminate",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a252e45ae646f999c535e1056536def2c871f085",
+   "rev": "6ca10c8b0e640e9e2c27b49b5ca9981063a2434f",
    "name": "versowebcomponents",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "744117af710b1c0400cd297c9ce91f8d0ad3a347",
+   "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a86770a5eba721c8554d1d7fce741bc4dde3bb61",
+   "rev": "0bd508e8362f56d4a05cbf63614d4c97db954041",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.31.0-rc2
+leanprover/lean4:v4.31.0