CI: Automatically Generating Html Documentation for each Pull Requests #2
Workflow file for this run
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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: [email protected] | |
| - 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 }} |