forked from argumentcomputer/yatima
-
Notifications
You must be signed in to change notification settings - Fork 0
/
lakefile.lean
146 lines (117 loc) · 4.76 KB
/
lakefile.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
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
import Lake
open Lake DSL
package Yatima
@[default_target]
lean_exe yatima where
supportInterpreter := true
root := `Main
lean_lib Yatima { roots := #[`Yatima] }
require LSpec from git
"https://github.com/lurk-lab/LSpec.git" @ "88f7d23e56a061d32c7173cea5befa4b2c248b41"
require YatimaStdLib from git
"https://github.com/lurk-lab/YatimaStdLib.lean" @ "10f2b444390a41ede90ca5c038c6ff972014d433"
require Cli from git
"https://github.com/lurk-lab/Cli.lean" @ "ef6f9bcd1738638fca8d319dbee653540d56614e"
require Lurk from git
"https://github.com/lurk-lab/Lurk.lean" @ "283a4008a606bccb109eda55c80a5eae39a62788"
require LightData from git
"https://github.com/lurk-lab/LightData" @ "6dfd01c9e056deaf5b76e20f995c39e840bbde86"
require std from git
"https://github.com/leanprover/std4/" @ "fde95b16907bf38ea3f310af406868fc6bcf48d1"
section Testing
lean_lib TestsUtils
lean_lib Fixtures {
roots := #[
`Fixtures.AnonGroups.ToBeImported,
`Fixtures.AnonGroups.ToImport,
`Fixtures.Termination.Init.Prelude,
`Fixtures.Termination.Init.Coe,
`Fixtures.Termination.Init.Notation,
`Fixtures.Termination.Init.Tactics,
`Fixtures.Termination.Init.SizeOf,
`Fixtures.Termination.Init.Core]
}
lean_exe Tests.AnonGroups.Definitions { supportInterpreter := true }
lean_exe Tests.AnonGroups.Inductives { supportInterpreter := true }
lean_exe Tests.AnonGroups.ToImport { supportInterpreter := true }
lean_exe Tests.Termination.NastyInductives { supportInterpreter := true }
lean_exe Tests.Termination.TrickyDef { supportInterpreter := true }
lean_exe Tests.Termination.Init { supportInterpreter := true }
lean_exe Tests.CodeGeneration.Primitives { supportInterpreter := true }
lean_exe Tests.CodeGeneration.TrickyTypes { supportInterpreter := true }
lean_exe Tests.Typechecker.Accept { supportInterpreter := true }
lean_exe Tests.Typechecker.Reject { supportInterpreter := true }
lean_exe Tests.Typechecker.TypecheckInLurk { supportInterpreter := true }
end Testing
section Setup
def runCmd (cmd : String) : ScriptM $ Except String String := do
let cmd := cmd.splitOn " "
if h : cmd ≠ [] then
let (cmd, args) := match h' : cmd with
| cmd :: args => (cmd, ⟨args⟩)
| [] => absurd h' (h' ▸ h)
let out ← IO.Process.output {
cmd := cmd
args := args
}
return if out.exitCode != 0
then .error out.stderr
else .ok out.stdout
else return .ok ""
script setup do
IO.println "building yatima"
match ← runCmd "lake exe yatima pin" with
| .error e => IO.eprintln e; return 1
| .ok _ =>
match ← runCmd "lake build" with
| .error e => IO.eprintln e; return 1
| .ok _ => pure ()
let binDir ← match ← IO.getEnv "HOME" with
| some homeDir =>
let binDir : FilePath := homeDir / ".local" / "bin"
IO.print s!"target directory for the yatima binary? (default={binDir}) "
let input := (← (← IO.getStdin).getLine).trim
pure $ if input.isEmpty then binDir else ⟨input⟩
| none =>
IO.print s!"target directory for the yatima binary? "
let binDir := (← (← IO.getStdin).getLine).trim
if binDir.isEmpty then
IO.eprintln "target directory can't be empty"; return 1
pure ⟨binDir⟩
IO.FS.writeBinFile (binDir / "yatima")
(← IO.FS.readBinFile $ "build" / "bin" / "yatima")
IO.println s!"yatima binary placed at {binDir}"
IO.println "compiling and hashing the typechecker"
match ← runCmd "lake exe yatima gentc" with
| .error err => IO.eprintln err; return 1
| .ok out => IO.print out; return 0
end Setup
section ImportAll
open System
partial def getLeanFilePaths (fp : FilePath) (acc : Array FilePath := #[]) :
IO $ Array FilePath := do
if ← fp.isDir then
(← fp.readDir).foldlM (fun acc dir => getLeanFilePaths dir.path acc) acc
else return if fp.extension == some "lean" then acc.push fp else acc
open Lean (RBTree)
def getAllFiles : ScriptM $ List String := do
let paths := (← getLeanFilePaths ⟨"Yatima"⟩).map toString
let paths : RBTree String compare := RBTree.ofList paths.toList -- ordering
return paths.toList
def getImportsString : ScriptM String := do
let paths ← getAllFiles
let imports := paths.map fun p =>
"import " ++ (p.splitOn ".").head!.replace "/" "."
return s!"{"\n".intercalate imports}\n"
script import_all do
IO.FS.writeFile ⟨"Yatima.lean"⟩ (← getImportsString)
return 0
script import_all? do
let importsFromUser ← IO.FS.readFile ⟨"Yatima.lean"⟩
let expectedImports ← getImportsString
if importsFromUser != expectedImports then
IO.eprintln "Invalid import list in 'Yatima.lean'"
IO.eprintln "Try running 'lake run import_all'"
return 1
return 0
end ImportAll