commit 57fb134506c279715fd0b541c397510cd81af1da Author: qwjyh Date: Wed Oct 23 16:03:06 2024 +0900 init 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/FfiTest.lean b/FfiTest.lean new file mode 100644 index 0000000..48a64fc --- /dev/null +++ b/FfiTest.lean @@ -0,0 +1,3 @@ +-- This module serves as the root of the `FfiTest` library. +-- Import modules here that should be built as part of the library. +import FfiTest.Basic \ No newline at end of file diff --git a/FfiTest/Basic.lean b/FfiTest/Basic.lean new file mode 100644 index 0000000..e99d3a6 --- /dev/null +++ b/FfiTest/Basic.lean @@ -0,0 +1 @@ +def hello := "world" \ No newline at end of file diff --git a/README.md b/README.md new file mode 100644 index 0000000..c1cd2df --- /dev/null +++ b/README.md @@ -0,0 +1 @@ +# ffi_test \ No newline at end of file diff --git a/lakefile.lean b/lakefile.lean new file mode 100644 index 0000000..6b29568 --- /dev/null +++ b/lakefile.lean @@ -0,0 +1,9 @@ +import Lake +open Lake DSL + +package "ffi_test" where + version := v!"0.1.0" + +@[default_target] +lean_lib «FfiTest» where + -- add library configuration options here diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 0000000..2bf5ad0 --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +stable