-
Notifications
You must be signed in to change notification settings - Fork 251
/
Utils.lean
59 lines (49 loc) · 2.03 KB
/
Utils.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
import Lean.Data.HashMap
open System
partial def getLeanFilePaths (fp : FilePath) (acc : Array FilePath := #[]) :
IO $ Array FilePath := do
if ← fp.isDir then
let mut extra : Array FilePath := #[]
for dirEntry in ← fp.readDir do
for innerFp in ← getLeanFilePaths dirEntry.path do
extra := extra.push innerFp
return acc.append extra
else match fp.extension with
| some "lean" => return acc.push fp
| _ => return acc
/-- Extracts the relevant imports of a Lean source code -/
def getFileImports (content : String) : List FilePath :=
let importLines := content.splitOn "\n" |>.filter (·.startsWith "import Mathlib.")
let imports := importLines.map fun line =>
let line := (line.splitOn "import ").get! 1
|>.replace "." "/"
|>.splitOn " "
|>.head!
line ++ ".lean"
imports.map FilePath.mk
/-- We store the root hash as a reader and cache the hash of each file for faster lookup -/
abbrev HashM := ReaderT UInt64 $ StateT (Lean.HashMap FilePath UInt64) IO
partial def getFileHash (filePath : FilePath) : HashM UInt64 := do
match (← get).find? filePath with
| some hash => pure hash
| none =>
let content ← IO.FS.readFile filePath
let imports := getFileImports content
let importHashes ← imports.mapM getFileHash
let fileHash := hash $ (← read) :: content.hash :: importHashes
modifyGet fun hashMap => (fileHash, hashMap.insert filePath fileHash)
def cacheHashes : HashM Unit := do
let leanFilePaths ← getLeanFilePaths ⟨"Mathlib"⟩
leanFilePaths.forM (discard $ getFileHash ·)
def getRootHash : IO UInt64 :=
return hash [
← IO.FS.readFile ⟨"lakefile.lean"⟩,
← IO.FS.readFile ⟨"lean-toolchain"⟩,
← IO.FS.readFile ⟨"lake-manifest.json"⟩
]
def getHashes : IO $ Lean.HashMap FilePath UInt64 :=
return (← StateT.run (ReaderT.run cacheHashes (← getRootHash)) default).2
def libDir : FilePath :=
"build" / "lib"
def oLeanFilePath (leanFilePath : FilePath) : FilePath :=
libDir / leanFilePath.withExtension "olean"