ci.yml

name: CI

on: [ push , pull_request , merge_group ]

concurrency:
  group: "${{ github.workflow }} @ ${{ github.event.pull_request.head.label || github.head_ref || github.ref }}"
  cancel-in-progress: true

# We set the supported coq-version from here. In order to use this environment variable correctly, look at how they are used in the following jobs.
env:
  coq-version-supported: '8.19'
  ocaml-version: '4.14-flambda'
  deployment-branch: 'gh-pages'

# Our jobs come in 3 stages, the latter stages depending on the former:
# - Stage 1: Build jobs
# - Stage 2: Documentation and validation jobs
# - Stage 3: Deployment job
# - Stage 4: Clean-up job

jobs:

#
#  Stage 1:
#

# Here we define the build jobs:
# - opam-build: Building the library using opam
# - quick-build: Building the library quickly using make
# - build: Building with timeing information for use in doc jobs

  # Building the library using opam
  opam-build:
    strategy:
      fail-fast: false
      matrix:
        coq-version-dummy:
        - 'supported'
        - 'latest'
        - 'dev'
        os:
          - ubuntu-latest
    env:
      coq-version: ${{ matrix.coq-version-dummy }}
    runs-on: ${{ matrix.os }}
    steps:
    # Github actions doesn't let us set workflow level enviornment variables inside the stategy of a job. Therefore we use the dummy variable coq-version in the matrix to set an environment varible env.coq-version, which uses the globablly set coq-version-supported when running the 'supported' case.
    - name: Set supported coq-version
      if: matrix.coq-version-dummy == 'supported'
      run: echo "coq-version=${{ env.coq-version-supported }}" >> $GITHUB_ENV

    - name: Checkout repo
      uses: actions/checkout@v4
    - name: Build HoTT
      uses: coq-community/docker-coq-action@v1
      with:
        opam_file: 'coq-hott.opam'
        coq_version: ${{ env.coq-version }}
        ocaml_version: ${{ env.ocaml-version }}
        export: 'OPAMWITHTEST'
      env:
        OPAMWITHTEST: 'true'

  # Quick build
  quick-build:
    strategy:
      fail-fast: false
      matrix:
        coq-version-dummy:
        - 'supported'
        - 'latest'
        - 'dev'
        os:
        - ubuntu-latest
    env:
      coq-version: ${{ matrix.coq-version-dummy }}
    runs-on: ${{ matrix.os }}
    steps:
    # Github actions doesn't let us set workflow level enviornment variables inside the stategy of a job. Therefore we use the dummy variable coq-version in the matrix to set an environment varible env.coq-version, which uses the globablly set coq-version-supported when running the 'supported' case.
    - name: Set supported coq-version
      if: matrix.coq-version-dummy == 'supported'
      run: echo "coq-version=${{ env.coq-version-supported }}" >> $GITHUB_ENV
    - name: Checkout repo
      uses: actions/checkout@v4
    - name: Build HoTT
      uses: coq-community/docker-coq-action@v1
      with:
        coq_version: ${{ env.coq-version }}
        ocaml_version: ${{ env.ocaml-version }}
        custom_script: |
          startGroup "Workaround permission issue" # https://github.com/coq-community/docker-coq-action#permissions
          sudo chown -R coq:coq .
          endGroup
          echo "::remove-matcher owner=coq-problem-matcher::" # remove problem matcher installed by Coq docker action, so we don't get duplicate warning annotations
          make -j2
    - name: Revert permissions
      # to avoid a warning at cleanup time - https://github.com/coq-community/docker-coq-action#permissions
      if: ${{ always() }}
      run: sudo chown -R 1001:116 .

  # Main build which docs will run off
  build:
    strategy:
      fail-fast: false
      matrix:
        # We build on our supported version of coq and the master version
        coq-version-dummy:
        - 'supported'
        - 'latest'
        include:
        - coq-version-dummy: 'dev'
          extra-gh-reportify: '--warnings'
    env:
      coq-version: ${{ matrix.coq-version-dummy }}
    runs-on: ubuntu-latest
    steps:
    # Github actions doesn't let us set workflow level enviornment variables inside the stategy of a job. Therefore we use the dummy variable coq-version in the matrix to set an environment varible env.coq-version, which uses the globablly set coq-version-supported when running the 'supported' case.
    - name: Set supported coq-version
      if: matrix.coq-version-dummy == 'supported'
      run: echo "coq-version=${{ env.coq-version-supported }}" >> $GITHUB_ENV
    # Checkout branch
    - uses: actions/checkout@v4
      with:
        submodules: recursive
    # We use the coq docker so we don't have to build coq
    - uses: coq-community/docker-coq-action@v1
      with:
        coq_version: ${{ env.coq-version }}
        ocaml_version: ${{ env.ocaml-version }}
        custom_script: |
          startGroup "Workaround permission issue" # https://github.com/coq-community/docker-coq-action#permissions
            sudo chown -R coq:coq .
          endGroup
          echo "::remove-matcher owner=coq-problem-matcher::" # remove problem matcher installed by Coq docker action, so we don't get duplicate warning annotations
          sudo apt-get -o Acquire::Retries=30 update -q
          sudo apt-get -o Acquire::Retries=30 install python3 python-is-python3 -y --allow-unauthenticated
          etc/coq-scripts/github/reportify-coq.sh --errors ${{ matrix.extra-gh-reportify }} make TIMED=1 -j2 --output-sync

    - name: Revert permissions
      # to avoid a warning at cleanup time - https://github.com/coq-community/docker-coq-action#permissions
      if: ${{ always() }}
      run: sudo chown -R 1001:116 .
    # Tar workspace files
    - name: 'Tar .vo files'
      run: tar -cf workspace.tar .
    # We upload build artifacts for use by documentation
    - name: 'Upload Artifact'
      uses: actions/upload-artifact@v4
      with:
        name: workspace-${{ env.coq-version }}
        path: workspace.tar

  # Nix build
  nix:
    runs-on: ubuntu-latest
    steps:
    - uses: actions/checkout@v4
    - uses: cachix/install-nix-action@v20
      with:
        name: coq-hott
        authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
        extraPullNames: coq-hott
    - run: nix build


#
#  Stage 2:
#

# Here we define the documentation and validation jobs:
# - doc-alectryon: Builds the alectryon documentation
# - doc-dep-graph: Builds dependency graphs
# - doc-coqdoc: Builds the coqdoc documentation
# - doc-timing: Builds the timing documentation
# - coqchk: Runs coqchk
# - install: Tests install target

   # alectryon job
  doc-alectryon:
    needs: build
    runs-on: ubuntu-latest
    steps:
    - uses: actions/checkout@v4
      with:
        submodules: recursive
    # Download artifact
    - uses: actions/download-artifact@v4
      with:
        name: workspace-${{ env.coq-version-supported }}
    # Unpack Tar
    - run: tar -xf workspace.tar
    - name: add problem matchers
      run: |
        #echo "::add-matcher::etc/coq-scripts/github/coq-oneline-error.json" # now via a script
        #echo "::add-matcher::etc/coq-scripts/github/coqdoc.json" # disabled for now, since they don't have file names
        echo "::add-matcher::etc/coq-scripts/github/alectryon-error.json"
        #echo "::add-matcher::etc/coq-scripts/github/alectryon-warning.json" # too noisy right now, cf https://github.com/cpitclaudel/alectryon/issues/34 and https://github.com/cpitclaudel/alectryon/issues/33
    - uses: coq-community/docker-coq-action@v1
      with:
        coq_version: ${{ env.coq-version-supported }}
        ocaml_version: ${{ env.ocaml-version }}
        custom_script: |
          opam install -y coq-serapi
          sudo apt-get -o Acquire::Retries=30 update -q
          sudo apt-get -o Acquire::Retries=30 install python3-pip python3-venv autoconf -y --allow-unauthenticated
          startGroup "Workaround permission issue" # https://github.com/coq-community/docker-coq-action#permissions
            sudo chown -R coq:coq .
          endGroup
          # Create and activate a virtual environment
          python3 -m venv myenv
          source myenv/bin/activate
          # Install the required Python packages in the virtual environment
          python -m pip install --upgrade pip
          python -m pip install pygments dominate beautifulsoup4 docutils==0.17.1
          echo "::remove-matcher owner=coq-problem-matcher::" # remove problem matcher installed by Coq docker action, so we don't get duplicate warning annotations
          make alectryon ALECTRYON_EXTRAFLAGS=--traceback
    - name: Revert permissions
      # to avoid a warning at cleanup time - https://github.com/coq-community/docker-coq-action#permissions
      if: ${{ always() }}
      run: sudo chown -R 1001:116 .
    - name: tar alectryon artifact
      run: tar -cf alectryon-html.tar alectryon-html
    - name: upload alectryon artifact
      uses: actions/upload-artifact@v4
      with:
        name: alectryon-html
        path: alectryon-html.tar


  # dependency graph doc job
  doc-dep-graphs:
    needs: build
    runs-on: ubuntu-latest
    steps:
    # Checkout branch
    - uses: actions/checkout@v4
      with:
        submodules: recursive
    # Download artifact
    - uses: actions/download-artifact@v4
      with:
        name: workspace-${{ env.coq-version-supported }}
    # Unpack Tar
    - run: tar -xf workspace.tar
    # We use the coq docker so we don't have to build coq
    - uses: coq-community/docker-coq-action@v1
      with:
        coq_version: ${{ env.coq-version-supported }}
        ocaml_version: ${{ env.ocaml-version }}
        custom_script: |
          sudo apt-get update
          sudo apt-get install -y ghc cabal-install
          sudo apt-get install -y --allow-unauthenticated \
          libssl-dev aspcud \
          graphviz xsltproc python3-lxml python-pexpect-doc \
          libxml2-dev libxslt1-dev time lua5.1 unzip npm
          # libnode-dev node-gyp

          cabal update
          cabal install --lib graphviz text fgl
          sudo -E npm config set strict-ssl false
          #sudo -E npm i -g npm
          sudo -E npm install -g doctoc

          startGroup "Workaround permission issue" # https://github.com/coq-community/docker-coq-action#permissions
            sudo chown -R coq:coq .
          endGroup
          echo "::remove-matcher owner=coq-problem-matcher::" # remove problem matcher installed by Coq docker action, so we don't get duplicate warning annotations
          ## Make dependency graph
          make HoTT.deps HoTTCore.deps
          runhaskell etc/DepsToDot.hs --coqdocbase="http://hott.github.io/Coq-HoTT/alectryon-html/" --title="HoTT Library Dependency Graph" < HoTT.deps > HoTT.dot
          runhaskell etc/DepsToDot.hs --coqdocbase="http://hott.github.io/Coq-HoTT/alectryon-html/" --title="HoTT Core Library Dependency Graph" < HoTTCore.deps > HoTTCore.dot
          dot -Tsvg HoTT.dot -o HoTT.svg
          dot -Tsvg HoTTCore.dot -o HoTTCore.svg
          rm -rf dep-graphs
          mkdir -p dep-graphs
          mv HoTT.svg HoTTCore.svg dep-graphs/

          ## Install coq-dpdgraph
          opam install coq-dpdgraph.1.0+8.19 -y

          # For some reason, we get a stackoverflow. So we are lax
          # with making these.
          ulimit -s unlimited
          make svg-file-dep-graphs -k || true
          ## Try to make again to see errors
          make svg-file-dep-graphs -k || true
          # `dot` hates file-dep-graphs/hott-all.dot, because it's too big, and
          # makes `dot` spin for over a dozen minutes.  So disable it for now.
          #make svg-aggregate-dep-graphs -k || exit $?

          # We try to make the index.html but there might be some dead
          # links if the previous didn't succeed.
          make file-dep-graphs/index.html -k || true

    - name: Revert permissions
      # to avoid a warning at cleanup time - https://github.com/coq-community/docker-coq-action#permissions
      if: ${{ always() }}
      run: sudo chown -R 1001:116 .
    # Tar dependency graph files
    - name: 'Tar .svg files'
      run: |
        tar -cf dep-graphs.tar dep-graphs
        tar -cf file-dep-graphs.tar file-dep-graphs
    # We upload the artifacts
    - name: 'Upload Artifact dep-graphs.tar'
      uses: actions/upload-artifact@v4
      with:
        name: dep-graphs
        path: dep-graphs.tar
    - name: 'Upload Artifact file-dep-graphs.tar'
      uses: actions/upload-artifact@v4
      with:
        name: file-dep-graphs
        path: file-dep-graphs.tar

  # doc-coqdoc job
  # This builds coqdoc and timing docs and uploads their artifacts
  doc-coqdoc:
    needs: build
    runs-on: ubuntu-latest
    steps:
    # Checkout branch
    - uses: actions/checkout@v4
      with:
        submodules: recursive
    # Download artifact
    - uses: actions/download-artifact@v4
      with:
        name: workspace-${{ env.coq-version-supported }}
    # Unpack Tar
    - run: tar -xf workspace.tar
    # We use the coq docker so we don't have to build coq
    - uses: coq-community/docker-coq-action@v1
      with:
        coq_version: ${{ env.coq-version-supported }}
        ocaml_version: ${{ env.ocaml-version }}
        custom_script: |
          startGroup "Workaround permission issue" # https://github.com/coq-community/docker-coq-action#permissions
            sudo chown -R coq:coq .
          endGroup
          echo "::remove-matcher owner=coq-problem-matcher::" # remove problem matcher installed by Coq docker action, so we don't get duplicate warning annotations
          ## Make HTML doc
          make -j2 html
          mv html coqdoc-html
    - name: Revert permissions
      # to avoid a warning at cleanup time - https://github.com/coq-community/docker-coq-action#permissions
      if: ${{ always() }}
      run: sudo chown -R 1001:116 .
    # Tar html files
    - name: 'Tar doc files'
      run: tar -cf coqdoc-html.tar coqdoc-html
    # Upload coqdoc-html artifact
    - name: 'Upload coqdoc-html Artifact'
      uses: actions/upload-artifact@v4
      with:
        name: coqdoc-html
        path: coqdoc-html.tar

  # doc-timing job
  # This builds coqdoc and timing docs and uploads their artifacts
  doc-timing:
    needs: build
    runs-on: ubuntu-latest
    steps:
    # Checkout branch
    - uses: actions/checkout@v4
      with:
        submodules: recursive
    # Download artifact
    - uses: actions/download-artifact@v4
      with:
        name: workspace-${{ env.coq-version-supported }}
    # Unpack Tar
    - run: tar -xf workspace.tar
    # We use the coq docker so we don't have to build coq
    - uses: coq-community/docker-coq-action@v1
      with:
        coq_version: ${{ env.coq-version-supported }}
        ocaml_version: ${{ env.ocaml-version }}
        custom_script: |
          sudo apt-get update
          sudo apt-get install -y time python3 python-is-python3 lua5.1
          startGroup "Workaround permission issue" # https://github.com/coq-community/docker-coq-action#permissions
            sudo chown -R coq:coq .
          endGroup
          echo "::remove-matcher owner=coq-problem-matcher::" # remove problem matcher installed by Coq docker action, so we don't get duplicate warning annotations
          ## Make timing doc
          make -j2 timing-html
    - name: Revert permissions
      # to avoid a warning at cleanup time - https://github.com/coq-community/docker-coq-action#permissions
      if: ${{ always() }}
      run: sudo chown -R 1001:116 .
    # Tar html files
    - name: 'Tar doc files'
      run: tar -cf timing-html.tar timing-html
    # Upload timing-html artifact
    - name: 'Upload timing-html Artifact'
      uses: actions/upload-artifact@v4
      with:
        name: timing-html
        path: timing-html.tar

  # The coqchk job
  coqchk:
    needs: build
    strategy:
      fail-fast: false
      matrix:
        # We build on our supported version of coq and the master version
        coq-version-dummy:
        - 'supported'
        - 'latest'
        - 'dev'
    env:
      coq-version: ${{ matrix.coq-version-dummy }}
    runs-on: ubuntu-latest
    steps:
    # Github actions doesn't let us set workflow level enviornment variables inside the stategy of a job. Therefore we use the dummy variable coq-version in the matrix to set an environment varible env.coq-version, which uses the globablly set coq-version-supported when running the 'supported' case.
    - name: Set supported coq-version
      if: matrix.coq-version-dummy == 'supported'
      run: echo "coq-version=${{ env.coq-version-supported }}" >> $GITHUB_ENV
    # Checkout branch
    - uses: actions/checkout@v4
      with:
        submodules: recursive
    # Download artifact
    - uses: actions/download-artifact@v4
      with:
        name: workspace-${{ env.coq-version }}
    # Unpack Tar
    - run: tar -xf workspace.tar
    # We use the coq docker so we don't have to build coq
    - uses: coq-community/docker-coq-action@v1
      with:
        coq_version: ${{ env.coq-version }}
        ocaml_version: ${{ env.ocaml-version }}
        custom_script: |
          startGroup "Workaround permission issue" # https://github.com/coq-community/docker-coq-action#permissions
            sudo chown -R coq:coq .
          endGroup
          echo "::remove-matcher owner=coq-problem-matcher::" # remove problem matcher installed by Coq docker action, so we don't get duplicate warning annotations
          make validate
    - name: Revert permissions
      # to avoid a warning at cleanup time - https://github.com/coq-community/docker-coq-action#permissions
      if: ${{ always() }}
      run: sudo chown -R 1001:116 .

  # Test install target
  install:
    needs: build
    strategy:
      fail-fast: false
      matrix:
        # We build on our supported version of coq and the master version
        coq-version-dummy:
        - 'supported'
        - 'latest'
        - 'dev'
    env:
      coq-version: ${{ matrix.coq-version-dummy }}
    runs-on: ubuntu-latest
    steps:
    # Github actions doesn't let us set workflow level enviornment variables inside the stategy of a job. Therefore we use the dummy variable coq-version in the matrix to set an environment varible env.coq-version, which uses the globablly set coq-version-supported when running the 'supported' case.
    - name: Set supported coq-version
      if: matrix.coq-version-dummy == 'supported'
      run: echo "coq-version=${{ env.coq-version-supported }}" >> $GITHUB_ENV
    # Checkout branch
    - uses: actions/checkout@v4
      with:
        submodules: recursive
    # Download artifact
    - uses: actions/download-artifact@v4
      with:
        name: workspace-${{ env.coq-version }}
    # Unpack Tar
    - run: tar -xf workspace.tar
    # We use the coq docker so we don't have to build coq
    - uses: coq-community/docker-coq-action@v1
      with:
        coq_version: ${{ env.coq-version }}
        ocaml_version: ${{ env.ocaml-version }}
        custom_script: |
          startGroup "Workaround permission issue" # https://github.com/coq-community/docker-coq-action#permissions
            sudo chown -R coq:coq .
          endGroup
          echo "::remove-matcher owner=coq-problem-matcher::" # remove problem matcher installed by Coq docker action, so we don't get duplicate warning annotations
          ## Test install target
          make install
          echo 'Require Import HoTT.HoTT.' | coqtop -q

    - name: Revert permissions
      # to avoid a warning at cleanup time - https://github.com/coq-community/docker-coq-action#permissions
      if: ${{ always() }}
      run: sudo chown -R 1001:116 .

#
#  Stage 3
#

  deploy-doc:
    # We only deploy when the reference is the master branch
    if: ${{ github.ref == 'refs/heads/master' }}
    # This job relies on the documentation jobs having finished. Technically we don't need to rely on coqchk and install, but it is simpler this way.
    needs:
    - coqchk
    - install
    - doc-alectryon
    - doc-dep-graphs
    - doc-coqdoc
    - doc-timing
    runs-on: ubuntu-latest
    steps:
    # Checkout branch
    - uses: actions/checkout@v4
    # Download alectryon artifact
    - uses: actions/download-artifact@v4
      with:
        name: alectryon-html
    # Download dependency graph artifacts
    - uses: actions/download-artifact@v4
      with:
        name: dep-graphs
    # Download file dependency graph artifacts
    - uses: actions/download-artifact@v4
      with:
        name: file-dep-graphs
    # Download coqdoc artifact
    - uses: actions/download-artifact@v4
      with:
        name: coqdoc-html
    # Download timing artifact
    - uses: actions/download-artifact@v4
      with:
        name: timing-html
    # Unpack Tar files
    - run: |
        mkdir doc
        tar -xf alectryon-html.tar  -C doc
        tar -xf dep-graphs.tar      -C doc
        tar -xf file-dep-graphs.tar -C doc
        tar -xf coqdoc-html.tar     -C doc
        tar -xf timing-html.tar     -C doc

    - name: Deploy 🚀
      uses: JamesIves/github-pages-deploy-action@4.1.8
      with:
        branch: ${{ env.deployment-branch }}
        folder: doc
        single-commit: true


#
#  Stage 4
#

# Here we define the cleanup job:
# - delete-artifacts: We delete the artifacts from the previous jobs

  delete-artifacts:
    # We always want to run this job even if we cancel
    if: ${{ always() }}
    # We depend on the stage 3 jobs
    needs:
    - deploy-doc
    runs-on: ubuntu-latest
    steps:
    # Delete workspace artifacts
    - uses: geekyeggo/delete-artifact@v5
      with:
        name: workspace-${{ env.coq-version-supported }}
    - uses: geekyeggo/delete-artifact@v5
      with:
        name: workspace-latest
    - uses: geekyeggo/delete-artifact@v5
      with:
        name: workspace-dev
    # Delete documentation artifacts
    - uses: geekyeggo/delete-artifact@v5
      with:
        name: dep-graphs
    - uses: geekyeggo/delete-artifact@v5
      with:
        name: file-dep-graphs
    - uses: geekyeggo/delete-artifact@v5
      with:
        name: alectryon-html
    - uses: geekyeggo/delete-artifact@v5
      with:
        name: coqdoc-html
    - uses: geekyeggo/delete-artifact@v5
      with:
        name: timing-html