diff options
| -rw-r--r-- | flake.lock | 6 | ||||
| -rw-r--r-- | flake.nix | 7 | ||||
| -rw-r--r-- | lakefile.lean | 15 | ||||
| -rw-r--r-- | lib/CWayland/CWayland.c | 7 | ||||
| -rw-r--r-- | lib/CWayland/CWayland.h | 20 |
5 files changed, 44 insertions, 11 deletions
@@ -20,11 +20,11 @@ }, "nixpkgs": { "locked": { - "lastModified": 1770537093, - "narHash": "sha256-pF1quXG5wsgtyuPOHcLfYg/ft/QMr8NnX0i6tW2187s=", + "lastModified": 1772419343, + "narHash": "sha256-QU3Cd5DJH7dHyMnGEFfPcZDaCAsJQ6tUD+JuUsYqnKU=", "owner": "nixos", "repo": "nixpkgs", - "rev": "fef9403a3e4d31b0a23f0bacebbec52c248fbb51", + "rev": "93178f6a00c22fcdee1c6f5f9ab92f2072072ea9", "type": "github" }, "original": { @@ -10,10 +10,13 @@ }; outputs = { self, nixpkgs, flake-utils }: flake-utils.lib.eachDefaultSystem (system: let - pkgs = import nixpkgs { inherit system; }; + pkgs = import nixpkgs { + inherit system; + config.allowUnsupportedSystem = true; # for macOS + }; lean-shell = pkgs.mkShell { name = "Lean"; - packages = [ pkgs.lean4 ]; + packages = [ pkgs.lean4 pkgs.wayland pkgs.pkg-config ]; }; in { devShells = { diff --git a/lakefile.lean b/lakefile.lean index ef12dad..ecee22d 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -2,17 +2,24 @@ 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"] + 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 ← captureProc { cmd := "pkg-config", args := #["--cflags", "libwayland-client"] } - -- let cFlags := cFlags.splitOn " " - let cFlags := #[] + 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) diff --git a/lib/CWayland/CWayland.c b/lib/CWayland/CWayland.c index 2b9bf6d..10c1cc2 100644 --- a/lib/CWayland/CWayland.c +++ b/lib/CWayland/CWayland.c @@ -1,6 +1,9 @@ -#include <lean/lean.h> +#include "CWayland.h" +#include <wayland-client.h> lean_obj_res lean_test_answer() { - return lean_io_result_mk_ok(lean_int_to_int(42)); + struct wl_display* disp = wl_display_connect(NULL); + wl_fixed_t fixed = wl_fixed_from_double(42.0); + return lean_io_result_mk_ok(lean_int_to_int(wl_fixed_to_int(fixed))); }
\ No newline at end of file diff --git a/lib/CWayland/CWayland.h b/lib/CWayland/CWayland.h new file mode 100644 index 0000000..42bc5ee --- /dev/null +++ b/lib/CWayland/CWayland.h @@ -0,0 +1,20 @@ +#pragma once + +#include <lean/lean.h> + +// Display + +lean_obj_res waylean_display_new(void); + +// Event Loop + +lean_obj_res waylean_event_loop_new (void); +lean_obj_res waylean_event_loop_add_display(lean_obj_arg event_loop, + lean_obj_arg display); +lean_obj_res waylean_event_loop_add_timer (lean_obj_arg event_loop, + unsigned delay_ms, + lean_obj_arg message); +lean_obj_res waylean_event_loop_add_signal (lean_obj_arg event_loop, + int signum, + lean_obj_arg message); +lean_obj_res waylean_event_loop_poll (lean_obj_arg event_loop);
\ No newline at end of file |