doc.yml

name: docs
on:
  push:

# 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 documentation.
    # Exclude expensive self-hosted runner. Reserved for performance benchmarking.
    # https://docs.github.com/en/enterprise-cloud@latest/actions/writing-workflows/choosing-where-your-workflow-runs/choosing-the-runner-for-a-job#choosing-github-hosted-runners
    runs-on: ubuntu-latest
    steps:
      - name: Checkout 🛎️
        uses: actions/checkout@v4

      - 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
          ~/.elan/bin/lean --version
          echo "$HOME/.elan/bin" >> $GITHUB_PATH

      - name: Generate docs 📜
        run: |
          bash ./docgen.sh

# stolen from mathlib: https://github.com/leanprover-community/mathlib4_docs/blob/1f4ea7657bc377b4298fd400e567471d3a248b2d/.github/workflows/docs.yaml#L79-L86
      - name: Upload artifact 📁
        uses: actions/upload-pages-artifact@v3
        with:
          path: '.lake/build/doc'

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