diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
new file mode 100644
index 0000000..a7e52a2
--- /dev/null
+++ b/.github/workflows/push.yml
@@ -0,0 +1,47 @@
+name: CI
+
+on:
+  push:
+    branches:
+      - main
+
+jobs:
+  build:
+    runs-on: ${{ matrix.os }}
+    strategy:
+      matrix:
+        os: [ubuntu-latest, macos-latest]
+    name: Build
+    steps:
+      - name: Checkout project
+        uses: actions/checkout@v2
+        with:
+          fetch-depth: 0
+      - name: Set up elan
+        run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
+      - name: Build project
+        run: ~/.elan/bin/lake build
+      - name: Download model
+        run: ~/.elan/bin/lake script run LeanInfer/download
+      - name: Build tests
+        run: ~/.elan/bin/lake build LeanInferTests
+  test_external:
+    needs: build
+    runs-on: ${{ matrix.os }}
+    strategy:
+      matrix:
+        os: [ubuntu-latest, macos-latest]
+    name: Test external
+    steps:
+      - name: Set up elan
+        run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
+      - name: Get lean4-example
+        run: |
+          git clone https://github.com/yangky11/lean4-example
+          cd lean4-example
+          git checkout LeanInfer-demo
+      - name: Build lean4-example
+        run: |
+          cd lean4-example
+          ~/.elan/bin/lake script run LeanInfer/download
+          ~/.elan/bin/lake build
\ No newline at end of file
diff --git a/.gitignore b/.gitignore
index 9366b53..22dc57e 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,4 +1,3 @@
-/build
 /lake-packages/*
 /.lake