CI: automatically generate HTML docs as artifacts by rocqnavi

.github/workflows/generate_docs.yml

@@ -0,0 +1,50 @@
+on:
+  push:
+    branches-ignore: ["gh-pages"]
+  pull_request:
+
+jobs:
+  generate-artifacts:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Set the variables for push event
+        if: ${{ github.event_name == 'push' }}
+        run: |
+          branch_name=${{ github.ref_name }}
+          short_sha=$(git rev-parse --short ${{ github.sha }})
+          echo "destination_dir=mathcomp-analysis_"$branch_name_$short_sha >> $GITHUB_ENV
+
+      - name: Set the variables for PR event
+        if: ${{ github.event_name == 'pull_request' }}
+        run: |
+          branch_name=${{ github.head_ref }}
+          echo "destination_dir=mathcomp-analysis_$branch_name" >> $GITHUB_ENV
+
+      - name: Set-up OCaml
+        uses: ocaml/setup-ocaml@v3
+        with:
+          ocaml-compiler: 4.14
+          opam-repositories: |
+            coq-extra-dev: https://coq.inria.fr/opam/extra-dev
+            coq-released: https://coq.inria.fr/opam/released
+            default: https://github.com/ocaml/opam-repository.git
+
+      - name: Build Mathcomp Analysis
+        run: opam install -y --deps-only . && opam exec -- make -j 4
+
+      - name: Build coq2html
+        run: opam install -y coq-rocqnavi && opam show coq-rocqnavi
+
+      - name: Generate Documents
+        run: |
+          mkdir -p artifact/${{ env.destination_dir }}
+          opam exec -- coq2html -title "Mathcomp Analysis" -d artifact/${{ env.destination_dir }} -base mathcomp -Q theories analysis -coqlib https://coq.inria.fr/doc/V8.18.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 classical/*.glob classical/*.v theories/*.glob theories/*.v
+
+      - name: Upload artifact
+        uses: actions/upload-artifact@v4
+        with:
+          name: ${{ env.destination_dir }}
+          path: artifact