From 47b7f986678a572870c7be745638c66800d6e90a Mon Sep 17 00:00:00 2001
From: Yoshihiro Imai <y.imai@aist.go.jp>
Date: Fri, 22 Nov 2024 11:27:16 +0900
Subject: [PATCH] CI: introduce a html generation action

---
 .../generate_htmldoc_for_pullrequests.yml     | 58 +++++++++++++++++++
 1 file changed, 58 insertions(+)
 create mode 100644 .github/workflows/generate_htmldoc_for_pullrequests.yml

diff --git a/.github/workflows/generate_htmldoc_for_pullrequests.yml b/.github/workflows/generate_htmldoc_for_pullrequests.yml
new file mode 100644
index 000000000..81c91fef5
--- /dev/null
+++ b/.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 }}