libraries-ext.ps generation (dep graph with daemons and clusters)

diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in
index aa9fb9c41a60a6201e8767f36cc7009094018f41..3dabc3ad4b99185e7ad8c0d932e04c2b532da14d 100644 (file)
--- 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 (file)
index 0000000..7872df2
--- /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 (file)
index 0000000..66bffba
--- /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 (file)
index 0000000..d7f9cf8
--- /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 (executable)
index 0000000..2abbbea
--- /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
+