blob: 271a2169e28bb42a7c5edcd367461279e1bf0e21 (
plain)
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
|
import Lean
import Lake
open Lake DSL
def evalPkgConfig (args : Array String) : IO (Array String) := do
let res ← IO.Process.output { cmd := "pkg-config", args := args }
if res.exitCode != 0 then
throw <| IO.userError s!"pkg-config failed: {res.stderr}"
return res.stdout.split Char.isWhitespace
|>.map (String.Slice.toString)
|>.filter (· != "")
|>.toArray
package «Waylean» where
moreLinkArgs := #["-L.lake/build/lib", "-lCWayland"] ++ (run_io evalPkgConfig #["--libs", "wayland-client"]).filter (· != "-lm")
extraDepTargets := #[`CWayland]
lean_lib «WaylandScannerLib» where
srcDir := "tools"
roots := #[`Scanner]
lean_exe «WaylandScanner» where
srcDir := "tools"
root := `Scanner
target «WaylandProtocolsSources» pkg : Unit := do
let scannerJob ← «WaylandScanner».fetch
let outPath := pkg.dir / "lib"
let srcPath := pkg.dir / "lib" / "Wayland" / "Protocols" / "xml"
let rootModule := "Wayland.Protocols"
scannerJob.bindM fun scannerFile ↦
Job.sync do
proc {
cmd := scannerFile.toString
args := #[rootModule, outPath.toString, srcPath.toString]
}
target «CWayland.o» pkg : System.FilePath := do
let objectFile := pkg.buildDir / "CWayland.o"
let srcJob ← inputFile (text := .true) <| pkg.dir / "lib" / "CWayland" / "CWayland.cc"
let cFlags ← evalPkgConfig #["--cflags", "wayland-client"]
buildFileAfterDep objectFile srcJob (fun srcFile ↦ do
let cFlags := cFlags ++ #["-I", (← getLeanIncludeDir).toString, "-I", (← IO.getEnv "C_INCLUDE_PATH").getD "", "-fPIC"]
compileO objectFile srcFile cFlags)
target «CWayland» pkg : System.FilePath := do
let objectFile ← «CWayland.o».fetch
let libFile := pkg.buildDir / "lib" / nameToStaticLib "CWayland"
buildStaticLib libFile #[objectFile]
lean_lib «Wayland» where
srcDir := "lib"
roots := #[`Wayland]
extraDepTargets := #[`WaylandProtocolsSources]
lean_exe «Waylean» where
srcDir := "src"
root := `Waylean
|
