From 57fb134506c279715fd0b541c397510cd81af1da Mon Sep 17 00:00:00 2001
From: qwjyh <urataw421@gmail.com>
Date: Wed, 23 Oct 2024 16:03:06 +0900
Subject: [PATCH] init

---
 .github/workflows/lean_action_ci.yml | 14 ++++++++++++++
 .gitignore                           |  1 +
 FfiTest.lean                         |  3 +++
 FfiTest/Basic.lean                   |  1 +
 README.md                            |  1 +
 lakefile.lean                        |  9 +++++++++
 lean-toolchain                       |  1 +
 7 files changed, 30 insertions(+)
 create mode 100644 .github/workflows/lean_action_ci.yml
 create mode 100644 .gitignore
 create mode 100644 FfiTest.lean
 create mode 100644 FfiTest/Basic.lean
 create mode 100644 README.md
 create mode 100644 lakefile.lean
 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/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