Skip to content

Commit

Permalink
hash module name instead of path
Browse files Browse the repository at this point in the history
  • Loading branch information
joneugster committed Feb 13, 2025
1 parent ecaadfe commit cf75039
Showing 1 changed file with 2 additions and 12 deletions.
14 changes: 2 additions & 12 deletions Cache/Hashing.lean
Original file line number Diff line number Diff line change
Expand Up @@ -139,19 +139,9 @@ partial def getHash (mod : Name) (sourceFile : FilePath) (visited : Std.HashSet
-- one import did not have a hash: invalidate hash of this module
modify fun stt => { stt with cache := stt.cache.insert mod none }
return none
/-
TODO: Currently, the cache uses the hash of the unresolved file name
(e.g. `Mathlib/Init.lean`) which is reconstructed from the module name
(e.g. `Mathlib.Init`) in `path`. It could, however, directly use `hash mod` instead.
We can change this at any time causing a one-time cache invalidation, just as
a toolchain-bump would.
-/
let filePath := mkFilePath (mod.components.map toString) |>.withExtension "lean"

let rootHash := (← get).rootHash
let pathHash := hash filePath.components -- TODO: change to `hash mod`
let fileHash := hash <| rootHash :: pathHash :: hashFileContents content :: importHashes.toList
let modHash := hash mod
let fileHash := hash <| rootHash :: modHash :: hashFileContents content :: importHashes.toList
if isPartOfMathlibCache mod then
-- mathlib/upstream: add hash to `hashMap`
modifyGet fun stt =>
Expand Down

0 comments on commit cf75039

Please sign in to comment.