docs.yaml

name: build and deploy mathlib4 docs

on:
  workflow_dispatch:
  schedule:
    - cron: '0 */8 * * *' # every 8 hours

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

jobs:
  build:
    name: build and deploy mathlib4 docs
    runs-on: doc-gen
    steps:
      - name: clean up
        run: |
          rm -rf mathlib4
          rm -rf workaround
          rm -rf $HOME/.elan
          rm -rf $HOME/.cache/mathlib

      - name: Checkout repo
        uses: actions/checkout@v3
        with:
          repository: leanprover-community/mathlib4
          path: mathlib4

      - name: install elan
        run: |
          set -o pipefail
          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
          echo "$HOME/.elan/bin" >> $GITHUB_PATH

      - name: get cache
        working-directory: mathlib4
        run: lake exe cache get

      - name: build mathlib
        working-directory: mathlib4
        run: env LEAN_ABORT_ON_PANIC=1 lake build

      - name: create dummy docs project
        run: |
          # Workaround for the lake issue
          elan default leanprover/lean4:nightly
          lake new workaround
          cd workaround
          cp -f ../mathlib4/lean-toolchain .
          echo 'require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"' >> lakefile.lean
          echo 'require «mathlib» from ".." / "mathlib4"' >> lakefile.lean

          # doc-gen4 expects to work on github repos with at least one commit
          git add .
          git commit -m "workaround"
          git remote add origin "https://github.com/leanprover/workaround"

          mkdir lake-packages
          cp -r ../mathlib4/lake-packages/* lake-packages/
          lake update

      - name: build doc-gen4
        working-directory: workaround
        run: |
          lake build doc-gen4

      - name: generate docs
        working-directory: workaround
        run: |
          lake build Std:docs Qq:docs Aesop:docs ProofWidgets:docs Mathlib:docs Archive:docs Counterexamples:docs docs:docs

      - name: copy extra files
        run: |
          cp mathlib4/docs/{100.yaml,overview.yaml,undergrad.yaml} workaround/build/doc

      - name: Upload artifact
        uses: actions/upload-pages-artifact@v1
        with:
          path: 'workaround/build/doc'

      - name: Deploy to GitHub Pages
        id: deployment
        uses: actions/deploy-pages@v1

      - name: clean up
        if: always()
        run: |
          rm -rf mathlib4
          rm -rf workaround
          rm -rf $HOME/.elan
          rm -rf $HOME/.cache/mathlib