Merge pull request #114 from lean-dojo/peiyang #89

	name: CI

	on:
	pull_request:
	branches:
	- main

	push:
	branches:
	- main

	jobs:
	build:
	runs-on: ubuntu-latest
	name: Build
	steps:
	- name: Checkout project
	uses: actions/checkout@v4
	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 -v -U
	- name: Download model
	run: \|
	export GIT_CLONE_PROTECTION_ACTIVE=false
	~/.elan/bin/lake exe LeanCopilot/download
	- name: Build tests
	run: ~/.elan/bin/lake build LeanCopilotTests -v -U
	test_external:
	needs: build
	runs-on: ubuntu-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
	export GIT_CLONE_PROTECTION_ACTIVE=false
	~/.elan/bin/lake exe LeanCopilot/download
	~/.elan/bin/lake build -v -U

Provide feedback