From 9b8a57ace85bca07520ba9434e67051d86e492f6 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 19 Dec 2005 11:13:48 +0000
Subject: [PATCH] libraries-ext.ps generation (dep graph with daemons and
 clusters)

---
 helm/ocaml/Makefile.in   |  6 ++++-
 helm/ocaml/clusters.dot  | 53 ++++++++++++++++++++++++++++++++++++++++
 helm/ocaml/daemons.dot   | 22 +++++++++++++++++
 helm/ocaml/deps.patch    | 11 +++++++++
 helm/ocaml/patch_deps.sh | 29 ++++++++++++++++++++++
 5 files changed, 120 insertions(+), 1 deletion(-)
 create mode 100644 helm/ocaml/clusters.dot
 create mode 100644 helm/ocaml/daemons.dot
 create mode 100644 helm/ocaml/deps.patch
 create mode 100755 helm/ocaml/patch_deps.sh

diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in
index aa9fb9c41..3dabc3ad4 100644
--- a/helm/ocaml/Makefile.in
+++ b/helm/ocaml/Makefile.in
@@ -87,9 +87,13 @@ METAS/META.helm-%: METAS/meta.helm-%.src
 	for i in $(MODULES); do echo "\"helm-$$i\" [shape=box,style=filled,fillcolor=yellow];" >> $@ ; done
 	echo "}" >> $@
 
+.extdep.dot: .dep.dot
+	./patch_deps.sh $< $@
+
 libraries.ps: .dep.dot
 	dot -Tps -o $@ $<
-
+libraries-ext.ps: .extdep.dot
+	dot -Tps -o $@ $<
 libraries-complete.ps: .alldep.dot
 	dot -Tps -o $@ $<
 
diff --git a/helm/ocaml/clusters.dot b/helm/ocaml/clusters.dot
new file mode 100644
index 000000000..7872df240
--- /dev/null
+++ b/helm/ocaml/clusters.dot
@@ -0,0 +1,53 @@
+//   clusterrank = none;
+  fillcolor = "gray93";
+  fontsize = 24;
+  node [fontsize = 24];
+  /* libs clusters */
+  subgraph cluster_presentation {
+    label = "Terms at the content and presentation level";
+    labelloc = "b";
+    labeljust = "r";
+    style = "filled";
+    color = "white"
+    acic_content;
+    cic_acic;
+    cic_disambiguation;
+    content_pres;
+    grafite;
+  }
+  subgraph cluster_partially {
+    label = "Partially specified terms";
+    labelloc = "t";
+    labeljust = "l";
+    style = "filled";
+    color = "white"
+    cic_unification;
+    tactics;
+    paramodulation;
+  }
+  subgraph cluster_fully {
+    label = "Fully specified terms";
+    labelloc = "b";
+    labeljust = "l";
+    style = "filled";
+    color = "white"
+    cic;
+    cic_proof_checking;
+    getter;
+    metadata;
+    urimanager;
+    whelp;
+  }
+  subgraph cluster_utilities {
+    label = "Utilities";
+    labelloc = "b";
+    labeljust = "r";
+    style = "filled";
+    color = "white"
+    extlib;
+    hgdome;
+    hmysql;
+    registry;
+//     utf8_macros;
+    xml;
+  }
diff --git a/helm/ocaml/daemons.dot b/helm/ocaml/daemons.dot
new file mode 100644
index 000000000..66bffba2d
--- /dev/null
+++ b/helm/ocaml/daemons.dot
@@ -0,0 +1,22 @@
+  /* apps */
+  subgraph applications {
+    node [shape=plaintext,style=filled,fillcolor=slategray2];
+    DependencyAnalyzer [label="Dependency\nAnalyzer"];
+    Getter;
+    Matita;
+    ProofChecker [label="Proof\nChecker"];
+    Uwobo;
+    Whelp;
+  }
+  /* apps dep */
+  DependencyAnalyzer -> metadata;
+  Getter -> getter;
+  Matita -> cic_disambiguation;
+  Matita -> grafite_engine;
+  Matita -> grafite_parser;
+  Matita -> hgdome;
+  Matita -> paramodulation;
+  ProofChecker -> cic_proof_checking;
+  Uwobo -> content_pres;
+  Whelp -> cic_disambiguation;
+  Whelp -> content_pres;
diff --git a/helm/ocaml/deps.patch b/helm/ocaml/deps.patch
new file mode 100644
index 000000000..d7f9cf8c9
--- /dev/null
+++ b/helm/ocaml/deps.patch
@@ -0,0 +1,11 @@
+--- .dep.dot	2005-12-19 12:07:15.000000000 +0100
++++ .dep.dot.new	2005-12-19 12:08:10.000000000 +0100
+@@ -14,7 +14,7 @@
+ "cic_unification" -> "library";
+ "library" -> "metadata";
+ "library" -> "cic_acic";
+-"metadata" -> "cic_proof_checking";
++"metadata" -> "cic";
+ "metadata" -> "hmysql";
+ "grafite" -> "content_pres";
+ "content_pres" -> "utf8_macros";
diff --git a/helm/ocaml/patch_deps.sh b/helm/ocaml/patch_deps.sh
new file mode 100755
index 000000000..2abbbeab1
--- /dev/null
+++ b/helm/ocaml/patch_deps.sh
@@ -0,0 +1,29 @@
+#!/bin/sh
+# script args: source_file target_file
+
+use_clusters='yes'
+
+# args: file snippet
+# file will be modified in place
+include_dot_snippet ()
+{
+  echo "Adding to $1 graphviz snipet $2 ..."
+  sed -i "/digraph/r $2" $1
+}
+
+# args: file patch
+apply_patch ()
+{
+  if [ -f "$2" ]; then
+    echo "Applying to $1 patch $2 ..."
+    patch $1 $2
+  fi
+}
+
+cp $1 $2
+apply_patch $2 deps.patch
+include_dot_snippet $2 daemons.dot
+if [ "$use_clusters" = "yes" ]; then
+  include_dot_snippet $2 clusters.dot
+fi
+
-- 
2.39.2