Merge pull request #227 from leanprover/bump_to_v4.14.0-rc1

chore: bump toolchain to v4.14.0-rc1
leanprover · Nov 4, 2024 · b6ae1cf · b6ae1cf
2 parents c2156be + cd6c6b9
commit b6ae1cf
Show file tree

Hide file tree

Showing 5 changed files with 6 additions and 6 deletions.
diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean
@@ -199,7 +199,7 @@ def autoLink (el : Element) : HtmlM Element := do
     for c in contents do
       match c with
       | Content.Character s =>
-        newContents := newContents ++ (← splitAround s unicodeToSplit |>.mapM linkify).join
+        newContents := newContents ++ (← splitAround s unicodeToSplit |>.mapM linkify).flatten
       | _ => newContents := newContents.push c
     return ⟨ name, attrs, newContents ⟩
   where

diff --git a/DocGen4/Output/References.lean b/DocGen4/Output/References.lean
@@ -74,7 +74,7 @@ def refItem (ref : BibItem) (backrefs : Array BackrefItem) : BaseHtmlM Html := d
     if backrefs.isEmpty then
       pure (.raw "")
     else
-      pure <small>[(← backrefs.mapIdxM toHtml).foldl (· ++ ·) #[]]</small>)
+      pure <small>[(← backrefs.mapFinIdxM toHtml).foldl (· ++ ·) #[]]</small>)
   pure <|
     <li id={s!"ref_{ref.citekey}"}>
       <a href={s!"#ref_{ref.citekey}"}>{.text ref.tag}</a>

diff --git a/DocGen4/Process/StructureInfo.lean b/DocGen4/Process/StructureInfo.lean
@@ -34,7 +34,7 @@ def getFieldTypes (v : InductiveVal) : MetaM (Array NameInfo) := do
 def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do
   let info ← Info.ofConstantVal v.toConstantVal
   let env ← getEnv
-  let parents := getParentStructures env v.name
+  let parents ← getAllParentStructures v.name
   let ctorVal := getStructureCtor env v.name
   let ctor ← NameInfo.ofTypedName ctorVal.name ctorVal.type
   match getStructureInfo? env v.name with

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "107e98b3e7603628d9bfd817b4704488d8a25e96",
+   "rev": "b41bc9cec7f433d6e1d74ff3b59edaaf58ad2915",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
+   "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.13.0
+leanprover/lean4:v4.14.0-rc1
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.13.0
		leanprover/lean4:v4.14.0-rc1