From f25a2dda4e949fc02cc783b9e7056cd2193ba006 Mon Sep 17 00:00:00 2001 From: Leopold Fajtak Date: Mon, 22 Sep 2025 09:56:03 +0200 Subject: [PATCH] Set up project --- .github/workflows/lean_action_ci.yml | 14 ++++++++++++++ .gitignore | 1 + InductiveVerification.lean | 3 +++ InductiveVerification/Basic.lean | 1 + Main.lean | 4 ++++ README.md | 1 + lakefile.toml | 10 ++++++++++ lean-toolchain | 1 + 8 files changed, 35 insertions(+) create mode 100644 .github/workflows/lean_action_ci.yml create mode 100644 .gitignore create mode 100644 InductiveVerification.lean create mode 100644 InductiveVerification/Basic.lean create mode 100644 Main.lean create mode 100644 README.md 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..09cd4ca --- /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@v4 + - 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/InductiveVerification.lean b/InductiveVerification.lean new file mode 100644 index 0000000..d9843f5 --- /dev/null +++ b/InductiveVerification.lean @@ -0,0 +1,3 @@ +-- This module serves as the root of the `InductiveVerification` library. +-- Import modules here that should be built as part of the library. +import InductiveVerification.Basic diff --git a/InductiveVerification/Basic.lean b/InductiveVerification/Basic.lean new file mode 100644 index 0000000..99415d9 --- /dev/null +++ b/InductiveVerification/Basic.lean @@ -0,0 +1 @@ +def hello := "world" diff --git a/Main.lean b/Main.lean new file mode 100644 index 0000000..9da78ea --- /dev/null +++ b/Main.lean @@ -0,0 +1,4 @@ +import InductiveVerification + +def main : IO Unit := + IO.println s!"Hello, {hello}!" diff --git a/README.md b/README.md new file mode 100644 index 0000000..a1136e3 --- /dev/null +++ b/README.md @@ -0,0 +1 @@ +# inductive-verification \ No newline at end of file diff --git a/lakefile.toml b/lakefile.toml new file mode 100644 index 0000000..a836890 --- /dev/null +++ b/lakefile.toml @@ -0,0 +1,10 @@ +name = "inductive-verification" +version = "0.1.0" +defaultTargets = ["inductive-verification"] + +[[lean_lib]] +name = "InductiveVerification" + +[[lean_exe]] +name = "inductive-verification" +root = "Main" diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 0000000..7f254a9 --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.23.0