📝 🔧 make html to make the html documentation (#1622)

* Chore: 📝 🔧 `make html` to make the html documentation using Rocqnavi
This change has been inspire in the repository: https://github.com/CoqHott/logrel-coq

Author: yoshihiro503

.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

.gitignore

@@ -14,3 +14,5 @@
 
 Makefile.coq
 Makefile.coq.conf
+
+html/

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 etc/builddoc_dependency_dot.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

etc/builddoc_dependency_dot.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";