chore: update dependencies and fix warnings (#576)

Author: david-christiansen

Manual/Defs.lean

@@ -489,7 +489,7 @@ The headers and bodies of definitions are elaborated together.
 If the header is incompletely specified (e.g. a parameter's type or the codomain is missing), then the body may provide sufficient information for the elaborator to reconstruct the missing parts.
 However, {tech}[instance implicit] parameters must be specified in the header or as {tech}[section variables].
 
-:::syntax Lean.Parser.Command.declaration alias:=Lean.Parser.Command.definition (title := "Definitions")
+:::syntax Lean.Parser.Command.declaration (alias := Lean.Parser.Command.definition) (title := "Definitions")
 Definitions that use `:=` associate the term on the right-hand side with the constant's name.
 The term is wrapped in a {keywordOf Lean.Parser.Term.fun}`fun` for each parameter, and the type is found by binding the parameters in a function type.
 Definitions with {keyword}`def` are {tech}[semireducible].
@@ -517,7 +517,7 @@ def $_ $_ where
 ```
 :::
 
-:::syntax Lean.Parser.Command.declaration alias:=Lean.Parser.Command.abbrev (title := "Abbreviations")
+:::syntax Lean.Parser.Command.declaration (alias := Lean.Parser.Command.abbrev) (title := "Abbreviations")
 Abbreviations are identical to definitions with {keyword}`def`, except they are {tech}[reducible].
 
 ```grammar
@@ -545,7 +545,7 @@ Unlike {tech}[axioms], opaque declarations can only be used for types that are i
 Also unlike axioms, the inhabitant of the type is used in compiled code.
 The {attr}`implemented_by` attribute can be used to instruct the compiler to emit a call to some other function as the compilation of an opaque constant.
 
-:::syntax Lean.Parser.Command.declaration alias:=Lean.Parser.Command.opaque (title := "Opaque Constants")
+:::syntax Lean.Parser.Command.declaration (alias := Lean.Parser.Command.opaque) (title := "Opaque Constants")
 Opaque definitions with right-hand sides are elaborated like other definitions.
 This demonstrates that the type is inhabited; the inhabitant plays no further role.
 ```grammar
@@ -579,7 +579,7 @@ However, because their use cases are quite different, they differ in many detail
 Theorems may be recursive, subject to the same conditions as {ref "recursive-definitions"}[recursive function definitions].
 However, it is more common to use tactics such as {tactic}`induction` or {tactic}`fun_induction` instead.
 
-:::syntax Lean.Parser.Command.declaration alias:=Lean.Parser.Command.theorem (title := "Theorems")
+:::syntax Lean.Parser.Command.declaration (alias := Lean.Parser.Command.theorem) (title := "Theorems")
 The syntax of theorems is like that of definitions, except the codomain (that is, the theorem statement) in the signature is mandatory.
 ```grammar
 $_:declModifiers
@@ -606,7 +606,7 @@ theorem $_ $_ where
 An {deftech}[example] is an anonymous definition that is elaborated and then discarded.
 Examples are useful for incremental testing during development and to make it easier to understand a file.
 
-:::syntax Lean.Parser.Command.declaration alias:=Lean.Parser.Command.example (title := "Examples")
+:::syntax Lean.Parser.Command.declaration (alias := Lean.Parser.Command.example) (title := "Examples")
 ```grammar
 $_:declModifiers
 example $_:optDeclSig := $_

Manual/Language/InductiveTypes/Structures.lean

@@ -275,7 +275,7 @@ This updating does not require that the index expression be in bounds for the ar
 Updating structures may use array indices as well as projection names.
 Updates at indices that are out of bounds are ignored:
 
-```lean name:=arrayUpdate
+```lean (name := arrayUpdate)
 structure AugmentedIntArray where
   array : Array Int
   augmentation : String := ""
@@ -492,7 +492,7 @@ def coords : Triple Nat := {fst := 17, snd := 2, thd := 95}
 ```
 
 Evaluating the first field index of {name}`coords` yields the underlying {name}`Pair`, rather than the contents of the field `fst`:
-```lean name:=coords1
+```lean (name := coords1)
 #eval coords.1
 ```
 ```leanOutput coords1

Manual/RecursiveDefs.lean

@@ -490,7 +490,7 @@ semireducible
 ```grammar
 irreducible
 ```
-These attributes can only be applied globally in the same file as the definition being modified, but they may be {keywordOf attrInst parser:=Lean.Parser.Term.attrKind}`local`ly applied anywhere.
+These attributes can only be applied globally in the same file as the definition being modified, but they may be {keywordOf attrInst (parser := Lean.Parser.Term.attrKind)}`local`ly applied anywhere.
 :::
 
 ## Reducibility and Tactics

Manual/Terms.lean

@@ -357,7 +357,7 @@ fun $x:ident : term => $t
 ```
 :::
 
-Function definitions defined with keywords such as {keywordOf Lean.Parser.Command.declaration parser:=Lean.Parser.Command.definition}`def` desugar to {keywordOf Lean.Parser.Term.fun}`fun`.
+Function definitions defined with keywords such as {keywordOf Lean.Parser.Command.declaration (parser := Lean.Parser.Command.definition)}`def` desugar to {keywordOf Lean.Parser.Term.fun}`fun`.
 Inductive type declarations, on the other hand, introduce new values with function types (constructors and type constructors) that cannot themselves be implemented using just {keywordOf Lean.Parser.Term.fun}`fun`.
 
 :::syntax term (title := "Curried Functions")

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "1a84b41c176a576e982676d6e1b0cb3df1786abb",
+   "rev": "4863fb303c5c761a66c17417cd024b094e5b9399",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "597aa7f6d1d4bc22c5bdef797797497b10bea1f4",
+   "rev": "0d0b1d3fae1157cc2df3480f7c0c98c33fc7bbe5",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",