ci.yml

name: CI

on:
  push:
    branches:
      - master
  pull_request:
    branches:
      - master

concurrency:
  group: ${{ github.workflow }}-${{ github.ref }}
  cancel-in-progress: ${{ github.ref != 'refs/heads/master' }}

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

jobs:
  build:
    name: Build project
    runs-on: ubuntu-latest
    needs: mk-all-check
    steps:
      - uses: actions/checkout@v7
      - name: Setup 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: Print lake and lean version
        run: |
          lake --version
          lean --version

      # Restore project cache
      - name: Get Mathlib cache
        run: lake exe cache get
      - name: Restore cache
        id: cache-restore
        uses: actions/cache/restore@v5
        with:
          path: .lake/Foundation-x86_64-unknown-linux-gnu.tar.gz
          # NOTE: including github branch name and SHA for avoding cache key reserving problem
          key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.ref_name }}-${{ github.sha }}
          restore-keys: |
            lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.ref_name }}
            lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
      - name: Unpack project cache
        if: hashFiles('.lake/Foundation-x86_64-unknown-linux-gnu.tar.gz') != ''
        run: lake unpack

      - name: Build Foundation
        run: lake build Foundation

      - name: Build docs
        run: lake build Foundation:docs

      - name: Pack project cache
        run: lake pack
      - name: Save project cache
        if: github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository
        id: cache-save
        uses: actions/cache/save@v5
        with:
          path: .lake/Foundation-x86_64-unknown-linux-gnu.tar.gz
          key: ${{ steps.cache-restore.outputs.cache-primary-key }}

      - uses: ts-graphviz/setup-graphviz@v2
      - name: Generate import graph
        run: |
          lake exe graph ./import_graph.png
          lake exe graph ./import_graph.pdf
          lake exe graph ./import_graph.html

      - name: Upload lean artifacts
        uses: actions/upload-artifact@v7
        with:
          name: lean-artifacts
          path: |
            .lake/build/doc
            import_graph.png
            import_graph.pdf
            import_graph.html
          retention-days: 1
          include-hidden-files: true

  check-references:
    name: Check references.bib format
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v7
      - name: Install bibtool
        run: |
          sudo apt-get update
          sudo apt-get install -y bibtool
      - name: Format references.bib
        run: |
          bibtool -r .bibtoolrsc -i references.bib -o references.bib.formatted
      - name: Check if formatted correctly
        run: |
          diff -u references.bib references.bib.formatted || (echo "references.bib is not formatted" && exit 1)

  mk-all-check:
    name: Check mk_all executed
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v7
      - name: Setup elan
        run: |
          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
      - name: Check mk_all executed
        run: |
          lake exe mk_all --module
          if [ -n "$(git diff)" ]; then
            echo "Files were modified by mk_all. Please run 'lake exe mk_all --module' and commit the changes."
            exit 1
          fi

  deploy:
    name: Generate page
    runs-on: ubuntu-latest
    if: github.ref == 'refs/heads/master'
    needs:
      - build
      - check-references
    environment:
      name: github-pages
      url: ${{ steps.deployment.outputs.page_url }}
    steps:
      - uses: actions/checkout@v7
      - uses: pandoc/actions/setup@v1

      - name: Download lean artifacts
        uses: actions/download-artifact@v8
        with:
          name: lean-artifacts
      - name: Copy from artifacts to pages
        run: |
          cp -r "$GITHUB_WORKSPACE/.lake/build/doc" pages/docs
          cp "$GITHUB_WORKSPACE/import_graph.png" \
             "$GITHUB_WORKSPACE/import_graph.pdf" \
             "$GITHUB_WORKSPACE/import_graph.html" \
             pages/

      - name: Compile README.md to index.html
        run: |
          pandoc \
           README.md \
           --from markdown \
           --to html5 \
           --standalone \
           --katex \
           --metadata title="FormalizedFormalLogic/Foundation" \
           --output pages/index.html

      - uses: actions/upload-pages-artifact@v5
        with:
          path: pages
      - uses: actions/deploy-pages@v5
        id: deployment