Skip to content

Commit

Permalink
doc(Cache/Hashing): add docstring for HashMemo (#21711)
Browse files Browse the repository at this point in the history
  • Loading branch information
joneugster committed Feb 12, 2025
1 parent 2ae982b commit f08a2f6
Showing 1 changed file with 18 additions and 0 deletions.
18 changes: 18 additions & 0 deletions Cache/Hashing.lean
Original file line number Diff line number Diff line change
Expand Up @@ -11,10 +11,28 @@ namespace Cache.Hashing

open System IO

/--
The `HashMemo` contains all information `Cache` needs about the modules:
* the name
* its imports
* the file's hash (in `hashMap` and `cache`)
additionally, it contains the `rootHash` which reflects changes to Mathlib's
Lake project settings.
-/
structure HashMemo where
/-- Hash of mathlib's lake project settings. -/
rootHash : UInt64
/-- Maps the `.lean` file of a module to the `.lean` files of its imports. -/
depsMap : Std.HashMap FilePath (Array FilePath) := ∅
/--
For files with a valid hash (usually Mathlib and upstream),
this contains the same information as `hashMap`.
Other files have `none` here and do not appear in `hashMap`
(e.g. `.lean` source could not be found, imports a file without valid hash).
-/
cache : Std.HashMap FilePath (Option UInt64) := ∅
/-- Stores the hash of the module's content for modules in Mathlib or upstream. -/
hashMap : ModuleHashMap := ∅
deriving Inhabited

Expand Down

0 comments on commit f08a2f6

Please sign in to comment.