build-and-docs.yml

# Copyright 2025 The Formal Conjectures Authors.

# Licensed under the Apache License, Version 2.0 (the "License");
# you may not use this file except in compliance with the License.
# You may obtain a copy of the License at

#     https://www.apache.org/licenses/LICENSE-2.0

# Unless required by applicable law or agreed to in writing, software
# distributed under the License is distributed on an "AS IS" BASIS,
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
# See the License for the specific language governing permissions and
# limitations under the License.

name: Build Lean project and deploy docs

on:
  push:
    branches:
      - main
  pull_request:

# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
permissions:
  contents: read
  pages: write
  id-token: write

jobs:
  build:
    runs-on: ubuntu-latest
    name: Build project
    steps:

      - name: Checkout project
        uses: actions/checkout@v6
        with:
          fetch-depth: 0

      - name: Install elan
        run: |
          set -o pipefail
          curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
          ./elan-init -y --default-toolchain none
          echo "$HOME/.elan/bin" >> $GITHUB_PATH

      - name: Generate All.lean
        run: |
          lake exe mk_all --lib FormalConjectures || true
          # Avoid including Test files from `Util/` to avoid inflating the
          # stats. This stop-gap should be removed after doing the TODO at
          # `fetchStatsMarkdown` in `docbuild/overwrite-index.lean`.
          grep -v "FormalConjectures\.Util\." FormalConjectures.lean > FormalConjectures/All.lean

      - name: Restore ~/.cache/mathlib
        uses: actions/cache/restore@v3
        with:
          path: ~/.cache/mathlib
          key: oleans-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('**/*.lean') }}
          restore-keys: |
            oleans-${{ hashFiles('lake-manifest.json') }}-
            oleans-

      - name: Get olean cache
        run: |
          lake exe cache unpack
          lake exe cache get

      - name: Build project
        run: |
          lake build

      - name: Pack olean cache
        run: |
          lake exe cache pack
          ls ~/.cache/mathlib

      - name: Save ~/.cache/mathlib
        uses: actions/cache/save@v3
        with:
          path: ~/.cache
          key: oleans-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('**/*.lean') }}

      - name: Prepare documentation
        run: |
          cd docbuild
          export MATHLIB_NO_CACHE_ON_UPDATE=1  # avoids "Failed to prune ProofWidgets cloud release: no such file or directory"
          lake update formal_conjectures

      - name: Cache documentation
        uses: actions/cache@v5
        with:
          path: docbuild/.lake/build/doc
          key: MathlibDoc-${{ hashFiles('docbuild/lake-manifest.json') }}-${{ hashFiles('**/*.lean') }}
          restore-keys: |
            MathlibDoc-${{ hashFiles('docbuild/lake-manifest.json') }}-
            MathlibDoc-

      - name: Build documentation
        run: |
          cd docbuild
          lake build FormalConjectures:docs

      - name: Extract documentation
        run: |
          cd docbuild
          mkdir out
          lake query FormalConjectures:docs > out-files.txt
          sed -i 's|^.*\.lake/build/doc/||' out-files.txt
          echo "::group::Generated files"
          cat out-files.txt
          echo "::endgroup::"
          rsync -a --files-from=out-files.txt --relative .lake/build/doc ./out

      - name: Set up Python
        uses: actions/setup-python@v6
        with:
          python-version: '3.12.9'

      - name: Install Python dependencies
        run: |
          python -m pip install --upgrade pip
          pip install pandas==2.2.3 numpy==2.2.3 plotly==5.20.0

      - name: Run plotting script
        run: |
          python docbuild/scripts/plot_growth.py

      - name: Inject stats into index.html
        shell: bash
        run: |
          cd docbuild
          lake exe overwrite_index ./out/index.html ./out/file_counts.html | tee -a "$GITHUB_STEP_SUMMARY"

      - name: Upload docs
        id: deployment
        uses: actions/upload-pages-artifact@v4
        with:
          path: docbuild/out

  # Deployment job
  deploy:
    if: github.ref == 'refs/heads/main'
    environment:
      name: github-pages
      url: ${{ steps.deployment.outputs.page_url }}
    runs-on: ubuntu-latest
    needs: build
    steps:
      - name: Deploy to GitHub Pages
        id: deployment
        uses: actions/deploy-pages@v4