diff options
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | flake.lock | 61 | ||||
| -rw-r--r-- | flake.nix | 24 | ||||
| -rw-r--r-- | lake-manifest.json | 5 | ||||
| -rw-r--r-- | lakefile.lean | 33 | ||||
| -rw-r--r-- | lean-toolchain | 1 | ||||
| -rw-r--r-- | lib/CWayland/CWayland.c | 6 | ||||
| -rw-r--r-- | lib/Wayland.lean | 1 | ||||
| -rw-r--r-- | lib/Wayland/Native.lean | 2 | ||||
| -rw-r--r-- | src/Waylean.lean | 5 |
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}." |