build.yml

name: CI

on:
  push:
    branches:
      - "master"
  pull_request:
  workflow_dispatch:

permissions:
  contents: read
  pages: write
  id-token: write

concurrency:
  group: ${{ github.workflow }}-${{ github.ref }}
  cancel-in-progress: true

jobs:
  build:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - name: Install elan
        run: |
          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
          echo "$HOME/.elan/bin" >> $GITHUB_PATH
      - name: Check toolchain version
        run: |
          elan --version
          lake --version
          lean --version
      - name: Restore cache
        uses: actions/cache/restore@v4
        with:
          path: .lake
          key: lake-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
          restore-keys: lake-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
      - name: Fetch cache
        run: lake exe cache get
      - name: Build doc-gen4
        run: lake build doc-gen4
      - name: Generate documents
        run: |
          lake build \
            Foundation:docs \
            Arithmetization:docs \
            Incompleteness:docs \
            Summary:docs
      - name: Save cache
        uses: actions/cache/save@v4
        with:
          path: .lake
          key: lake-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
      - name: Upload documents
        uses: actions/upload-pages-artifact@v1
        with:
          path: .lake/build/doc
      - name: Deploy
        uses: actions/deploy-pages@v1