From 97aa8685f9b19543079281c2f1e4259709c60c00 Mon Sep 17 00:00:00 2001 From: Greg Shuflin Date: Mon, 1 Dec 2025 00:37:22 -0800 Subject: [PATCH] Initial commit --- .gitignore | 1 + LeanGraphics.lean | 3 +++ LeanGraphics/Basic.lean | 1 + Main.lean | 4 ++++ README.md | 9 +++++++++ justfile | 7 +++++++ lake-manifest.json | 5 +++++ lakefile.toml | 10 ++++++++++ lean-toolchain | 1 + 9 files changed, 41 insertions(+) create mode 100644 .gitignore create mode 100644 LeanGraphics.lean create mode 100644 LeanGraphics/Basic.lean create mode 100644 Main.lean create mode 100644 README.md create mode 100644 justfile create mode 100644 lake-manifest.json create mode 100644 lakefile.toml create mode 100644 lean-toolchain diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..bfb30ec --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +/.lake diff --git a/LeanGraphics.lean b/LeanGraphics.lean new file mode 100644 index 0000000..cc783dd --- /dev/null +++ b/LeanGraphics.lean @@ -0,0 +1,3 @@ +-- This module serves as the root of the `LeanGraphics` library. +-- Import modules here that should be built as part of the library. +import LeanGraphics.Basic diff --git a/LeanGraphics/Basic.lean b/LeanGraphics/Basic.lean new file mode 100644 index 0000000..849272b --- /dev/null +++ b/LeanGraphics/Basic.lean @@ -0,0 +1 @@ +def startupMsg := "Lean4 graphics test" diff --git a/Main.lean b/Main.lean new file mode 100644 index 0000000..c7c3354 --- /dev/null +++ b/Main.lean @@ -0,0 +1,4 @@ +import LeanGraphics + +def main : IO Unit := + IO.println s!"{startupMsg}" diff --git a/README.md b/README.md new file mode 100644 index 0000000..b5866f7 --- /dev/null +++ b/README.md @@ -0,0 +1,9 @@ +# lean-graphics + + +This is an experiment in writing GUI programs using Lean4. + +## Prior art + +- Lean4 SDL3 bindings: https://github.com/ValorZard/lean-sdl3 and https://github.com/ValorZard/lean-sdl-test +- Doom-like game: https://github.com/oOo0oOo/LeanDoomed diff --git a/justfile b/justfile new file mode 100644 index 0000000..8623b63 --- /dev/null +++ b/justfile @@ -0,0 +1,7 @@ +_default: + @just --list + + +# Run main binary +run: + lake exec lean-graphics diff --git a/lake-manifest.json b/lake-manifest.json new file mode 100644 index 0000000..fb849f6 --- /dev/null +++ b/lake-manifest.json @@ -0,0 +1,5 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "«lean-graphics»", + "lakeDir": ".lake"} diff --git a/lakefile.toml b/lakefile.toml new file mode 100644 index 0000000..524230c --- /dev/null +++ b/lakefile.toml @@ -0,0 +1,10 @@ +name = "lean-graphics" +version = "0.1.0" +defaultTargets = ["lean-graphics"] + +[[lean_lib]] +name = "LeanGraphics" + +[[lean_exe]] +name = "lean-graphics" +root = "Main" diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 0000000..370b26d --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.25.2