Skip to content

Commit 724c1d5

Browse files
committed
CI: Rocqnavi released version
1 parent d9ba8ca commit 724c1d5

File tree

1 file changed

+3
-4
lines changed

1 file changed

+3
-4
lines changed

.github/workflows/generate_docs.yml

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -28,20 +28,19 @@ jobs:
2828
with:
2929
ocaml-compiler: 4.14
3030
opam-repositories: |
31-
coq-extra-dev: https://coq.inria.fr/opam/extra-dev
3231
coq-released: https://coq.inria.fr/opam/released
3332
default: https://github.com/ocaml/opam-repository.git
3433
3534
- name: Build Mathcomp Analysis
3635
run: opam install -y --deps-only . && opam exec -- make -j 4
3736

38-
- name: Build coq2html
39-
run: opam install -y coq-rocqnavi && opam show coq-rocqnavi
37+
- name: Build rocqnavi
38+
run: opam install -y rocq-navi && opam show rocq-navi
4039

4140
- name: Generate Documents
4241
run: |
4342
mkdir -p artifact/${{ env.destination_dir }}
44-
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
43+
opam exec -- rocqnavi -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
4544
4645
- name: Upload artifact
4746
uses: actions/upload-artifact@v4

0 commit comments

Comments
 (0)