Merge pull request #34 from Peiyang-Song/main

Set up CI

.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

.gitignore

@@ -1,4 +1,3 @@
-/build
 /lake-packages/*
 /.lake