From a0fb5e8d41644aeb42c649e281ceb7caf20e2b1e Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 3 Sep 2024 13:43:15 +1000 Subject: [PATCH 1/3] chore: bump toolchain to v4.12.0-rc1 --- lake-manifest.json | 2 +- lean-toolchain | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 4d7d749..2466dd3 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "929690af200efb291babee737b087d244a70c3c3", + "rev": "7f31364c8263a8898b53f563ac335fbc838f7a2d", "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lean-toolchain b/lean-toolchain index 5a9c76d..98556ba 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.11.0 +leanprover/lean4:v4.12.0-rc1 From c5b5ddf131ef93bb5a7d6a6be935ab1ef438dd40 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Tue, 3 Sep 2024 20:49:26 +0200 Subject: [PATCH 2/3] upgrade to new hashmap --- DocGen4/Load.lean | 3 --- DocGen4/Output.lean | 1 - DocGen4/Output/Base.lean | 4 ++-- DocGen4/Output/DocString.lean | 21 ++++++++++++--------- DocGen4/Output/Module.lean | 2 +- DocGen4/Output/ToJson.lean | 14 +++++++------- DocGen4/Process/Analyze.lean | 20 ++++++++++---------- DocGen4/Process/Hierarchy.lean | 8 ++------ 8 files changed, 34 insertions(+), 39 deletions(-) diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean index 260cc56..929d492 100644 --- a/DocGen4/Load.lean +++ b/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 diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 0411a46..e61632a 100644 --- a/DocGen4/Output.lean +++ b/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 diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index a15113d..3c0ab73 100644 --- a/DocGen4/Output/Base.lean +++ b/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 /-- diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index ec7150f..6553c55 100644 --- a/DocGen4/Output/DocString.lean +++ b/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 is fixed diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index 226bdbf..69bf23b 100644 --- a/DocGen4/Output/Module.lean +++ b/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 diff --git a/DocGen4/Output/ToJson.lean b/DocGen4/Output/ToJson.lean index 8c56185..b3634b9 100644 --- a/DocGen4/Output/ToJson.lean +++ b/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) diff --git a/DocGen4/Process/Analyze.lean b/DocGen4/Process/Analyze.lean index 90191fb..5462458 100644 --- a/DocGen4/Process/Analyze.lean +++ b/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,7 +46,7 @@ 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`. -/ @@ -54,7 +54,7 @@ structure AnalyzerResult where /-- 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 diff --git a/DocGen4/Process/Hierarchy.lean b/DocGen4/Process/Hierarchy.lean index 185c2ce..58f428a 100644 --- a/DocGen4/Process/Hierarchy.lean +++ b/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", From b75e7061690eb98a326106a61d5b6bc14202d544 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Tue, 3 Sep 2024 22:54:12 +0200 Subject: [PATCH 3/3] chore: update dependencies again --- lake-manifest.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 2466dd3..4cbff7f 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "7f31364c8263a8898b53f563ac335fbc838f7a2d", + "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",