CI: introduce a html generation action

Author: yoshihiro503

.github/workflows/generate_htmldoc_for_pullrequests.yml

@@ -0,0 +1,58 @@
+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 }}