chore: bump toolchain to v4.31.0-rc1 (#864)

Author: Garmelon

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "99ada816d9929a51132d5b5dc4f43c51f16d67d8",
+   "rev": "08da3f6f41c075e0c18d37eb0fd417c10ed77b6e",
    "name": "illuminate",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a456461b368b71d2accd95234832cd9c174b5437",
+   "rev": "d575be693add4fe9cb996968968ce42ce75c5ccd",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

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

src/tests/Tests/LeanCode.lean

@@ -114,7 +114,9 @@ end
 def unusedArgFn (unused : Nat) : Nat := 0
 ```
 ```leanOutput unusedVar
-unused variable `unused`
+Variable name `unused` is not explicitly referenced.
+
+The binding can be removed (if unused) or named `_` (if used implicitly).
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 ```

src/verso-blog/VersoBlog/LiterateLeanPage.lean

@@ -570,7 +570,7 @@ directory that contains a toolchain file and a Lake configuration (`lakefile.tom
 Set the option `verso.literateMarkdown.logInlines` to `true` to see the error messages that
 prevented elaboration of inline elements.
 -/
-syntax "def_literate_page " ident optConfig " from " ident " in " str " as " str (" with " term)? (rewrites)? : command
+syntax "def_literate_page " ident Lean.Parser.Tactic.optConfig " from " ident " in " str " as " str (" with " term)? (rewrites)? : command
 /--
 Creates a post from a literate Lean module with Markdown module docstrings in it, performing a
 best-effort conversion from a large subset of Markdown to Verso documents. Inline code elements are
@@ -587,7 +587,7 @@ directory that contains a toolchain file and a Lake configuration (`lakefile.tom
 Set the option `verso.literateMarkdown.logInlines` to `true` to see the error messages that
 prevented elaboration of inline elements.
 -/
-syntax "def_literate_post " ident optConfig " from " ident " in " str " as " str (" with " term)? (rewrites)? : command
+syntax "def_literate_post " ident Lean.Parser.Tactic.optConfig " from " ident " in " str " as " str (" with " term)? (rewrites)? : command
 
 
 

src/verso-blog/VersoBlog/LiterateModuleDocs.lean

@@ -124,7 +124,7 @@ module {lit}`MOD` in the project directory {lit}`DIR` with title {lit}`TITLE`.
 (`lakefile.toml` or `lakefile.lean`), which should depend on the same version of Verso that this
 website is using.
 -/
-syntax "literate_page " ident optConfig " from " ident " in " str " as " str (" with " term)? : command
+syntax "literate_page " ident Lean.Parser.Tactic.optConfig " from " ident " in " str " as " str (" with " term)? : command
 /--
 Creates a post from a literate Lean module with Verso-based module docstrings in it. Markdown module
 docstrings are supported, but no attempt is made to elaborate included code.
@@ -136,7 +136,7 @@ module {lit}`MOD` in the project directory {lit}`DIR` with title {lit}`TITLE`.
 (`lakefile.toml` or `lakefile.lean`), which should depend on the same version of Verso that this
 website is using.
 -/
-syntax "literate_post " ident optConfig " from " ident " in " str " as " str (" with " term)? : command
+syntax "literate_post " ident Lean.Parser.Tactic.optConfig " from " ident " in " str " as " str (" with " term)? : command
 
 open Verso Doc in
 open Lean Elab Command in

test-projects/literate-config/lean-toolchain

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

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

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

test-projects/website/DemoSite/Blog/Conditionals.lean

@@ -49,7 +49,6 @@ example : 2 < 5 := by
 Here's the error:
 ```leanOutput fst
 unsolved goals
-case a.a
 ⊢ (Nat.succ 2).le 3
 ```
 
@@ -254,8 +253,8 @@ example : (123123190283102938019238098 * 1234124).toString.length > 14 := by
 ```
 ```leanOutput traces
 [diag] Diagnostics
-  [reduction] unfolded reducible declarations (max: 46, num: 1):
-    [reduction] outParam ↦ 46
+  [reduction] unfolded reducible declarations (max: 40, num: 1):
+    [reduction] outParam ↦ 40
   [type_class] used instances (max: 54, num: 1):
     [type_class] Lean.Grind.CommRing.OfCommSemiring.instOfNatQ ↦ 54
   [reduction] Axioms (possibly imported non-exposed defs) that were tried to be unfolded (max: 22, num: 1):