lean_doc.yml

on:
  push:

jobs:
  build_docs:
    runs-on: ubuntu-latest
    name: Build docs
    environment: 
      name: documentation
      url: https://pygae.github.io/lean-ga-docs
    steps:

    - name: 📁 Checkout project
      uses: actions/checkout@v2
      with:
        fetch-depth: 0

    - 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: 🐍 Install Python
      uses: actions/setup-python@v1
      with:
        python-version: 3.8

    - name: 📁 Checkout Lean's doc-gen
      uses: actions/checkout@v2
      with:
        fetch-depth: 0
        repository: leanprover-community/doc-gen
        path: doc-gen

    - name: 🐍 Install Python dependencies
      run: |
        python -m pip install --upgrade pip
        pip install -r doc-gen/requirements.txt
        ls doc-gen

    - name: ✏️ Mangle paths for doc-gen
      run: |
        lean_version="$(sed '/^lean_version/!d;s/.*"\(.*\)".*/\1/' leanpkg.toml)"
        mathlib_git_hash="$(sed '/rev/!d;s/.*"\([a-z0-9]*\)".*/\1/' leanpkg.toml)"
        cd doc-gen
        sed -i "s/rev = \"\S*\"/rev = \"$mathlib_git_hash\"/" leanpkg.toml
        
        # Force doc_gen project to match the Lean version used in CI.
        # If they are incompatible, something in doc_gen will fail to compile,
        # but this is better than trying to recompile all of mathlib.
        elan override set "$lean_version"

        leanproject get-mathlib-cache
        echo -e "path ../src" >> leanpkg.path
        cat leanpkg.path
        (cd ../src;
        find "." -name \*.lean -not -name all.lean \
          | sed 's,^\./,,;s,\.lean$,,;s,/,.,g;s,^,import ,' \
          | sort >./all.lean)

        cp _target/deps/mathlib/docs/references.bib ../docs

        cat ../src/all.lean
        lean --path

    - name: 🔧 Build the lean code
      run: |
        cd doc-gen
        lean -v
        lean --make src/entrypoint.lean

    - name: 📝 Export Lean symbol information
      run: |
        cd doc-gen
        lean --run src/entrypoint.lean > export.json

    - name: 📚 Build HTML docs
      run: |
        cd doc-gen
        python3 \
          -c "import print_docs; del print_docs.extra_doc_files[:]; print_docs.copy_yaml_bib_files = lambda p: None; print_docs.library_link_roots['lean-ga'] = 'https://github.com/pygae/lean-ga/blob/$GITHUB_SHA/src/'; print_docs.main()" \
          -r .. -w 'https://pygae.github.io/lean-ga-docs/' -t built-docs

    - name: 🔑 Install SSH Client
      uses: webfactory/ssh-agent@v0.4.1
      with:
        ssh-private-key: ${{ secrets.DEPLOY_KEY }}

    - name: 🚀 Deploy
      uses: JamesIves/github-pages-deploy-action@3.7.1
      with:
        SSH: true
        SINGLE_COMMIT: true
        REPOSITORY_NAME: pygae/lean-ga-docs
        BRANCH: gh-pages # The branch the action should deploy to.
        FOLDER: doc-gen/built-docs # The folder the action should deploy.