max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: make .lean hashes cross-platform compatible (leanprover/lake#170)

Browse source
This commit is contained in:
Sebastian Ullrich 2023-05-23 14:10:19 +02:00 • committed by GitHub
parent 72487e5650
commit a32c3e0140
3 changed files with 212 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
Lake/Build/Module.lean
View file

@ -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

13
Lake/Build/Trace.lean
View file

@ -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 :=

198
flake.lock generated Normal file
View file

@ -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
}