From 3f082287cc346f82568adb9086b2068827f29e1b Mon Sep 17 00:00:00 2001 From: Siddhartha Gadgil Date: Mon, 18 May 2026 09:03:09 +0530 Subject: [PATCH 1/2] Created shell --- .github/workflows/lean_action_ci.yml | 14 ++++++++++++++ .gitignore | 1 + Main.lean | 4 ++++ ShellWall.lean | 3 +++ ShellWall/Basic.lean | 1 + lakefile.toml | 10 ++++++++++ lean-toolchain | 1 + 7 files changed, 34 insertions(+) create mode 100644 .github/workflows/lean_action_ci.yml create mode 100644 .gitignore create mode 100644 Main.lean create mode 100644 ShellWall.lean create mode 100644 ShellWall/Basic.lean create mode 100644 lakefile.toml create mode 100644 lean-toolchain diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml new file mode 100644 index 0000000..c48bd68 --- /dev/null +++ b/.github/workflows/lean_action_ci.yml @@ -0,0 +1,14 @@ +name: Lean Action CI + +on: + push: + pull_request: + workflow_dispatch: + +jobs: + build: + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v5 + - uses: leanprover/lean-action@v1 diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..bfb30ec --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +/.lake diff --git a/Main.lean b/Main.lean new file mode 100644 index 0000000..762f725 --- /dev/null +++ b/Main.lean @@ -0,0 +1,4 @@ +import ShellWall + +def main : IO Unit := + IO.println s!"Hello, {hello}!" diff --git a/ShellWall.lean b/ShellWall.lean new file mode 100644 index 0000000..873a184 --- /dev/null +++ b/ShellWall.lean @@ -0,0 +1,3 @@ +-- This module serves as the root of the `ShellWall` library. +-- Import modules here that should be built as part of the library. +import ShellWall.Basic diff --git a/ShellWall/Basic.lean b/ShellWall/Basic.lean new file mode 100644 index 0000000..99415d9 --- /dev/null +++ b/ShellWall/Basic.lean @@ -0,0 +1 @@ +def hello := "world" diff --git a/lakefile.toml b/lakefile.toml new file mode 100644 index 0000000..0aa1b32 --- /dev/null +++ b/lakefile.toml @@ -0,0 +1,10 @@ +name = "ShellWall" +version = "0.1.0" +defaultTargets = ["shellwall"] + +[[lean_lib]] +name = "ShellWall" + +[[lean_exe]] +name = "shellwall" +root = "Main" diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 0000000..33e0c08 --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.29.1 From 0e6a9fdd43a06a371ef9681e2d018d4925cdecd7 Mon Sep 17 00:00:00 2001 From: Siddhartha Gadgil Date: Mon, 18 May 2026 09:12:15 +0530 Subject: [PATCH 2/2] manifest created --- lake-manifest.json | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 lake-manifest.json diff --git a/lake-manifest.json b/lake-manifest.json new file mode 100644 index 0000000..998b24c --- /dev/null +++ b/lake-manifest.json @@ -0,0 +1,5 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "ShellWall", + "lakeDir": ".lake"}