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 «CWayland» { moreLinkArgs := #["-L.lake/build/lib", "-lLibCWayland"] ++ (run_io evalPkgConfig #["--libs", "wayland-client"]).filter (· != "-lm") 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 ← 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 «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 }