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 }}