generate_htmldoc_for_pullrequests.yml

on:
  pull_request:

jobs:
  generate-html-and-deploy:
    runs-on: ubuntu-latest
    steps:
      - name: Set the destination directory for PR event
        if: ${{ github.event_name == 'pull_request' }}
        run: echo "destination_dir=doc/pr/${{ github.head_ref }}" >> $GITHUB_ENV

      - name: Setup Graphviz
        uses: ts-graphviz/setup-graphviz@v2

      - name: Checkout
        uses: actions/checkout@v4

      - name: Setup Coq
        uses: coq-community/docker-coq-action@v1
        with:
          opam_file: 'coq-mathcomp-analysis.opam'
          coq_version: 8.19
          ocaml_version: 4.14-flambda
          before_install: |
            opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
            opam update
            opam install -y coq-rocqnavi
          before_script: |
            startGroup "Workaround permission issue"
              sudo chown -R coq:coq .
            endGroup
          after_script: |
            mkdir -p html
            FILES=$(find . -name "*.v" -or -name "*.glob")
            coq2html -d html -title "MathComp-Analysis" -base mathcomp \
              -Q theories analysis -coqlib https://coq.inria.fr/doc/V8.19.0/stdlib/ \
              -external https://math-comp.github.io/htmldoc_2_1_0/ mathcomp.ssreflect \
              -external https://math-comp.github.io/htmldoc_2_1_0/ mathcomp.algebra \
              $FILES

      - name: Deploy
        uses: peaceiris/actions-gh-pages@v4
        with:
          github_token: ${{ secrets.GITHUB_TOKEN }}
          publish_dir: html/
          destination_dir: ${{ env.destination_dir }}
          keep_files: true
          user_name: github-actions
          user_email: github-actions@github.com

      - name: Set URL of the Html doc
        run: echo "doc_url=https://${{ github.repository_owner }}.github.io/${{ github.event.repository.name }}/${{ env.destination_dir }}" >> $GITHUB_ENV
      - name: Feedback as a PR comment
        if: ${{ github.event_name == 'pull_request' && github.event.action == 'opened' }}
        run: |
          gh pr comment ${{ github.event.number }} --body "The HTML Documentation was generated by Rocqnavi: ${{ env.doc_url }}"
        env:
          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}