META files are now automatically generated from META-*.src files.

In this way all the hard-coded file paths have been removed.
Installation and uninstallation (still not implemented) should be also
easier.
Moreover, an error in a sub-directory now stops the whole processing.

diff --git a/helm/ocaml/.cvsignore b/helm/ocaml/.cvsignore
new file mode 100644 (file)
index 0000000..68dd36d
--- /dev/null
+++ b/helm/ocaml/.cvsignore
@@ -0,0 +1 @@
+META.helm-cic META.helm-getter META.helm-cic_annotations META.helm-pxp META.helm-cic_annotations_cache META.helm-urimanager META.helm-cic_cache META.helm-xml META.helm-cic_proof_checking

diff --git a/helm/ocaml/META.helm-cic b/helm/ocaml/META.helm-cic
deleted file mode 100644 (file)
index 4fcb705..0000000
--- a/helm/ocaml/META.helm-cic
+++ /dev/null
@@ -1,6 +0,0 @@
-requires="helm-urimanager helm-pxp"
-version="0.0.1"
-archive(byte)="cic.cma"
-archive(native)="cic.cmxa"
-linkopts=""
-directory="/home/sacerdot/miohelm/helm/ocaml/cic"

diff --git a/helm/ocaml/META.helm-cic.src b/helm/ocaml/META.helm-cic.src
new file mode 100644 (file)
index 0000000..ee898d8
--- /dev/null
+++ b/helm/ocaml/META.helm-cic.src
@@ -0,0 +1,5 @@
+requires="helm-urimanager helm-pxp"
+version="0.0.1"
+archive(byte)="cic.cma"
+archive(native)="cic.cmxa"
+linkopts=""

diff --git a/helm/ocaml/META.helm-cic_annotations b/helm/ocaml/META.helm-cic_annotations
deleted file mode 100644 (file)
index db13618..0000000
--- a/helm/ocaml/META.helm-cic_annotations
+++ /dev/null
@@ -1,6 +0,0 @@
-requires="helm-cic helm-xml lablgtk"
-version="0.0.1"
-archive(byte)="cic_annotations.cma"
-archive(native)="cic_annotations.cmxa"
-linkopts=""
-directory="/home/sacerdot/miohelm/helm/ocaml/cic_annotations"

diff --git a/helm/ocaml/META.helm-cic_annotations.src b/helm/ocaml/META.helm-cic_annotations.src
new file mode 100644 (file)
index 0000000..ec5462f
--- /dev/null
+++ b/helm/ocaml/META.helm-cic_annotations.src
@@ -0,0 +1,5 @@
+requires="helm-cic helm-xml lablgtk"
+version="0.0.1"
+archive(byte)="cic_annotations.cma"
+archive(native)="cic_annotations.cmxa"
+linkopts=""

diff --git a/helm/ocaml/META.helm-cic_annotations_cache b/helm/ocaml/META.helm-cic_annotations_cache
deleted file mode 100644 (file)
index 5065413..0000000
--- a/helm/ocaml/META.helm-cic_annotations_cache
+++ /dev/null
@@ -1,6 +0,0 @@
-requires="helm-cic_annotations"
-version="0.0.1"
-archive(byte)="cic_annotations_cache.cma"
-archive(native)="cic_annotations_cache.cmxa"
-linkopts=""
-directory="/home/sacerdot/miohelm/helm/ocaml/cic_annotations_cache"

diff --git a/helm/ocaml/META.helm-cic_annotations_cache.src b/helm/ocaml/META.helm-cic_annotations_cache.src
new file mode 100644 (file)
index 0000000..38f5d1d
--- /dev/null
+++ b/helm/ocaml/META.helm-cic_annotations_cache.src
@@ -0,0 +1,5 @@
+requires="helm-cic_annotations"
+version="0.0.1"
+archive(byte)="cic_annotations_cache.cma"
+archive(native)="cic_annotations_cache.cmxa"
+linkopts=""

diff --git a/helm/ocaml/META.helm-cic_cache b/helm/ocaml/META.helm-cic_cache
deleted file mode 100644 (file)
index 0b6b4e6..0000000
--- a/helm/ocaml/META.helm-cic_cache
+++ /dev/null
@@ -1,6 +0,0 @@
-requires="helm-cic"
-version="0.0.1"
-archive(byte)="cic_cache.cma"
-archive(native)="cic_cache.cmxa"
-linkopts=""
-directory="/home/sacerdot/miohelm/helm/ocaml/cic_cache"

diff --git a/helm/ocaml/META.helm-cic_cache.src b/helm/ocaml/META.helm-cic_cache.src
new file mode 100644 (file)
index 0000000..28ea57e
--- /dev/null
+++ b/helm/ocaml/META.helm-cic_cache.src
@@ -0,0 +1,5 @@
+requires="helm-cic"
+version="0.0.1"
+archive(byte)="cic_cache.cma"
+archive(native)="cic_cache.cmxa"
+linkopts=""

diff --git a/helm/ocaml/META.helm-cic_proof_checking b/helm/ocaml/META.helm-cic_proof_checking
deleted file mode 100644 (file)
index 59657d3..0000000
--- a/helm/ocaml/META.helm-cic_proof_checking
+++ /dev/null
@@ -1,8 +0,0 @@
-requires="helm-cic"
-version="0.0.1"
-archive(byte)="cic_proof_checking.cma"
-archive(native)="cic_proof_checking.cmxa"
-archive(byte,miniReduction)="cicSubstitution.cmo cicMiniReduction.cmo"
-archive(native,miniReduction)="cicSubstitution.cmx cicMiniReduction.cmx"
-linkopts=""
-directory="/home/sacerdot/miohelm/helm/ocaml/cic_proof_checking"

diff --git a/helm/ocaml/META.helm-cic_proof_checking.src b/helm/ocaml/META.helm-cic_proof_checking.src
new file mode 100644 (file)
index 0000000..08b099e
--- /dev/null
+++ b/helm/ocaml/META.helm-cic_proof_checking.src
@@ -0,0 +1,7 @@
+requires="helm-cic"
+version="0.0.1"
+archive(byte)="cic_proof_checking.cma"
+archive(native)="cic_proof_checking.cmxa"
+archive(byte,miniReduction)="cicSubstitution.cmo cicMiniReduction.cmo"
+archive(native,miniReduction)="cicSubstitution.cmx cicMiniReduction.cmx"
+linkopts=""

diff --git a/helm/ocaml/META.helm-getter b/helm/ocaml/META.helm-getter
deleted file mode 100644 (file)
index 088aa3b..0000000
--- a/helm/ocaml/META.helm-getter
+++ /dev/null
@@ -1,6 +0,0 @@
-requires="helm-urimanager pxp netclient"
-version="0.0.1"
-archive(byte)="getter.cma"
-archive(native)="getter.cmxa"
-linkopts=""
-directory="/home/sacerdot/miohelm/helm/ocaml/getter"

diff --git a/helm/ocaml/META.helm-getter.src b/helm/ocaml/META.helm-getter.src
new file mode 100644 (file)
index 0000000..8ba941f
--- /dev/null
+++ b/helm/ocaml/META.helm-getter.src
@@ -0,0 +1,5 @@
+requires="helm-urimanager pxp netclient"
+version="0.0.1"
+archive(byte)="getter.cma"
+archive(native)="getter.cmxa"
+linkopts=""

diff --git a/helm/ocaml/META.helm-pxp b/helm/ocaml/META.helm-pxp
deleted file mode 100644 (file)
index 68bdbf2..0000000
--- a/helm/ocaml/META.helm-pxp
+++ /dev/null
@@ -1,6 +0,0 @@
-requires="helm-getter"
-version="0.0.1"
-archive(byte)="pxp.cma"
-archive(native)="pxp.cmxa"
-linkopts=""
-directory="/home/sacerdot/miohelm/helm/ocaml/pxp"

diff --git a/helm/ocaml/META.helm-pxp.src b/helm/ocaml/META.helm-pxp.src
new file mode 100644 (file)
index 0000000..33210a7
--- /dev/null
+++ b/helm/ocaml/META.helm-pxp.src
@@ -0,0 +1,5 @@
+requires="helm-getter"
+version="0.0.1"
+archive(byte)="pxp.cma"
+archive(native)="pxp.cmxa"
+linkopts=""

diff --git a/helm/ocaml/META.helm-urimanager b/helm/ocaml/META.helm-urimanager
deleted file mode 100644 (file)
index 805f9f1..0000000
--- a/helm/ocaml/META.helm-urimanager
+++ /dev/null
@@ -1,6 +0,0 @@
-requires="str"
-version="0.0.1"
-archive(byte)="urimanager.cma"
-archive(native)="urimanager.cmxa"
-linkopts=""
-directory="/home/sacerdot/miohelm/helm/ocaml/urimanager"

diff --git a/helm/ocaml/META.helm-urimanager.src b/helm/ocaml/META.helm-urimanager.src
new file mode 100644 (file)
index 0000000..ff18746
--- /dev/null
+++ b/helm/ocaml/META.helm-urimanager.src
@@ -0,0 +1,5 @@
+requires="str"
+version="0.0.1"
+archive(byte)="urimanager.cma"
+archive(native)="urimanager.cmxa"
+linkopts=""

diff --git a/helm/ocaml/META.helm-xml b/helm/ocaml/META.helm-xml
deleted file mode 100644 (file)
index 7f59db4..0000000
--- a/helm/ocaml/META.helm-xml
+++ /dev/null
@@ -1,6 +0,0 @@
-requires=""
-version="0.0.1"
-archive(byte)="xml.cma"
-archive(native)="xml.cmxa"
-linkopts=""
-directory="/home/sacerdot/miohelm/helm/ocaml/xml"

diff --git a/helm/ocaml/META.helm-xml.src b/helm/ocaml/META.helm-xml.src
new file mode 100644 (file)
index 0000000..1cd68fe
--- /dev/null
+++ b/helm/ocaml/META.helm-xml.src
@@ -0,0 +1,5 @@
+requires=""
+version="0.0.1"
+archive(byte)="xml.cma"
+archive(native)="xml.cmxa"
+linkopts=""

diff --git a/helm/ocaml/Makefile b/helm/ocaml/Makefile
index e488c640136557294c234b60aa727e34f02fdb64..d983eea74dc2125fcdfcfd45fdeaeb492542e560 100644 (file)
--- a/helm/ocaml/Makefile
+++ b/helm/ocaml/Makefile
@@ -1,6 +1,31 @@
 # Warning: the modules must be in compilation order
-MODULES= xml urimanager getter pxp cic cic_annotations cic_annotations_cache \
-         cic_cache cic_proof_checking
+MODULES = xml urimanager getter pxp cic cic_annotations cic_annotations_cache \
+          cic_cache cic_proof_checking
 
-all opt depend install uninstall clean:
-       for i in $(MODULES) ; do (cd $$i ; make $@) ; done
+METAS = $(MODULES:%=META.helm-%)
+CWD=`pwd`
+
+all: $(METAS) $(MODULES:%=%.all)
+opt: $(METAS) $(MODULES:%=%.opt)
+depend: $(MODULES:%=%.depend)
+install: $(MODULES:%=%.install)
+uninstall: $(MODULES:%=%.uninstall)
+clean: $(MODULES:%=%.clean)
+       rm -f $(METAS)
+
+$(MODULES:%=%.all):
+       export OCAMLPATH=$(CWD):$$OCAMLPATH ; cd $(@:%.all=%) ; make all
+$(MODULES:%=%.opt):
+       export OCAMLPATH=$(CWD):$$OCAMLPATH ; cd $(@:%.opt=%) ; make opt
+$(MODULES:%=%.depend):
+       export OCAMLPATH=$(CWD):$$OCAMLPATH ; cd $(@:%.depend=%) ; make depend
+$(MODULES:%=%.install):
+       cd $(@:%.install=%) ; make install
+$(MODULES:%=%.uninstall):
+       cd $(@:%.uninstall=%) ; make uninstall
+$(MODULES:%=%.clean):
+       cd $(@:%.clean=%) ; make clean
+$(MODULES:%=META.helm-%):
+       cp $@.src $@ ; echo "directory=\"$(CWD)/$(@:META.helm-%=%)\"" >> $@
+META.helm-%: META.helm-%.src
+       cp $< $@ ; echo "directory=\"$(CWD)/$(@:META.helm-%=%)\"" >> $@