Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - doc(Cache/Hashing): add docstring for HashMemo #21711

Closed
wants to merge 11 commits into from
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