Merge pull request #264 from leanprover/bump_to_v4.17.0-rc1

chore: bump toolchain to v4.17.0-rc1

DocGen4/Output/References.lean

@@ -65,16 +65,16 @@ open scoped DocGen4.Jsx
 
 def refItem (ref : BibItem) (backrefs : Array BackrefItem) : BaseHtmlM Html := do
   let backrefs := backrefs.filter (fun x => x.citekey == ref.citekey)
-  let toHtml (i : Fin backrefs.size) (backref : BackrefItem) : BaseHtmlM (Array Html) := do
+  let toHtml (i : Nat) (backref : BackrefItem) : BaseHtmlM (Array Html) := do
     let href := s!"{← moduleNameToLink backref.modName}#_backref_{backref.index}"
     let title := s!"File: {backref.modName}" ++
       if backref.funName.isEmpty then "" else s!"\nLocation: {backref.funName}"
-    pure #[.raw " ", <a href={href} title={title}>{.text s!"[{i.1 + 1}]"}</a>]
+    pure #[.raw " ", <a href={href} title={title}>{.text s!"[{i + 1}]"}</a>]
   let backrefHtml : Html ← (do
     if backrefs.isEmpty then
       pure (.raw "")
     else
-      pure <small>[(← backrefs.mapFinIdxM toHtml).foldl (· ++ ·) #[]]</small>)
+      pure <small>[(← backrefs.mapIdxM toHtml).foldl (· ++ ·) #[]]</small>)
   pure <|
     <li id={s!"ref_{ref.citekey}"}>
       <a href={s!"#ref_{ref.citekey}"}>{.text ref.tag}</a>

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d835296a6149acb9bd2ff65ec01b728b9cc99a1c",
+   "rev": "a2eb24a3dbf681f2b655f82ba5ee5b139d4a5abc",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,20 +15,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e86d905bf1453554ea60a853e275bd9de30e0501",
+   "rev": "d890360c960358a42965bdc15defa3fd09feba38",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/dupuisf/BibtexQuery",
+  {"url": "https://github.com/kim-em/BibtexQuery",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9e99cb8cd9ba6906472634e6973c7e27482a70bb",
+   "rev": "2411c47ee06f2fc986d929e22731c77e61eaadb6",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "bump_to_v4.17.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/acmepjz/md4lean",

lakefile.lean

@@ -14,8 +14,11 @@ lean_exe «doc-gen4» {
 require MD4Lean from git
   "https://github.com/acmepjz/md4lean" @ "main"
 
+-- Once https://github.com/dupuisf/BibtexQuery/pull/20 is merged, we can use this again:
+-- require BibtexQuery from git
+--   "https://github.com/dupuisf/BibtexQuery" @ "master"
 require BibtexQuery from git
-  "https://github.com/dupuisf/BibtexQuery" @ "master"
+  "https://github.com/kim-em/BibtexQuery" @ "bump_to_v4.17.0-rc1"
 
 require «UnicodeBasic» from git
   "https://github.com/fgdorais/lean4-unicode-basic" @ "main"
@@ -156,7 +159,7 @@ module_facet docs (mod) : FilePath := do
   let bibPrepassJob ← bibPrepass.fetch
   let modJob ← mod.leanArts.fetch
   -- Build all documentation imported modules
-  let imports ← mod.imports.fetch
+  let imports ← (← mod.imports.fetch).await
   let depDocJobs := Job.mixArray <| ← imports.mapM fun mod => fetch <| mod.facet `docs
   let srcUri ← getSrcUri mod
   let buildDir := (← getRootPackage).buildDir
@@ -195,7 +198,7 @@ target coreDocs : Unit := do
   return Job.mixArray <| ← coreComponents.mapM coreTarget
 
 library_facet docs (lib) : FilePath := do
-  let mods ← lib.modules.fetch
+  let mods ← (← lib.modules.fetch).await
   let moduleJobs := Job.mixArray <| ← mods.mapM (fetch <| ·.facet `docs)
   let coreJobs ← coreDocs.fetch
   let exeJob ← «doc-gen4».fetch
@@ -237,7 +240,7 @@ library_facet docs (lib) : FilePath := do
         return dataFile
 
 library_facet docsHeader (lib) : FilePath := do
-  let mods ← lib.modules.fetch
+  let mods ← (← lib.modules.fetch).await
   let moduleJobs := Job.mixArray <| ← mods.mapM (fetch <| ·.facet `docs)
   let exeJob ← «doc-gen4».fetch
   let coreJobs ← coreDocs.fetch

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.16.0
+leanprover/lean4:v4.17.0-rc1