-
Notifications
You must be signed in to change notification settings - Fork 6
/
lakefile.lean
77 lines (60 loc) · 2.43 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
import Lake
open Lake DSL
package YatimaStdLib
@[default_target]
lean_lib YatimaStdLib where
-- https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/error.20loading.20library.20Aesop-Nanos.2Edll/near/316767700
-- precompileModules := true
def ffiC := "ffi.c"
def ffiO := "ffi.o"
target importTarget (pkg : Package) : FilePath := do
let oFile := pkg.oleanDir / ffiO
let srcJob ← inputFile $ pkg.dir / ffiC
buildFileAfterDep oFile srcJob fun srcFile => do
let flags := #["-I", (← getLeanIncludeDir).toString, "-fPIC"]
compileO ffiC oFile srcFile flags
extern_lib ffi (pkg : Package) := do
let name := nameToStaticLib "ffi"
let job ← fetch <| pkg.target ``importTarget
buildStaticLib (pkg.buildDir / defaultLibDir / name) #[job]
extern_lib rust_ffi (pkg : Package) := do
proc { cmd := "cargo", args := #["build", "--release"], cwd := pkg.dir }
let name := nameToStaticLib "rust_ffi"
return (pure $ pkg.dir / "target" / "release" / name)
require std from git
"https://github.com/leanprover/std4/" @ "fde95b16907bf38ea3f310af406868fc6bcf48d1"
require LSpec from git
"https://github.com/yatima-inc/lspec/" @ "88f7d23e56a061d32c7173cea5befa4b2c248b41"
section ImportAll
open System
open Lean (RBTree)
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
def getAllFiles : ScriptM $ List String := do
let paths := (← getLeanFilePaths ⟨"YatimaStdLib"⟩).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 ⟨"YatimaStdLib.lean"⟩ (← getImportsString)
return 0
script import_all? do
let importsFromUser ← IO.FS.readFile ⟨"YatimaStdLib.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
lean_exe Tests.UInt
lean_exe Tests.ByteArray
lean_exe Tests.ByteVector
lean_exe Tests.LightData