From: Stefano Zacchiroli Date: Thu, 2 Feb 2006 10:35:13 +0000 (+0000) Subject: moved dot stuff to STATS/ X-Git-Tag: make_still_working~7690 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=782253ebe87375f52c07899c1501db5a665a457f;p=helm.git moved dot stuff to STATS/ --- diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in index 337dd0ca0..7ab72ed24 100644 --- a/helm/ocaml/Makefile.in +++ b/helm/ocaml/Makefile.in @@ -1,3 +1,6 @@ + +export SHELL=/bin/bash + # Warning: the modules must be in compilation order NULL = MODULES = \ @@ -27,7 +30,7 @@ MODULES = \ lexicon \ grafite_engine \ grafite_parser \ - tactics/paramodulation \ + tactics/paramodulation \ $(NULL) OCAMLFIND_DEST_DIR = @OCAMLFIND_DEST_DIR@ @@ -49,10 +52,21 @@ clean: $(MODULES:%=%.clean) clean_metas (for m in $(MODULES); do echo -n "$$m:"; cat $$m/.stats; done) \ | sort -t : -k 2 -n -r > .stats +EXTRA_DIST_CLEAN = \ + libraries-clusters.ps \ + libraries-clusters.pdf \ + libraries-ext.ps \ + libraries.ps \ + .dep.dot \ + .extdep.dot \ + .clustersdep.dot \ + $(NULL) + clean_metas: rm -f $(METAS) distclean: clean clean_metas - rm -f Makefile Makefile.common configure config.log config.cache config.status + rm -f configure config.log config.cache config.status + rm -f Makefile Makefile.common $(EXTRA_DIST_CLEAN) .PHONY: all opt world metas depend install uninstall clean clean_metas distclean @@ -96,9 +110,9 @@ METAS/META.helm-%: METAS/meta.helm-%.src echo "}" >> $@ .extdep.dot: .dep.dot - ./patch_deps.sh $< $@ + STATS/patch_deps.sh $< $@ .clustersdep.dot: .dep.dot - USE_CLUSTERS=yes ./patch_deps.sh $< $@ + USE_CLUSTERS=yes STATS/patch_deps.sh $< $@ libraries.ps: .dep.dot dot -Tps -o $@ $< diff --git a/helm/ocaml/STATS/clusters.dot b/helm/ocaml/STATS/clusters.dot new file mode 100644 index 000000000..b7298bce8 --- /dev/null +++ b/helm/ocaml/STATS/clusters.dot @@ -0,0 +1,57 @@ +// 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_disambiguation; + content_pres; + grafite_parser; + lexicon; + } + subgraph cluster_partially { + label = "Partially specified terms"; + labelloc = "t"; + labeljust = "l"; + style = "filled"; + color = "white" + cic_unification; + tactics; + grafite; + grafite_engine; + } + subgraph cluster_fully { + label = "Fully specified terms"; + labelloc = "b"; + labeljust = "l"; + style = "filled"; + color = "white" + cic; + cic_proof_checking; + getter; + metadata; + urimanager; + whelp; + library; + cic_acic; + } + subgraph cluster_utilities { + label = "Utilities"; + labelloc = "b"; + labeljust = "r"; + style = "filled"; + color = "white" + extlib; + hgdome; + hmysql; + registry; + utf8_macros; + xml; + logger; + } diff --git a/helm/ocaml/STATS/daemons.dot b/helm/ocaml/STATS/daemons.dot new file mode 100644 index 000000000..4a8ba388f --- /dev/null +++ b/helm/ocaml/STATS/daemons.dot @@ -0,0 +1,19 @@ + /* apps */ + subgraph applications { + node [shape=plaintext,style=filled,fillcolor=slategray2]; + DependencyAnalyzer [label="Dependency\nAnalyzer\n .3 klocs"]; + Getter [label="Getter\n .3 klocs"]; + Matita [label="Matita\n 6.7 klocs"]; + ProofChecker [label="Proof Checker\n .1 klocs"]; + Uwobo [label="Uwobo\n 2.1 klocs"]; + Whelp [label="Whelp\n .6 klocs"]; + } + /* apps dep */ + DependencyAnalyzer -> metadata; + Getter -> getter; + Matita -> grafite_engine; + Matita -> grafite_parser; + Matita -> hgdome; + ProofChecker -> cic_proof_checking; + Uwobo -> content_pres; + Whelp -> grafite_parser; diff --git a/helm/ocaml/STATS/deps.patch b/helm/ocaml/STATS/deps.patch new file mode 100644 index 000000000..90130dfe8 --- /dev/null +++ b/helm/ocaml/STATS/deps.patch @@ -0,0 +1,23 @@ +--- .clustersdep.dot 2006-01-26 10:10:46.000000000 +0100 ++++ .clustersdep.new 2006-01-26 10:10:44.000000000 +0100 +@@ -1,11 +1,8 @@ + digraph G { + xml [label="xml\n.5 klocs"]; +- xmldiff [label="xmldiff\n.3 klocs"]; + whelp [label="whelp\n.3 klocs"]; + utf8_macros [label="utf8_macros\n.2 klocs"]; + urimanager [label="urimanager\n.2 klocs"]; +- thread [label="thread\n.2 klocs"]; +- paramodulation [label="paramodulation\n5.9 klocs"]; + tactics [label="tactics\n10.0 klocs"]; + registry [label="registry\n.6 klocs"]; + metadata [label="metadata\n1.9 klocs"]; +@@ -42,7 +39,7 @@ + "cic_unification" -> "library"; + "library" -> "metadata"; + "library" -> "cic_acic"; +-"metadata" -> "cic_proof_checking"; ++"metadata" -> "cic"; + "metadata" -> "hmysql"; + "grafite" -> "cic"; + "content_pres" -> "utf8_macros"; diff --git a/helm/ocaml/STATS/patch_deps.sh b/helm/ocaml/STATS/patch_deps.sh new file mode 100755 index 000000000..d7dd7b3ba --- /dev/null +++ b/helm/ocaml/STATS/patch_deps.sh @@ -0,0 +1,53 @@ +#!/bin/sh +# script args: source_file target_file + +use_clusters='no' +if [ ! -z "$USE_CLUSTERS" ]; then + use_clusters=$USE_CLUSTERS +fi + +# args: file snippet +# file will be modified in place +include_dot_snippet () +{ + echo "Adding to $1 graphviz snippet $2 ..." + sed -i "/digraph/r $2" $1 +} + +# args: stats file +# file will be modified in place +include_loc_stats () +{ + echo "Adding to $1 KLOCs stats from $2 ..." + tmp=`mktemp tmp.stats.XXXXXX` + for l in `cat $2`; do + module=$(basename $(echo $l | cut -d : -f 1)) + stat=$(echo $l | cut -d : -f 2) + if [ "$stat" = "LOC" ]; then + locs=$(echo $l | cut -d : -f 3) + klocs=$(echo "scale=1; $locs / 1000" | bc) + if [ "$klocs" = "0" ]; then klocs=".1"; fi + printf ' %s [label="%s\\n%s klocs"];\n' $module $module $klocs >> $tmp + fi + done + include_dot_snippet $1 $tmp + rm $tmp +} + +# args: file patch +apply_patch () +{ + if [ -f "$2" ]; then + echo "Applying to $1 patch $2 ..." + patch $1 $2 + fi +} + +cp $1 $2 +include_loc_stats $2 .stats +apply_patch $2 STATS/deps.patch +include_dot_snippet $2 STATS/daemons.dot +if [ "$use_clusters" = "yes" ]; then + include_dot_snippet $2 STATS/clusters.dot +fi + diff --git a/helm/ocaml/clusters.dot b/helm/ocaml/clusters.dot deleted file mode 100644 index b7298bce8..000000000 --- a/helm/ocaml/clusters.dot +++ /dev/null @@ -1,57 +0,0 @@ -// 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_disambiguation; - content_pres; - grafite_parser; - lexicon; - } - subgraph cluster_partially { - label = "Partially specified terms"; - labelloc = "t"; - labeljust = "l"; - style = "filled"; - color = "white" - cic_unification; - tactics; - grafite; - grafite_engine; - } - subgraph cluster_fully { - label = "Fully specified terms"; - labelloc = "b"; - labeljust = "l"; - style = "filled"; - color = "white" - cic; - cic_proof_checking; - getter; - metadata; - urimanager; - whelp; - library; - cic_acic; - } - subgraph cluster_utilities { - label = "Utilities"; - labelloc = "b"; - labeljust = "r"; - style = "filled"; - color = "white" - extlib; - hgdome; - hmysql; - registry; - utf8_macros; - xml; - logger; - } diff --git a/helm/ocaml/daemons.dot b/helm/ocaml/daemons.dot deleted file mode 100644 index 4a8ba388f..000000000 --- a/helm/ocaml/daemons.dot +++ /dev/null @@ -1,19 +0,0 @@ - /* apps */ - subgraph applications { - node [shape=plaintext,style=filled,fillcolor=slategray2]; - DependencyAnalyzer [label="Dependency\nAnalyzer\n .3 klocs"]; - Getter [label="Getter\n .3 klocs"]; - Matita [label="Matita\n 6.7 klocs"]; - ProofChecker [label="Proof Checker\n .1 klocs"]; - Uwobo [label="Uwobo\n 2.1 klocs"]; - Whelp [label="Whelp\n .6 klocs"]; - } - /* apps dep */ - DependencyAnalyzer -> metadata; - Getter -> getter; - Matita -> grafite_engine; - Matita -> grafite_parser; - Matita -> hgdome; - ProofChecker -> cic_proof_checking; - Uwobo -> content_pres; - Whelp -> grafite_parser; diff --git a/helm/ocaml/deps.patch b/helm/ocaml/deps.patch deleted file mode 100644 index 90130dfe8..000000000 --- a/helm/ocaml/deps.patch +++ /dev/null @@ -1,23 +0,0 @@ ---- .clustersdep.dot 2006-01-26 10:10:46.000000000 +0100 -+++ .clustersdep.new 2006-01-26 10:10:44.000000000 +0100 -@@ -1,11 +1,8 @@ - digraph G { - xml [label="xml\n.5 klocs"]; -- xmldiff [label="xmldiff\n.3 klocs"]; - whelp [label="whelp\n.3 klocs"]; - utf8_macros [label="utf8_macros\n.2 klocs"]; - urimanager [label="urimanager\n.2 klocs"]; -- thread [label="thread\n.2 klocs"]; -- paramodulation [label="paramodulation\n5.9 klocs"]; - tactics [label="tactics\n10.0 klocs"]; - registry [label="registry\n.6 klocs"]; - metadata [label="metadata\n1.9 klocs"]; -@@ -42,7 +39,7 @@ - "cic_unification" -> "library"; - "library" -> "metadata"; - "library" -> "cic_acic"; --"metadata" -> "cic_proof_checking"; -+"metadata" -> "cic"; - "metadata" -> "hmysql"; - "grafite" -> "cic"; - "content_pres" -> "utf8_macros"; diff --git a/helm/ocaml/patch_deps.sh b/helm/ocaml/patch_deps.sh deleted file mode 100755 index dbdd27c11..000000000 --- a/helm/ocaml/patch_deps.sh +++ /dev/null @@ -1,53 +0,0 @@ -#!/bin/sh -# script args: source_file target_file - -use_clusters='no' -if [ ! -z "$USE_CLUSTERS" ]; then - use_clusters=$USE_CLUSTERS -fi - -# args: file snippet -# file will be modified in place -include_dot_snippet () -{ - echo "Adding to $1 graphviz snippet $2 ..." - sed -i "/digraph/r $2" $1 -} - -# args: stats file -# file will be modified in place -include_loc_stats () -{ - echo "Adding to $1 KLOCs stats from $2 ..." - tmp=`mktemp tmp.stats.XXXXXX` - for l in `cat $2`; do - module=$(basename $(echo $l | cut -d : -f 1)) - stat=$(echo $l | cut -d : -f 2) - if [ "$stat" = "LOC" ]; then - locs=$(echo $l | cut -d : -f 3) - klocs=$(echo "scale=1; $locs / 1000" | bc) - if [ "$klocs" = "0" ]; then klocs=".1"; fi - printf ' %s [label="%s\\n%s klocs"];\n' $module $module $klocs >> $tmp - fi - done - include_dot_snippet $1 $tmp - rm $tmp -} - -# args: file patch -apply_patch () -{ - if [ -f "$2" ]; then - echo "Applying to $1 patch $2 ..." - patch $1 $2 - fi -} - -cp $1 $2 -include_loc_stats $2 .stats -apply_patch $2 deps.patch -include_dot_snippet $2 daemons.dot -if [ "$use_clusters" = "yes" ]; then - include_dot_snippet $2 clusters.dot -fi -