docs.yaml

name: build and deploy mathlib4 docs

on:
  push:
    branches:
      - main
  pull_request:
  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_docs
          rm -rf mathlib4
          rm -rf workaround
          rm -rf $HOME/.elan
          rm -rf $HOME/.cache/mathlib

      - name: Checkout repo
        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
        with:
          repository: leanprover-community/mathlib4_docs
          path: mathlib4_docs


      - name: Checkout mathlib
        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
        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: set default toolchain
        working-directory: mathlib4
        run: |
          elan default $(cat lean-toolchain)

      - 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: |
          lake new workaround lib
          cd workaround
          cp -f ../mathlib4/lean-toolchain .
          cp -f ../mathlib4_docs/lakefile.toml .

          # doc-gen4 expects to work on github repos with at least one commit
          git config user.email "mathlib4_docs@leanprover-community.github.io"
          git config user.name "mathlib4_docs CI"
          git add .
          git commit -m "workaround"
          git remote add origin "https://github.com/leanprover-community/workaround"

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

          # Copy references.bib over while doc-gen lacks support for subproject references.bib
          mkdir docs/
          cp ../mathlib4/docs/references.bib docs/references.bib

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

      - name: build import graph
        working-directory: mathlib4
        run: |
          lake exe graph mathlib.html

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

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

      - name: copy import graph
        run: |
          cp mathlib4/mathlib.html workaround/.lake/build/doc

      - name: Upload artifact
        uses: actions/upload-pages-artifact@fc324d3547104276b827a68afc52ff2a11cc49c9 # v5.0.0
        with:
          path: 'workaround/.lake/build/doc'

      - name: Deploy to GitHub Pages
        if: github.ref == 'refs/heads/main'
        id: deployment
        uses: actions/deploy-pages@cd2ce8fcbc39b97be8ca5fce6e763baed58fa128 # v5.0.0

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

  notify_if_failed:
    runs-on: ubuntu-latest
    needs: build
    if: always() && github.event_name != 'pull_request'
    steps:
      - name: Checkout repository
        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3

      - name: Get job status and URLs
        id: get-status
        env:
          GH_TOKEN: ${{ github.token }}
        run: |
          JOB_NAME="build and deploy mathlib4 docs"

          # Get URL and conclusion for the specific job
          JOB_DATA=$(gh run view ${{ github.run_id }} --json jobs --jq \
            ".jobs[] | select(.name == \"$JOB_NAME\")")

          JOB_URL=$(echo "$JOB_DATA" | jq -r '.url')

          JOB_CONCLUSION=$(echo "$JOB_DATA" | jq -r '.conclusion')

          echo "job_url=${JOB_URL}" | tee -a "$GITHUB_OUTPUT"
          echo "job_conclusion=${JOB_CONCLUSION}" | tee -a "$GITHUB_OUTPUT"

      - name: Post failure / cancelled message for mathlib_test_executable on Zulip
        if: steps.get-status.outputs.job_conclusion != 'success'
        uses: zulip/github-actions-zulip/send-message@bd8ec52de371d139ae8313661b7d8318c19266aa # v2.0.1
        with:
          api-key: ${{ secrets.ZULIP_API_KEY }}
          email: 'leanprover-community-monitor-runners-bot@leanprover.zulipchat.com'
          organization-url: 'https://leanprover.zulipchat.com'
          to: 'nightly-testing-mathlib'
          type: 'stream'
          topic: 'mathlib4_docs failure'
          content: |
            ❌ mathlib4_docs [${{ steps.get-status.outputs.job_conclusion }}](${{ steps.get-status.outputs.job_url }}) on ${{ github.sha }}

  workflow-keepalive:
    if: github.event_name == 'schedule'
    runs-on: ubuntu-latest
    permissions:
      actions: write
    steps:
      - uses: liskin/gh-workflow-keepalive@f72ff1a1336129f29bf0166c0fd0ca6cf1bcb38c # v1.2.1