docs.yml

on:
  push:
    branches:
      - master

name: Build and deploy documentation

# borrowed from https://github.com/teorth/pfr/blob/master/.github/workflows/push.yml
permissions:
  contents: read
  pages: write
  id-token: write

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

      - name: Install Graphviz
        run: sudo apt-get update && sudo apt-get install -y graphviz

      - name: Verify Graphviz Installation
        run: dot -V
      ##################
      # Remove this section if you don't want docs to be made
      - 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: Get Mathlib cache
        run: lake -Kenv=dev exe cache get || true

      - name: Build project
        run: lake -Kenv=dev build HepLean

      - name: make TODO list
        run : lake exe TODO_to_yml mkFile

      - name: make list of informal proofs and lemmas
        run : lake exe informal mkFile mkDot mkHTML

      - name: make stats page
        run : lake exe stats mkHTML

      - name: make notes
        run : lake exe notes

      - name: Generate svg from dot
        run : dot -Tsvg -o ./docs/graph.svg ./docs/InformalDot.dot

      - name: Replace template file with custom
        run : cp ./scripts/Template.lean .lake/packages/doc-gen4/DocGen4/Output/Template.lean

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

      - name: Build documentation
        run: lake -Kenv=dev build HepLean:docs

      - name: Copy documentation to `docs/docs`
        run: |
          mv .lake/build/doc docs/docs
      #End Section
      ##################
      - name: Bundle dependencies
        uses: ruby/setup-ruby@v1
        with:
          working-directory: docs
          ruby-version: "3.1" # Not needed with a .ruby-version file
          bundler-cache: true # runs 'bundle install' and caches installed gems automatically


      - name: Bundle website
        working-directory: docs
        run: JEKYLL_ENV=production bundle exec jekyll build

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

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