]> 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 54a2f1d1660d48d405f75bba3064a32fde5c2427..7ea740bc6430e4a4017d9e09720f12791c5060d0 100644 (file)
@@ -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
@@ -59,6 +59,8 @@ gTopLevel.opt: $(TOPLEVELOBJS:.cmo=.cmx) $(LIBRARIES_OPT)
 
 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)
@@ -91,10 +93,12 @@ cleantest:
        rm -f $(OUTTESTS)
 tests/%.cic.test: tests/%.cic regtest
        time ./regtest -gen $<
-test:
+test: regtest
        ./regtest $(INTESTS) 2> /dev/null
-envtest:
+envtest: regtest
        ./regtest -dump $(INTESTS) 2> /dev/null
+librarytest: testlibrary.opt
+       ./testlibrary.opt - <index.txt 2>/dev/null >LOG &
 
 ifneq ($(MAKECMDGOALS), depend)
    include .depend