push.yml

on:
  push:
    branches:
      - main

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

jobs:
  build_blueprint:
    runs-on: ubuntu-latest
    name: Build blueprint
    steps:
      - name: Checkout project
        uses: actions/checkout@v4
        with:
          fetch-depth: 0

      - name: Install Python
        uses: actions/setup-python@v5
        with:
          python-version: '3.9'
          cache: 'pip' # cache pip dependencies

      - name: Update pip
        run: |
          pip install --upgrade pip

      - name: Install blueprint apt dependencies
        run: |
          sudo apt-get update
          sudo apt-get install -y graphviz libgraphviz-dev pdf2svg dvisvgm

      - name: Install blueprint dependencies
        run: |
          cd blueprint && pip install -r requirements.txt

      - name: Build blueprint and copy to `docs/blueprint`
        run: |
          make blueprint
          mkdir -p docs
          mv blueprint/web docs/

      - name: Clear previously saved cache
        uses: DareFox/delete-cache-by-key@v1.0.1
        with:
          key: Blueprint-cache
          mode: exact
        continue-on-error: true

      - name: Save blueprint for future use
        uses: actions/cache/save@v4
        with:
          path: |
            docs/web
          key: Blueprint-cache


      - name: Restore previous documentation, while we wait for the next one to be generated
        uses: actions/cache/restore@v4
        with:
          path: |
            docs/docs
          key: Documentation-cache
        continue-on-error: true


      - name: Setup Pages
        uses: actions/configure-pages@v5

      - name: Upload blueprint artifact
        uses: actions/upload-pages-artifact@v3
        with:
          path: docs

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


  # generate doc after blueprint (as it's quite a bit longer)
  build_docs:
    runs-on: ubuntu-latest
    name: Build docs
    steps:
      - name: Checkout project
        uses: actions/checkout@v4
        with:
          fetch-depth: 0

      - name: Install elan
        run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain $(cat lean-toolchain)

      - name: Build project
        run: make LAKEBIN='~/.elan/bin/lake' build

      - name: Cache mathlib docs
        uses: actions/cache@v3
        with:
          path: |
            .lake/build/doc/Init
            .lake/build/doc/Lake
            .lake/build/doc/Lean
            .lake/build/doc/Std
            .lake/build/doc/Mathlib
            .lake/build/doc/declarations
            !.lake/build/doc/declarations/declaration-data-PrimeNumberTheoremAnd*
          key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
          restore-keys: |
            MathlibDoc-

      - name: Build documentation
        run: make LAKEBIN='~/.elan/bin/lake' doc

      - name: Copy documentation to `docs/docs`
        run: |
          mkdir -p docs
          cp -r .lake/build/doc docs/docs

      - name: Clear previously saved cache
        uses: DareFox/delete-cache-by-key@v1.0.1
        with:
          key: Documentation-cache
          mode: exact
        continue-on-error: true

      - name: Save documentation for future use
        uses: actions/cache/save@v4
        with:
          path: |
            docs/docs
          key: Documentation-cache

      #- name: Download blueprint artifacts
      #  uses: actions/download-artifact@v3
      #  with:
      #    path: blueprint_artifacts
      #    
      #- name: Extract blueprint artifacts
      #  run: tar xvf blueprint_artifacts/github-pages/artifact.tar -C docs/

      - name: Restore previously generated blueprint
        uses: actions/cache/restore@v4
        with:
          path: |
            docs/web
          key: Blueprint-cache
        continue-on-error: true

      ## cannot use upload-pages-artifact@v3 twice (it is used for the blueprint above)
      ## it fails because two identically named artifacts are uploaded
      ## (for github pages deployment to work, the artifact must be named 'github-pages')
      ## This could be fixed using upload-artifact's 'overwrite:true' option, but it is not implemented on upload-pages-artifact
      ## Copied the archive/upload action from upload-pages-artifact below.
      ## This should be replaced with
      ##   - name: Upload docs & blueprint artifact
      ##     uses: actions/upload-pages-artifact@v3
      ##     with:
      ##       path: docs
      ##       name: github-pages
      ##       overwrite: true
      ## when this is supported
      - name: Archive artifact
        shell: sh
        run: |
          echo ::group::Archive artifact
          tar \
            --dereference --hard-dereference \
            --directory "$INPUT_PATH" \
            -cvf "$RUNNER_TEMP/artifact.tar" \
            --exclude=.git \
            --exclude=.github \
            --exclude=".[^/]*" \
            .
          echo ::endgroup::
        env:
          INPUT_PATH: docs

      - name: Upload artifact
        id: upload-artifact
        uses: actions/upload-artifact@v4
        with:
          name: github-pages
          path: ${{ runner.temp }}/artifact.tar
          retention-days: 1
          if-no-files-found: error
          overwrite: true

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