push_pr.yml

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
      - 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: 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
          ~/.elan/bin/lake exe LeanCopilot/download
          ~/.elan/bin/lake build