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

import Lean
import Lake
open Lake DSL

package «CWayland» {
  moreLinkArgs := #["-L.lake/build/lib", "-lLibCWayland"]
  extraDepTargets := #[Lean.Name.mkStr1 "LibCWayland"]
}

target «LibCWayland.o» pkg : System.FilePath := do
  let objectFile := pkg.buildDir / "LibCWayland.o"
  let srcJob ← inputFile (text := .true) <| pkg.dir / "lib" / "CWayland" / "CWayland.c"
  -- let cFlags ← captureProc { cmd := "pkg-config", args := #["--cflags", "libwayland-client"] }
  -- let cFlags := cFlags.splitOn " "
  let cFlags := #[]
  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 «LibCWayland» pkg : System.FilePath := do
  let name := nameToStaticLib "LibCWayland"
  let objectFile ← fetch <| pkg.target (Lean.Name.mkStr1 "LibCWayland.o")
  buildStaticLib (pkg.buildDir / "lib" / name) #[objectFile]

lean_lib «Wayland» {
  srcDir := "lib"
  roots := #[`Wayland]
}

lean_exe «Waylean» {
  srcDir := "src"
  root := `Waylean
}