diff --git a/.github/workflows/generate_docs.yml b/.github/workflows/generate_docs.yml new file mode 100644 index 0000000000..cef459a3cf --- /dev/null +++ b/.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