From 87552336143ee6eea9ed87866d344947dbe71719 Mon Sep 17 00:00:00 2001
From: Yoshihiro Imai <y.imai@aist.go.jp>
Date: Fri, 10 Jan 2025 17:27:43 +0900
Subject: [PATCH] feat: make looks good for Hierarchy graphs

---
 generate_index.ml                   | 4 ++--
 graphviz.ml                         | 3 +++
 graphviz.mli                        | 1 +
 tools/generate-hierarchy-graph.sh   | 8 +++++++-
 tools/generate-mathcomp-analysis.sh | 4 +++-
 5 files changed, 16 insertions(+), 4 deletions(-)

diff --git a/generate_index.ml b/generate_index.ml
index fed7de06..594b3c95 100644
--- a/generate_index.ml
+++ b/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"/>
diff --git a/graphviz.ml b/graphviz.ml
index dfd54530..af8e2c28 100644
--- a/graphviz.ml
+++ b/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)
diff --git a/graphviz.mli b/graphviz.mli
index d9ad32e5..c431c4d0 100644
--- a/graphviz.mli
+++ b/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
diff --git a/tools/generate-hierarchy-graph.sh b/tools/generate-hierarchy-graph.sh
index dfc70f7b..72a679c9 100755
--- a/tools/generate-hierarchy-graph.sh
+++ b/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
diff --git a/tools/generate-mathcomp-analysis.sh b/tools/generate-mathcomp-analysis.sh
index e11bc6e5..b4ad4cb4 100755
--- a/tools/generate-mathcomp-analysis.sh
+++ b/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