+
+export SHELL=/bin/bash
+
# Warning: the modules must be in compilation order
NULL =
MODULES = \
lexicon \
grafite_engine \
grafite_parser \
- tactics/paramodulation \
+ tactics/paramodulation \
$(NULL)
OCAMLFIND_DEST_DIR = @OCAMLFIND_DEST_DIR@
(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
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 $@ $<
--- /dev/null
+// 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;
+ }
--- /dev/null
+ /* 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;
--- /dev/null
+--- .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";
--- /dev/null
+#!/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
+
+++ /dev/null
-// 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;
- }
+++ /dev/null
- /* 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;
+++ /dev/null
---- .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";
+++ /dev/null
-#!/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
-
projects / helm.git / commitdiff