]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/Makefile
New target librarytest (to apply testlibrary.opt to index.txt). The output
[helm.git] / helm / gTopLevel / Makefile
index d668434534736a4119bad4414da72a32b43977d5..7ea740bc6430e4a4017d9e09720f12791c5060d0 100644 (file)
@@ -1,8 +1,8 @@
 BIN_DIR = /usr/local/bin
 REQUIRES = lablgtkmathview helm-cic_textual_parser helm-tex_cic_textual_parser \
            gdome2-xslt helm-mathql_interpreter helm-mathql_generator \
-                          helm-tactics hbugs-client mathml-editor helm-cic_transformations \
-           helm-cic_textual_parser2
+          helm-tactics hbugs-client mathml-editor helm-cic_transformations \
+           helm-cic_textual_parser2 helm-cic_cache
 PREDICATES = "gnome,init,glade"
 OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o
 OCAMLFIND = ocamlfind
@@ -13,8 +13,8 @@ OCAMLDEP = ocamldep -pp camlp4o
 LIBRARIES = $(shell $(OCAMLFIND) query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES))
 LIBRARIES_OPT = $(shell $(OCAMLFIND) query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES))
 
-all: styles gTopLevel regtest
-opt: styles gTopLevel.opt regtest.opt
+all: styles gTopLevel
+opt: styles gTopLevel.opt
 
 start:
        $(MAKE) -C ../hbugs/ start
@@ -29,11 +29,13 @@ INTERFACE_FILES = \
 
 DEPOBJS = \
        $(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.ml) \
-       gTopLevel.ml regtest.ml batchParser.ml batchParser.mli
+       gTopLevel.ml regtest.ml testlibrary.ml batchParser.ml batchParser.mli
 
 TOPLEVELOBJS = $(INTERFACE_FILES:%.mli=%.cmo) gTopLevel.cmo
 REGTESTOBJS = \
        $(INTERFACE_FILES:%.mli=%.cmo) batchParser.cmo regtest.cmo
+TESTLIBOBJS = \
+       $(INTERFACE_FILES:%.mli=%.cmo) testlibrary.cmo
 
 $(INTERFACE_FILES:%.mli=%.cmo): $(LIBRARIES)
 $(INTERFACE_FILES:%.mli=%.cmx): $(LIBRARIES_OPT)
@@ -55,6 +57,10 @@ gTopLevel: $(TOPLEVELOBJS) $(LIBRARIES)
 gTopLevel.opt: $(TOPLEVELOBJS:.cmo=.cmx) $(LIBRARIES_OPT)
        $(OCAMLOPT) -linkpkg -o $@ $(TOPLEVELOBJS:.cmo=.cmx)
 
+testlibrary: $(TESTLIBOBJS) $(LIBRARIES)
+       $(OCAMLC) -linkpkg -o $@ $(TESTLIBOBJS)
+testlibrary.opt: $(TESTLIBOBJS:.cmo=.cmx) $(LIBRARIES)
+       $(OCAMLOPT) -linkpkg -o $@ $(TESTLIBOBJS:.cmo=.cmx)
 regtest: $(REGTESTOBJS) $(LIBRARIES)
        $(OCAMLC) -linkpkg -o $@ $(REGTESTOBJS)
 regtest.opt: $(REGTESTOBJS:.cmo=.cmx) $(LIBRARIES)
@@ -80,14 +86,19 @@ uninstall:
 
 .PHONY: install uninstall clean test
 
-TESTS := $(patsubst %, %.test, $(wildcard tests/*.cic))
-gentest: $(TESTS)
+INTESTS := $(wildcard tests/*.cic)
+OUTTESTS := $(patsubst %, %.test, $(INTESTS))
+gentest: $(OUTTESTS)
 cleantest:
-       rm -f $(TESTS)
-tests/%.cic.test: tests/%.cic
+       rm -f $(OUTTESTS)
+tests/%.cic.test: tests/%.cic regtest
        time ./regtest -gen $<
-test:
-       time ./regtest $(TESTS)
+test: regtest
+       ./regtest $(INTESTS) 2> /dev/null
+envtest: regtest
+       ./regtest -dump $(INTESTS) 2> /dev/null
+librarytest: testlibrary.opt
+       ./testlibrary.opt - <index.txt 2>/dev/null >LOG &
 
 ifneq ($(MAKECMDGOALS), depend)
    include .depend