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.

Sign up for GitHub

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
Closed

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

Changes from 6 commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
917786e
add doc
joneugster Feb 11, 2025
1592c9d
whitespace
joneugster Feb 11, 2025
b505b7d
Merge branch 'master' into eugster/cache_cleanup_doc_hashMemo
joneugster Feb 11, 2025
38d78d6
Merge branch 'master' into eugster/cache_cleanup_doc_hashMemo
joneugster Feb 11, 2025
bc050ab
typo
joneugster Feb 11, 2025
ed792df
Merge remote-tracking branch 'origin/master' into eugster/cache_clean…
joneugster Feb 11, 2025
e251781
Revert "typo"
joneugster Feb 11, 2025
363e5c3
clarify
joneugster Feb 11, 2025
9b90b28
Update Cache/Hashing.lean
joneugster Feb 11, 2025
9bdb648
clarify
joneugster Feb 11, 2025
e88a97b
clarify
joneugster Feb 11, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 18 additions & 2 deletions Cache/Hashing.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,10 +11,26 @@ 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
/-- Stores the imports of a module -/
depsMap : Std.HashMap FilePath (Array FilePath) := ∅
/--
For modules in Mathlib or upstream, this contains the same information
as `hashMap`. Contains `none` if a source file couldn't be found.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is it none only for source files not in mathlib?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

updated the docstring. Files downstream will fall into the latter category, but not necessarily exclusively.

E.g. if you'll write import Mathlib.Data in another mathlib file and try to get cache, this file will have none as Mathlib/Data.lean doesn't exist. (meaning no cache will be retrieved for the file with bad import)

-/
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 Expand Up @@ -61,9 +77,9 @@ Computes the root hash, which mixes the hashes of the content of:
* `lakefile.lean`
* `lean-toolchain`
* `lake-manifest.json`
and the hash of `Lean.gitHash`.
and the hash of `Lean.githash`.

(We hash `Lean.gitHash` in case the toolchain changes even though `lean-toolchain` hasn't.
(We hash `Lean.githash` in case the toolchain changes even though `lean-toolchain` hasn't.
This happens with the `lean-pr-testing-NNNN` toolchains when Lean 4 PRs are updated.)
-/
def getRootHash : CacheM UInt64 := do
Expand Down