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 }