From f262431123c296af5ee697079c7ade3bf6f8c550 Mon Sep 17 00:00:00 2001 From: Yoshihiro Imai Date: Wed, 14 May 2025 16:29:49 +0900 Subject: [PATCH 1/2] Chore: :memo: :wrench: `make html` to make the html documentation using Rocqnavi This change has been inspire in the repository: https://github.com/CoqHott/logrel-coq --- .github/workflows/generate_docs.yml | 12 +++-- .gitignore | 2 + Makefile.common | 72 +++++++++-------------------- html_doc/generate_deps.pl | 41 ++++++++++++++++ 4 files changed, 72 insertions(+), 55 deletions(-) create mode 100644 html_doc/generate_deps.pl diff --git a/.github/workflows/generate_docs.yml b/.github/workflows/generate_docs.yml index 56e40a1d8..e76a4fdf7 100644 --- a/.github/workflows/generate_docs.yml +++ b/.github/workflows/generate_docs.yml @@ -23,6 +23,9 @@ jobs: branch_name=${{ github.head_ref }} echo "destination_dir=mathcomp-analysis_$branch_name" >> $GITHUB_ENV + - name: Setup Graphviz + uses: ts-graphviz/setup-graphviz@v2 + - name: Set-up OCaml uses: ocaml/setup-ocaml@v3 with: @@ -34,13 +37,14 @@ jobs: - name: Build Mathcomp Analysis run: opam install -y --deps-only . && opam exec -- make -j 4 - - name: Build rocqnavi - run: opam install -y rocq-navi && opam show rocq-navi + - name: Install Rocqnavi + run: opam install -y rocq-navi - name: Generate Documents run: | - mkdir -p artifact/${{ env.destination_dir }} - opam exec -- rocqnavi -title "Mathcomp Analysis" -d artifact/${{ env.destination_dir }} -base mathcomp -Q theories analysis -coqlib https://coq.inria.fr/doc/V8.20.0/stdlib/ -external https://math-comp.github.io/htmldoc_2_3_0/ mathcomp.ssreflect -external https://math-comp.github.io/htmldoc_2_3_0/ mathcomp.algebra $(find . -name "*.v" -or -name "*.glob") + mkdir -p artifact + opam exec -- make html + cp -r html artifact/${{ env.destination_dir }} - name: Upload artifact uses: actions/upload-artifact@v4 diff --git a/.gitignore b/.gitignore index 6eeb1c7a7..ac8865cd8 100644 --- a/.gitignore +++ b/.gitignore @@ -14,3 +14,5 @@ Makefile.coq Makefile.coq.conf + +html/ diff --git a/Makefile.common b/Makefile.common index 182b22825..9ce49cd9c 100644 --- a/Makefile.common +++ b/Makefile.common @@ -119,54 +119,24 @@ endif %.vo: __always__ Makefile.coq +$(COQMAKE) $@ -# the doc targets doc and doc-clean are essentially copied from the Mathematical -# Components repository -# we reuse the scripts from the math-comp git repo (which is hard wired) -# modulo one fix: we change builddoc_lib.sh:l.18 to s/\(\*{5,}+\)//g; - -MATHCOMP = ../math-comp/ - -doc: __always__ Makefile.coq - mkdir -p _build_doc/ - cp -r $(COQFILES) -t _build_doc/ --parents - cp _CoqProject Makefile* _build_doc - mkdir -p _build_doc/htmldoc - . $(MATHCOMP)etc/utils/builddoc_lib.sh; \ - cd _build_doc && mangle_sources $(COQFILES) - +cd _build_doc && $(COQMAKE) -# let's forget about the dependency graph for the time being... -# cd _build_doc && grep -v vio: .Makefile.coq.d > depend -# cd _build_doc && cat depend | $(MATHCOMP)etc/buildlibgraph $(COQFILES) > htmldoc/depend.js - cd _build_doc && $(COQDOC) -t "MathComp Analysis" \ - -g --utf8 -Q classical mathcomp.classical -Q theories mathcomp.analysis \ - --parse-comments \ - --multi-index $(COQFILES) -d htmldoc - . $(MATHCOMP)etc/utils/builddoc_lib.sh; \ - cd _build_doc && postprocess_html - cp $(MATHCOMP)etc/artwork/coqdoc.css _build_doc/htmldoc - -doc-clean: - rm -rf _build_doc/ - -coq2html: - $(COQDEP) -f _CoqProject > depend.d - ../coq2html/ocamldot/ocamldot depend.d > depend.dot - gsed -i 's/Classical/mathcomp\.classical/' depend.dot - gsed -i 's/Theories/mathcomp\.analysis/' depend.dot - gsed -i 's/Reals_stdlib/mathcomp\.reals_stdlib/' depend.dot - gsed -i 's/Experimental_reals/mathcomp\.experimental_reals/' depend.dot - gsed -i 's/Reals/mathcomp\.reals/' depend.dot - gsed -i 's/Analysis_stdlib/mathcomp\.analysis_stdlib/' depend.dot - gsed -i 's/\//\./g' depend.dot - ../coq2html/tools/generate-hierarchy-graph.sh - find . -not -path '*/.*' -name "*.v" -or -name "*.glob" | xargs ../coq2html/coq2html \ - -hierarchy-graph hierarchy-graph.dot \ - -dependency-graph depend.dot \ - -title "Mathcomp Analysis" \ - -d html/ -base mathcomp -Q theories analysis \ - -coqlib https://rocq-prover.org/doc/V8.20.1/stdlib/ \ - -external https://math-comp.github.io/htmldoc_2_3_0/ mathcomp.ssreflect \ - -external https://math-comp.github.io/htmldoc_2_3_0/ mathcomp.algebra - -coq2html-clean: - rm -f */*.glob +# Html documentation + +DOCDIR=html + +$(DOCDIR)/dependency_graph.pre: + mkdir -p $(DOCDIR) + coqdep -f _CoqProject | perl html_doc/generate_deps.pl > $(DOCDIR)/dependency_graph.pre + +$(DOCDIR)/dependency_graph.dot: $(DOCDIR)/dependency_graph.pre + mkdir -p $(DOCDIR) + tred $(DOCDIR)/dependency_graph.pre > $(DOCDIR)/dependency_graph.dot + +html: build $(DOCDIR)/dependency_graph.dot + mkdir -p $(DOCDIR) + find . -not -path '*/.*' -name "*.v" -or -name "*.glob" | xargs rocqnavi \ + -title "Mathcomp Analysis" \ + -d $(DOCDIR) -base mathcomp -Q theories analysis \ + -coqlib https://rocq-prover.org/doc/V8.20.1/stdlib/ \ + -dependency-graph $(DOCDIR)/dependency_graph.dot \ + -external https://math-comp.github.io/htmldoc_2_3_0/ mathcomp.ssreflect \ + -external https://math-comp.github.io/htmldoc_2_3_0/ mathcomp.algebra diff --git a/html_doc/generate_deps.pl b/html_doc/generate_deps.pl new file mode 100644 index 000000000..14fa5161d --- /dev/null +++ b/html_doc/generate_deps.pl @@ -0,0 +1,41 @@ +print "digraph depend {\n"; +print " node [shape = ellipse,style=filled,colorscheme = paired12];\n"; +print " subgraph cluster_analysis { label=\"Analysis\" }\n"; +print " subgraph cluster_classical { label=\"Classical\" }\n"; +print " subgraph cluster_reals { label=\"Reals\" }\n"; +print " subgraph cluster_experimental_reals { label=\"ExperimentalReals\" }\n"; +print " subgraph cluster_analysis { label=\"Analysis\" }\n"; +print " subgraph cluster_topology { label=\"Topology\" }\n"; +print " subgraph cluster_normedtype { label=\"NormedType\" }\n"; +print " subgraph cluster_lebesgue_integral { label=\"Lebesgue_integral\" }\n"; +while (<>) { + if (m/([^\s]*)\.vo.*:(.*)/) { + $dests = $2 ; + ($path,$src) = ($1 =~ s/\//\//rg =~ m/^(?:(.*\/))?([^.]*)$/); + if ($path =~ m/classical\//) { + $url="mathcomp.classical.$src.html"; + print "subgraph cluster_classical { \"$path$src\"[label=\"$src\",URL=\"$url\",fillcolor=1]}\n"; + }elsif ($path =~ m/reals\// or $path =~ m/reals_stdlib\//) { + print "subgraph cluster_reals { \"$path$src\"[label=\"$src\",fillcolor=2,fontcolor=white]}" + }elsif ($path =~ m/experimental_reals\//) { + print "subgraph cluster_experimental_reals { \"$path$src\"[label=\"$src\",fillcolor=3]}" + }elsif ($path =~ m/theories\/topology_theory\//) { + print "subgraph cluster_topology { \"$path$src\"[label=\"$src\",fillcolor=4,fontcolor=white]}" + }elsif ($path =~ m/theories\/normedtype_theory\//) { + print "subgraph cluster_normedtype { \"$path$src\"[label=\"$src\",fillcolor=9]}" + }elsif ($path =~ m/theories\/lebesgue_integral_theory\//) { + print "subgraph cluster_lebesgue_integral { \"$path$src\"[label=\"$src\",fillcolor=10,fontcolor=white]}" + }elsif ($path =~ m/theories\//) { + print "subgraph cluster_analysis { \"$path$src\"[label=\"$src\",fillcolor=5]}" + }elsif ($path =~ m/analysis_stdlib\/.*/) { + print "subgraph cluster_analysis { \"$path$src\"[label=\"$src\",fillcolor=5]}" + }else { + $url="/mathcomp.$src.html"; + print "\"$path$src\"[label=\"$src\",URL=\"$url\",fillcolor=6,fontcolor=white]" + } + for my $dest (split(" ", $dests)) { + print " \"$1\" -> \"$path$src\";\n" if ($dest =~ m/(.*)\.vo/); + } + } +} +print "}\n"; From 8be745e71c1614ce1bf4be285071896ea211a5b2 Mon Sep 17 00:00:00 2001 From: Yoshihiro Imai Date: Wed, 4 Jun 2025 10:22:11 +0900 Subject: [PATCH 2/2] chore: move the perl script generate denendency graph as a dot format to etc directory and rename --- Makefile.common | 2 +- html_doc/generate_deps.pl => etc/builddoc_dependency_dot.pl | 0 2 files changed, 1 insertion(+), 1 deletion(-) rename html_doc/generate_deps.pl => etc/builddoc_dependency_dot.pl (100%) diff --git a/Makefile.common b/Makefile.common index 9ce49cd9c..936cd4ca8 100644 --- a/Makefile.common +++ b/Makefile.common @@ -125,7 +125,7 @@ DOCDIR=html $(DOCDIR)/dependency_graph.pre: mkdir -p $(DOCDIR) - coqdep -f _CoqProject | perl html_doc/generate_deps.pl > $(DOCDIR)/dependency_graph.pre + coqdep -f _CoqProject | perl etc/builddoc_dependency_dot.pl > $(DOCDIR)/dependency_graph.pre $(DOCDIR)/dependency_graph.dot: $(DOCDIR)/dependency_graph.pre mkdir -p $(DOCDIR) diff --git a/html_doc/generate_deps.pl b/etc/builddoc_dependency_dot.pl similarity index 100% rename from html_doc/generate_deps.pl rename to etc/builddoc_dependency_dot.pl