Skip to content

Commit

Permalink
CI: use opam coq extradev package
Browse files Browse the repository at this point in the history
  • Loading branch information
yoshihiro503 committed Feb 7, 2025
1 parent dc6a6f8 commit d736895
Showing 1 changed file with 3 additions and 8 deletions.
11 changes: 3 additions & 8 deletions .github/workflows/generate_docs.yml
Original file line number Diff line number Diff line change
Expand Up @@ -23,30 +23,25 @@ jobs:
branch_name=${{ github.head_ref }}
echo "destination_dir=mathcomp-analysis_$branch_name" >> $GITHUB_ENV
- name: Clone Coq2html
uses: actions/checkout@v4
with:
repository: affeldt-aist/coq2html
path: coq2html

- 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: cd coq2html/ && opam exec -- make
run: opam install -y coq-rocqnavi && opam show coq-rocqnavi

- name: Generate Documents
run: |
mkdir -p artifact/${{ env.destination_dir }}
coq2html/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
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
Expand Down

0 comments on commit d736895

Please sign in to comment.