chore: bump toolchain to v4.12.0-rc1

DocGen4/Load.lean

@@ -3,10 +3,7 @@ Copyright (c) 2021 Henrik Böving. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-
-import Lean
 import DocGen4.Process
-import Lean.Data.HashMap
 
 namespace DocGen4
 

DocGen4/Output.lean

@@ -16,7 +16,6 @@ import DocGen4.Output.SourceLinker
 import DocGen4.Output.Search
 import DocGen4.Output.ToJson
 import DocGen4.Output.FoundationalTypes
-import Lean.Data.HashMap
 
 namespace DocGen4
 

DocGen4/Output/Base.lean

@@ -81,7 +81,7 @@ structure SiteContext where
   /--
   The references as a map.
   -/
-  refsMap : HashMap String BibItem
+  refsMap : Std.HashMap String BibItem
 
 /--
 The writable state used in the `HtmlM` monad for HTML templating.
@@ -211,7 +211,7 @@ Returns the doc-gen4 link to a declaration name.
 -/
 def declNameToLink (name : Name) : HtmlM String := do
   let res ← getResult
-  let module := res.moduleNames[res.name2ModIdx.find! name |>.toNat]!
+  let module := res.moduleNames[res.name2ModIdx[name]!.toNat]!
   return (← moduleNameToLink module) ++ "#" ++ name.toString
 
 /--

DocGen4/Output/DocString.lean

@@ -1,9 +1,12 @@
 import MD4Lean
 import DocGen4.Output.Template
-import Lean.Data.Parsec
+import Std.Internal.Parsec
 import UnicodeBasic
 
-open Lean Xml Parser Parsec DocGen4.Process
+open Lean Xml Parser DocGen4.Process
+
+open Std.Internal.Parsec
+open Std.Internal.Parsec.String
 
 namespace DocGen4
 namespace Output
@@ -30,7 +33,7 @@ def splitAround (s : String) (p : Char → Bool) : List String := splitAroundAux
 instance : Inhabited Element := ⟨"", Lean.RBMap.empty, #[]⟩
 
 /-- Parse an array of Xml/Html document from String. -/
-def manyDocument : Parsec (Array Element) := many (prolog *> element <* many Misc) <* eof
+def manyDocument : Parser (Array Element) := many (prolog *> element <* many Misc) <* eof
 
 /--
   Generate id for heading elements, with the following rules:
@@ -83,7 +86,7 @@ def nameToLink? (s : String) : HtmlM (Option String) := do
     else
       match (← getCurrentName) with
       | some currentName =>
-        match res.moduleInfo.find! currentName |>.members |> filterDocInfo |>.find? (sameEnd ·.getName name) with
+        match res.moduleInfo[currentName]! |>.members |> filterDocInfo |>.find? (sameEnd ·.getName name) with
         | some info =>
           declNameToLink info.getName
         | _ => return none
@@ -159,7 +162,7 @@ def addHeadingAttributes (el : Element) (funName : String)
 /-- Find a bibitem if `href` starts with `thePrefix`. -/
 def findBibitem? (href : String) (thePrefix : String := "") : HtmlM (Option BibItem) := do
   if href.startsWith thePrefix then
-    pure <| (← read).refsMap.find? (href.drop thePrefix.length)
+    pure <| (← read).refsMap[href.drop thePrefix.length]?
   else
     pure .none
 
@@ -246,14 +249,14 @@ partial def modifyElement (element : Element) (funName : String) : HtmlM Element
       return ⟨ name, attrs, ← modifyContents contents funName modifyElement ⟩
 
 /-- Find all references in a markdown text. -/
-partial def findAllReferences (refsMap : HashMap String BibItem) (s : String) (i : String.Pos := 0)
-    (ret : HashSet String := .empty) : HashSet String :=
+partial def findAllReferences (refsMap : Std.HashMap String BibItem) (s : String) (i : String.Pos := 0)
+    (ret : Std.HashSet String := .empty) : Std.HashSet String :=
   let lps := s.posOfAux '[' s.endPos i
   if lps < s.endPos then
     let lpe := s.posOfAux ']' s.endPos lps
     if lpe < s.endPos then
       let citekey := Substring.toString ⟨s, ⟨lps.1 + 1⟩, lpe⟩
-      match refsMap.find? citekey with
+      match refsMap[citekey]? with
       | .some _ => findAllReferences refsMap s lpe (ret.insert citekey)
       | .none => findAllReferences refsMap s lpe ret
     else
@@ -269,7 +272,7 @@ def docStringToHtml (docString : String) (funName : String) : HtmlM (Array Html)
   match MD4Lean.renderHtml (docString ++ refsMarkdown) with
   | .some rendered =>
     match manyDocument rendered.mkIterator with
-    | Parsec.ParseResult.success _ res =>
+    | .success _ res =>
       let newRes ← modifyElements res funName modifyElement
       -- TODO: use `toString` instead of `eToStringEscaped`
       -- once <https://github.com/leanprover/lean4/issues/4411> is fixed

DocGen4/Output/Module.lean

@@ -159,7 +159,7 @@ Returns the list of all imports this module does.
 -/
 def getImports (module : Name) : HtmlM (Array Name) := do
   let res ← getResult
-  return res.moduleInfo.find! module |>.imports
+  return res.moduleInfo[module]!.imports
 
 /--
 Sort the list of all modules this one is importing, linkify it

DocGen4/Output/ToJson.lean

@@ -50,9 +50,9 @@ structure JsonIndexedModule where
 
 structure JsonIndex where
   declarations : List (String × JsonIndexedDeclarationInfo) := []
-  instances : HashMap String (RBTree String Ord.compare) := .empty
-  modules : HashMap String JsonIndexedModule := {}
-  instancesFor : HashMap String (RBTree String Ord.compare) := .empty
+  instances : Std.HashMap String (RBTree String Ord.compare) := .empty
+  modules : Std.HashMap String JsonIndexedModule := {}
+  instancesFor : Std.HashMap String (RBTree String Ord.compare) := .empty
 
 instance : ToJson JsonHeaderIndex where
   toJson idx := Json.mkObj <| idx.declarations.map (fun (k, v) => (k, toJson v))
@@ -87,23 +87,23 @@ def JsonIndex.addModule (index : JsonIndex) (module : JsonModule) : BaseHtmlM Js
 
   -- TODO: In theory one could sort instances and imports by name and batch the writes
   for inst in module.instances do
-    let mut insts := index.instances.findD inst.className {}
+    let mut insts := index.instances.getD inst.className {}
     insts := insts.insert inst.name
     index := { index with instances := index.instances.insert inst.className insts }
     for typeName in inst.typeNames do
-      let mut instsFor := index.instancesFor.findD typeName {}
+      let mut instsFor := index.instancesFor.getD typeName {}
       instsFor := instsFor.insert inst.name
       index := { index with instancesFor := index.instancesFor.insert typeName instsFor }
 
   -- TODO: dedup
-  if index.modules.find? module.name |>.isNone then
+  if index.modules[module.name]?.isNone then
     let moduleLink ← moduleNameToLink (String.toName module.name)
     let indexedModule := { url := moduleLink, importedBy := #[] }
     index := { index with modules := index.modules.insert module.name indexedModule }
 
   for imp in module.imports do
     let indexedImp ←
-      match index.modules.find? imp with
+      match index.modules[imp]? with
       | some i => pure i
       | none =>
         let impLink ← moduleNameToLink (String.toName imp)

DocGen4/Process/Analyze.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 
-import Lean
-import Lean.Data.HashMap
-import Lean.Data.HashSet
+import Lean.Meta.Basic
+import Std.Data.HashMap
+import Std.Data.HashSet
 
 import DocGen4.Process.Base
 import DocGen4.Process.Hierarchy
@@ -46,15 +46,15 @@ structure AnalyzerResult where
   /--
   The map from module names to indices of the `moduleNames` array.
   -/
-  name2ModIdx : HashMap Name ModuleIdx
+  name2ModIdx : Std.HashMap Name ModuleIdx
   /--
   The list of all modules, accessible nicely via `name2ModIdx`.
   -/
   moduleNames : Array Name
   /--
   A map from module names to information about these modules.
   -/
-  moduleInfo : HashMap Name Module
+  moduleInfo : Std.HashMap Name Module
   deriving Inhabited
 
 namespace ModuleMember
@@ -91,9 +91,9 @@ def AnalyzeTask.getLoad : AnalyzeTask → Array Name
 | loadAll load => load
 | loadAllLimitAnalysis load => load
 
-def getAllModuleDocs (relevantModules : Array Name) : MetaM (HashMap Name Module) := do
+def getAllModuleDocs (relevantModules : Array Name) : MetaM (Std.HashMap Name Module) := do
   let env ← getEnv
-  let mut res := mkHashMap relevantModules.size
+  let mut res := Std.HashMap.empty relevantModules.size
   for module in relevantModules do
     let modDocs := getModuleDoc? env module |>.getD #[] |>.map .modDoc
     let some modIdx := env.getModuleIdx? module | unreachable!
@@ -109,8 +109,8 @@ of this `MetaM` run and mentioned by the `AnalyzeTask`.
 def process (task : AnalyzeTask) : MetaM (AnalyzerResult × Hierarchy) := do
   let env ← getEnv
   let relevantModules := match task with
-    | .loadAll _ => HashSet.fromArray env.header.moduleNames
-    | .loadAllLimitAnalysis analysis => HashSet.fromArray analysis
+    | .loadAll _ => Std.HashSet.insertMany {} env.header.moduleNames
+    | .loadAllLimitAnalysis analysis => Std.HashSet.insertMany {} analysis
   let allModules := env.header.moduleNames
 
   let mut res ← getAllModuleDocs relevantModules.toArray
@@ -132,7 +132,7 @@ def process (task : AnalyzeTask) : MetaM (AnalyzerResult × Hierarchy) := do
         let analysis ← Prod.fst <$> Meta.MetaM.toIO (DocInfo.ofConstant (name, cinfo)) config { env := env } {} {}
         if let some dinfo := analysis then
           let moduleName := env.allImportedModuleNames.get! modidx
-          let module := res.find! moduleName
+          let module := res[moduleName]!
           return res.insert moduleName {module with members := module.members.push (ModuleMember.docInfo dinfo)}
         else
           return res

DocGen4/Process/Hierarchy.lean

@@ -4,10 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 import Lean
-import Lean.Data.HashMap
-
-def Lean.HashSet.fromArray [BEq α] [Hashable α] (xs : Array α) : Lean.HashSet α :=
-  xs.foldr (flip .insert) .empty
 
 namespace DocGen4
 
@@ -81,8 +77,8 @@ partial def insert! (h : Hierarchy) (n : Name) : Hierarchy := Id.run do
 partial def fromArray (names : Array Name) : Hierarchy :=
   names.foldl insert! (empty anonymous false)
 
-def baseDirBlackList : HashSet String :=
-  HashSet.fromArray #[
+def baseDirBlackList : Std.HashSet String :=
+  Std.HashSet.ofList [
     "404.html",
     "color-scheme.js",
     "declaration-data.js",

lake-manifest.json

@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "929690af200efb291babee737b087d244a70c3c3",
+   "rev": "7afce91e4fcee25c1ed06dca8d71b82bed396776",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c138ab5c566c4268798b24bfcbea2f4c42413cdd",
+   "rev": "0a294fe9bf23b396c5cc955054c50b9b652ec5ad",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.11.0
+leanprover/lean4:v4.12.0-rc1