Merge branch 'main' of https://github.com/lean-dojo/LeanCopilot into … #84

	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: Install Git LFS
	run: \|
	git lfs update --force
	git lfs install
	- 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 exe LeanCopilot/download
	- name: Build tests
	run: ~/.elan/bin/lake build LeanCopilotTests
	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 LeanCopilot-demo
	- name: Install Git LFS
	run: \|
	cd lean4-example
	git lfs update --force
	git lfs install
	- name: Build lean4-example
	run: \|
	cd lean4-example
	~/.elan/bin/lake exe LeanCopilot/download
	~/.elan/bin/lake build

Provide feedback