Skip to content

Commit

Permalink
fix: add .hash files to the cache (#7291)
Browse files Browse the repository at this point in the history
These files are new in v4.1.0. If we don't cache them (or regenerate them, but they are tiny files so there is no reason not to cache them) then lake gets messed up unless you use the `-R` option in the next `lake build`.



Co-authored-by: Mario Carneiro <di.gama@gmail.com>
  • Loading branch information
digama0 and digama0 committed Sep 21, 2023
1 parent a526f3e commit 1b0c360
Show file tree
Hide file tree
Showing 2 changed files with 5 additions and 2 deletions.
5 changes: 4 additions & 1 deletion Cache/IO.lean
Original file line number Diff line number Diff line change
Expand Up @@ -245,10 +245,13 @@ Each build file also has a `Bool` indicating whether that file is required for c
def mkBuildPaths (path : FilePath) : IO $ List (FilePath × Bool) := do
let packageDir ← getPackageDir path
return [
(packageDir / LIBDIR / path.withExtension "trace", true),
(packageDir / LIBDIR / path.withExtension "trace", true), -- this one has to be first
(packageDir / LIBDIR / path.withExtension "olean", true),
(packageDir / LIBDIR / path.withExtension "olean.hash", true),
(packageDir / LIBDIR / path.withExtension "ilean", true),
(packageDir / LIBDIR / path.withExtension "ilean.hash", true),
(packageDir / IRDIR / path.withExtension "c", true),
(packageDir / IRDIR / path.withExtension "c.hash", true),
(packageDir / LIBDIR / path.withExtension "extra", false)]

/-- Check that all required build files exist. -/
Expand Down
2 changes: 1 addition & 1 deletion lake-manifest.json
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@
{"git":
{"url": "https://github.com/leanprover/std4",
"subDir?": null,
"rev": "67855403d60daf181775fa1ec63b04e70bcc3921",
"rev": "67855403d60daf181775fa1ec63b04e70bcc3921",
"opts": {},
"name": "std",
"inputRev?": "main",
Expand Down

0 comments on commit 1b0c360

Please sign in to comment.