feat: make looks good for Hierarchy graphs

generate_index.ml

@@ -249,12 +249,12 @@ let overwrite_dot_file_with_url xref_table dot_file = (* dirty *)
 
 
 let generate_hierarchy_graph title xref_table output_dir dot_file =
-  overwrite_dot_file_with_url xref_table dot_file;
+(*  overwrite_dot_file_with_url xref_table dot_file;*)
   let png_filename = "hierarchy_graph.png" in
   let png_path = Filename.concat output_dir png_filename in
   let map_path = Filename.concat output_dir "hierarchy_graph.map" in
   Graphviz.from_file dot_file
-  |> Graphviz.generate_file png_path map_path;
+  |> Graphviz.neato png_path map_path;
   let map = read_file map_path in
   (*TODO: ↓ The map id (#Hierarchy) should be taken from dot file *)
   Printf.sprintf {|<h2>Mathematical Structures (%s only)</h2><img src="%s" title usemap="#Hierarchy"/>

graphviz.ml

@@ -4,3 +4,6 @@ let from_file filename = filename
 
 let generate_file pngfile mapfile srcfile =
   Common.shell (Printf.sprintf "tred %s | dot -Tpng -o %s -Tcmapx -o %s" srcfile pngfile mapfile)
+
+let neato pngfile mapfile srcfile =
+  Common.shell (Printf.sprintf "neato -Tpng -n2 %s -o %s -Tcmapx -o %s" srcfile pngfile mapfile)

graphviz.mli

@@ -3,3 +3,4 @@ type t
 val from_file : string -> t
 
 val generate_file : string -> string -> t -> unit
+val neato : string -> string -> t -> unit

tools/generate-hierarchy-graph.sh

@@ -1,6 +1,12 @@
+set -eux
+DIR=$(pwd `dirname 0`)
 coqtop <<EOF
 From HB Require Import structures.
 Require Import mathcomp.classical.all_classical.
+Require Import mathcomp.reals_stdlib/Rstruct.
+Require Import mathcomp.reals.all_reals.
+Require Import mathcomp.analysis_stdlib.Rstruct_topology.
 Require Import mathcomp.analysis.all_analysis.
-HB.graph "hierarchy-graph.dot".
+HB.graph "$DIR/hierarchy-graph0.dot".
 EOF
+ccomps -x $DIR/hierarchy-graph0.dot | tred | dot | gvpack -array3 > $DIR/hierarchy-graph.dot

tools/generate-mathcomp-analysis.sh

@@ -26,12 +26,14 @@ sed -i 's/Analysis_stdlib/mathcomp\.analysis_stdlib/' depend.dot
 sed -i 's/\//\./g' depend.dot
 
 $DIR/tools/generate-hierarchy-graph.sh
+HIERARCHY=$OUTDIR/hierarchy-graph.dot
+cp hierarchy-graph.dot $HIERARCHY
 
 $DIR/coq2html -title "MathComp-Analysis($COMMIT_HASH)" -d $OUTDIR -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 \
-  -hierarchy-graph "hierarchy-graph.dot" \
+  -hierarchy-graph $HIERARCHY \
   -dependency-graph "depend.dot" \
   $FILES