chore: update for Lean 4.15.0-rc1 (#238)

examples/website-examples/lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/subverso.git",
    "type": "git",
    "subDir": null,
-   "rev": "88819d235a5058aa4b9049d213a2b3493b18887e",
+   "rev": "1c1514540a039a18b12feb738ddf2ac5a5fda45c",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lake-manifest.json

@@ -1,24 +1,24 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/subverso.git",
+ [{"url": "https://github.com/david-christiansen/md4lean",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "88819d235a5058aa4b9049d213a2b3493b18887e",
-   "name": "subverso",
+   "rev": "2b381ee8dceba3b934d3d4aea4a2702a61e5664f",
+   "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "parser",
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/david-christiansen/md4lean",
+  {"url": "https://github.com/leanprover/subverso.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2b381ee8dceba3b934d3d4aea4a2702a61e5664f",
-   "name": "MD4Lean",
+   "rev": "1c1514540a039a18b12feb738ddf2ac5a5fda45c",
+   "name": "subverso",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "parser",
+   "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "verso",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2024-11-27
+leanprover/lean4:v4.15.0-rc1

src/verso/Verso/Parser.lean

@@ -1610,7 +1610,10 @@ where
 
 /--
 info: Success! Final stack:
-  (Verso.Syntax.metadata_block "%%%" [] "%%%")
+  (Verso.Syntax.metadata_block
+   "%%%"
+   (Term.structInstFields [])
+   "%%%")
 All input consumed.
 -/
 #guard_msgs in
@@ -1620,11 +1623,11 @@ All input consumed.
 info: Success! Final stack:
   (Verso.Syntax.metadata_block
    "%%%"
-   [(Term.structInstField
-     (Term.structInstLVal `foo [])
-     ":="
-     `bar)
-    []]
+   (Term.structInstFields
+    [(Term.structInstField
+      (Term.structInstLVal `foo [])
+      [[] [] (Term.structInstFieldDef ":=" `bar)])
+     []])
    "%%%")
 All input consumed.
 -/
@@ -1635,13 +1638,15 @@ All input consumed.
 info: Success! Final stack:
   (Verso.Syntax.metadata_block
    "%%%"
-   [(Term.structInstField
-     (Term.structInstLVal `foo [])
-     ":="
-     `bar)
-    []
-    (Term.structInstFieldAbbrev `x)
-    []]
+   (Term.structInstFields
+    [(Term.structInstField
+      (Term.structInstLVal `foo [])
+      [[] [] (Term.structInstFieldDef ":=" `bar)])
+     []
+     (Term.structInstField
+      (Term.structInstLVal `x [])
+      [])
+     []])
    "%%%")
 All input consumed.
 -/
@@ -3025,11 +3030,15 @@ Remaining:
 info: Success! Final stack:
   [(Verso.Syntax.metadata_block
     "%%%"
-    [(Term.structInstField
-      (Term.structInstLVal `foo [])
-      ":="
-      (num "53"))
-     []]
+    (Term.structInstFields
+     [(Term.structInstField
+       (Term.structInstLVal `foo [])
+       [[]
+        []
+        (Term.structInstFieldDef
+         ":="
+         (num "53"))])
+      []])
     "%%%")
    (Verso.Syntax.para
     "para{"

src/verso/Verso/Syntax.lean

@@ -73,7 +73,7 @@ syntax (name:=header) inline* : block
 open Lean.Parser.Term in
 
 open Lean.Parser Term in
-def metadataContents := sepByIndent (structInstFieldAbbrev <|> structInstField) ", " (allowTrailingSep := true)
+def metadataContents := structInstFields (sepByIndent structInstField ", " (allowTrailingSep := true))
 
 /-- Metadata for this section, defined by the current genre -/
 syntax (name:=metadata_block) "%%%" metadataContents "%%%" : block