From 0a6d8bd4c1eae9c04dbc5b7379d811dfdc80ab19 Mon Sep 17 00:00:00 2001
From: SnO2WMaN <me@sno2wman.net>
Date: Tue, 21 Nov 2023 13:57:04 +0900
Subject: [PATCH 1/2] ci: Add workflow to check build successful

---
 .editorconfig            | 13 +++++++++++++
 .github/workflows/ci.yml | 41 ++++++++++++++++++++++++++++++++++++++++
 2 files changed, 54 insertions(+)
 create mode 100644 .editorconfig
 create mode 100644 .github/workflows/ci.yml

diff --git a/.editorconfig b/.editorconfig
new file mode 100644
index 00000000..f96bc4cc
--- /dev/null
+++ b/.editorconfig
@@ -0,0 +1,13 @@
+root = true
+
+[*]
+indent_style = tab
+indent_size = 2
+end_of_line = lf
+charset = utf-8
+trim_trailing_whitespace = true
+insert_final_newline = true
+
+[*.{yml,yaml}]
+indent_style = space
+indent_size = 2
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
new file mode 100644
index 00000000..c01f8ffc
--- /dev/null
+++ b/.github/workflows/ci.yml
@@ -0,0 +1,41 @@
+name: CI
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+
+# concurrency:
+#   group: ${{ github.workflow }}-${{ github.ref }}
+#   cancel-in-progress: true
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v3
+      - name: Install elan
+        run: |
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+      - name: Cache dependencies
+        uses: actions/cache@v3
+        with:
+          path: |
+            ./lake-packages
+          key: deps-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
+          restore-keys: |
+            deps-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}
+      - name: Cache build
+        uses: actions/cache@v3
+        with:
+          path: |
+            ./build
+          key: build-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ github.sha }}
+          restore-keys: |
+            build-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}
+      - name: Build
+        run: |
+          lake exe cache get
+          lake build

From 47881294ad925c017e440f2c4108789365029867 Mon Sep 17 00:00:00 2001
From: SnO2WMaN <me@sno2wman.net>
Date: Tue, 21 Nov 2023 13:57:17 +0900
Subject: [PATCH 2/2] fix

---
 Logic.lean                             | 1 -
 Logic/Propositional/Basic/Formula.lean | 4 ++--
 2 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/Logic.lean b/Logic.lean
index b42b369f..1a04d1b8 100644
--- a/Logic.lean
+++ b/Logic.lean
@@ -3,7 +3,6 @@ import Logic.Vorspiel.Order
 import Logic.Vorspiel.Meta
 
 import Logic.Logic.LogicSymbol
-import Logic.Logic.Logic
 
 -- Propositional
 
diff --git a/Logic/Propositional/Basic/Formula.lean b/Logic/Propositional/Basic/Formula.lean
index 76bea083..6a26026c 100644
--- a/Logic/Propositional/Basic/Formula.lean
+++ b/Logic/Propositional/Basic/Formula.lean
@@ -1,4 +1,4 @@
-import Logic.Logic.Logic
+import Logic.Logic.LogicSymbol
 
 namespace LO
 
@@ -40,4 +40,4 @@ end Formula
 
 end Propositional
 
-end LO
\ No newline at end of file
+end LO