initial commit

10 files changed, 139 insertions, 0 deletions

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..bfb30ec
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+/.lake
diff --git a/flake.lock b/flake.lock
new file mode 100644
index 0000000..1ea53c5
--- /dev/null
+++ b/flake.lock
@@ -0,0 +1,61 @@
+{
+  "nodes": {
+    "flake-utils": {
+      "inputs": {
+        "systems": "systems"
+      },
+      "locked": {
+        "lastModified": 1731533236,
+        "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1770537093,
+        "narHash": "sha256-pF1quXG5wsgtyuPOHcLfYg/ft/QMr8NnX0i6tW2187s=",
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "fef9403a3e4d31b0a23f0bacebbec52c248fbb51",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nixos",
+        "ref": "nixpkgs-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-utils": "flake-utils",
+        "nixpkgs": "nixpkgs"
+      }
+    },
+    "systems": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}
diff --git a/flake.nix b/flake.nix
new file mode 100644
index 0000000..180b480
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,24 @@
+{
+  description = "Lean Wayland API for Lean";
+  inputs = {
+    nixpkgs = {
+      url = "github:nixos/nixpkgs/nixpkgs-unstable";
+    };
+    flake-utils = {
+      url = "github:numtide/flake-utils";
+    };
+  };
+  outputs = { self, nixpkgs, flake-utils }: flake-utils.lib.eachDefaultSystem (system:
+    let
+      pkgs = import nixpkgs { inherit system; };
+      lean-shell = pkgs.mkShell {
+        name = "Lean";
+        packages = [ pkgs.lean4 ];
+      };
+    in {
+    devShells = {
+      default = lean-shell;
+      lean = lean-shell;
+    };
+  });
+}
diff --git a/lake-manifest.json b/lake-manifest.json
new file mode 100644
index 0000000..f1c2a09
--- /dev/null
+++ b/lake-manifest.json
@@ -0,0 +1,5 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "Waylean",
+ "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
new file mode 100644
index 0000000..ef12dad
--- /dev/null
+++ b/lakefile.lean
@@ -0,0 +1,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
+}
diff --git a/lean-toolchain b/lean-toolchain
new file mode 100644
index 0000000..5249182
--- /dev/null
+++ b/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.27.0
diff --git a/lib/CWayland/CWayland.c b/lib/CWayland/CWayland.c
new file mode 100644
index 0000000..2b9bf6d
--- /dev/null
+++ b/lib/CWayland/CWayland.c
@@ -0,0 +1,6 @@
+#include <lean/lean.h>
+
+lean_obj_res lean_test_answer()
+{
+    return lean_io_result_mk_ok(lean_int_to_int(42));
+}
\ No newline at end of file
diff --git a/lib/Wayland.lean b/lib/Wayland.lean
new file mode 100644
index 0000000..16f5c4c
--- /dev/null
+++ b/lib/Wayland.lean
@@ -0,0 +1 @@
+import Wayland.Native
diff --git a/lib/Wayland/Native.lean b/lib/Wayland/Native.lean
new file mode 100644
index 0000000..ded2e3a
--- /dev/null
+++ b/lib/Wayland/Native.lean
@@ -0,0 +1,2 @@
+@[extern "lean_test_answer"]
+opaque testAnswer : IO Int
diff --git a/src/Waylean.lean b/src/Waylean.lean
new file mode 100644
index 0000000..5445f25
--- /dev/null
+++ b/src/Waylean.lean
@@ -0,0 +1,5 @@
+import Wayland
+
+def main : IO Unit := do
+  let answer ← testAnswer
+  IO.println s!"Hello, world! The answer is {answer}."