diff --git a/Lake/Build/Module.lean b/Lake/Build/Module.lean index 528a86db47..f9f1012e5e 100644 --- a/Lake/Build/Module.lean +++ b/Lake/Build/Module.lean @@ -16,7 +16,7 @@ def Module.buildUnlessUpToDate (mod : Module) (depTrace : BuildTrace) : BuildM PUnit := do let isOldMode ← getIsOldMode let argTrace : BuildTrace := pureHash mod.leanArgs - let srcTrace : BuildTrace ← computeTrace mod.leanFile + let srcTrace : BuildTrace ← computeTrace { path := mod.leanFile : TextFilePath } let modTrace := (← getLeanTrace).mix <| argTrace.mix <| srcTrace.mix depTrace let modUpToDate ← do if isOldMode then diff --git a/Lake/Build/Trace.lean b/Lake/Build/Trace.lean index 41d89c86b5..0c63b1345d 100644 --- a/Lake/Build/Trace.lean +++ b/Lake/Build/Trace.lean @@ -131,6 +131,18 @@ def computeFileHash (file : FilePath) : IO Hash := instance : ComputeHash FilePath IO := ⟨computeFileHash⟩ +/-- + A wrapper around `FilePath` that adjusts its `ComputeHash` implementation + to normalize `\r\n` sequences to `\n` for cross-platform compatibility. -/ +structure TextFilePath where + path : FilePath + +instance : ComputeHash TextFilePath IO where + computeHash file := do + let text ← IO.FS.readFile file.path + let text := text.replace "\r\n" "\n" + return Hash.ofString text + instance [ComputeHash α m] [Monad m] : ComputeHash (Array α) m where computeHash ar := ar.foldlM (fun b a => Hash.mix b <$> computeHash a) Hash.nil @@ -171,6 +183,7 @@ def getFileMTime (file : FilePath) : IO MTime := return (← file.metadata).modified instance : GetMTime FilePath := ⟨getFileMTime⟩ +instance : GetMTime TextFilePath := ⟨(getFileMTime ·.path)⟩ /-- Check if the info's `MTIme` is at least `depMTime`. -/ def checkIfNewer [GetMTime i] (info : i) (depMTime : MTime) : BaseIO Bool := diff --git a/flake.lock b/flake.lock new file mode 100644 index 0000000000..c7847cf374 --- /dev/null +++ b/flake.lock @@ -0,0 +1,198 @@ +{ + "nodes": { + "flake-utils": { + "inputs": { + "systems": "systems" + }, + "locked": { + "lastModified": 1681202837, + "narHash": "sha256-H+Rh19JDwRtpVPAWp64F+rlEtxUWBAQW28eAi3SRSzg=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "cfacdce06f30d2b68473a46042957675eebb3401", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "flake-utils_2": { + "locked": { + "lastModified": 1656928814, + "narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "lean": { + "inputs": { + "flake-utils": "flake-utils_2", + "lean4-mode": "lean4-mode", + "nix": "nix", + "nixpkgs": "nixpkgs_2" + }, + "locked": { + "lastModified": 1684657055, + "narHash": "sha256-88pPIe514ltykRuMjyaX9Wutm/xK18m7e+2awQnjBA8=", + "owner": "leanprover", + "repo": "lean4", + "rev": "8d4dd2311ccfa3de8dbcaba015b52e3ae1ed308d", + "type": "github" + }, + "original": { + "owner": "leanprover", + "repo": "lean4", + "type": "github" + } + }, + "lean4-mode": { + "flake": false, + "locked": { + "lastModified": 1676498134, + "narHash": "sha256-u3WvyKxOViZG53hkb8wd2/Og6muTecbh+NdflIgVeyk=", + "owner": "leanprover", + "repo": "lean4-mode", + "rev": "2c6ef33f476fdf5eb5e4fa4fa023ba8b11372440", + "type": "github" + }, + "original": { + "owner": "leanprover", + "repo": "lean4-mode", + "type": "github" + } + }, + "lowdown-src": { + "flake": false, + "locked": { + "lastModified": 1633514407, + "narHash": "sha256-Dw32tiMjdK9t3ETl5fzGrutQTzh2rufgZV4A/BbxuD4=", + "owner": "kristapsdz", + "repo": "lowdown", + "rev": "d2c2b44ff6c27b936ec27358a2653caaef8f73b8", + "type": "github" + }, + "original": { + "owner": "kristapsdz", + "repo": "lowdown", + "type": "github" + } + }, + "nix": { + "inputs": { + "lowdown-src": "lowdown-src", + "nixpkgs": "nixpkgs", + "nixpkgs-regression": "nixpkgs-regression" + }, + "locked": { + "lastModified": 1657097207, + "narHash": "sha256-SmeGmjWM3fEed3kQjqIAO8VpGmkC2sL1aPE7kKpK650=", + "owner": "NixOS", + "repo": "nix", + "rev": "f6316b49a0c37172bca87ede6ea8144d7d89832f", + "type": "github" + }, + "original": { + "owner": "NixOS", + "repo": "nix", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1653988320, + "narHash": "sha256-ZaqFFsSDipZ6KVqriwM34T739+KLYJvNmCWzErjAg7c=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "2fa57ed190fd6c7c746319444f34b5917666e5c1", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixos-22.05-small", + "repo": "nixpkgs", + "type": "github" + } + }, + "nixpkgs-regression": { + "locked": { + "lastModified": 1643052045, + "narHash": "sha256-uGJ0VXIhWKGXxkeNnq4TvV3CIOkUJ3PAoLZ3HMzNVMw=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2", + "type": "github" + }, + "original": { + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2", + "type": "github" + } + }, + "nixpkgs_2": { + "locked": { + "lastModified": 1657208011, + "narHash": "sha256-BlIFwopAykvdy1DYayEkj6ZZdkn+cVgPNX98QVLc0jM=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "2770cc0b1e8faa0e20eb2c6aea64c256a706d4f2", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixpkgs-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, + "nixpkgs_3": { + "locked": { + "lastModified": 1659914493, + "narHash": "sha256-lkA5X3VNMKirvA+SUzvEhfA7XquWLci+CGi505YFAIs=", + "owner": "nixos", + "repo": "nixpkgs", + "rev": "022caabb5f2265ad4006c1fa5b1ebe69fb0c3faf", + "type": "github" + }, + "original": { + "owner": "nixos", + "ref": "nixos-21.05", + "repo": "nixpkgs", + "type": "github" + } + }, + "root": { + "inputs": { + "flake-utils": "flake-utils", + "lean": "lean", + "nixpkgs": "nixpkgs_3" + } + }, + "systems": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + } + }, + "root": "root", + "version": 7 +}