X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FMakefile;h=abe03e42deea4548ab18076141e04d2f86a318cc;hb=f4b9cc6f689b52e0408ac3231ba2a480d71216fb;hp=bcf0b74ff0500dae449d09a1418889038730b7a2;hpb=12809955a4a6c693072f5b924603165f83cc382e;p=helm.git diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index bcf0b74ff..abe03e42d 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -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 -opt: styles gTopLevel.opt +all: styles gTopLevel regtest +opt: styles gTopLevel.opt regtest.opt start: $(MAKE) -C ../hbugs/ start @@ -23,13 +23,17 @@ stop: INTERFACE_FILES = \ proofEngine.mli logicalOperations.mli oldDisambiguate.mli \ - disambiguatingParser.mli termEditor.mli xmlDiff.mli chosenTransformer.mli \ - termViewer.mli invokeTactics.mli hbugs.mli chosenTermEditor.mli -# texTermEditor.mli + disambiguatingParser.mli termEditor.mli texTermEditor.mli xmlDiff.mli \ + chosenTransformer.mli termViewer.mli invokeTactics.mli hbugs.mli \ + chosenTermEditor.mli -DEPOBJS = $(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.ml) gTopLevel.ml +DEPOBJS = \ + $(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.ml) \ + gTopLevel.ml regtest.ml batchParser.ml batchParser.mli TOPLEVELOBJS = $(INTERFACE_FILES:%.mli=%.cmo) gTopLevel.cmo +REGTESTOBJS = \ + $(INTERFACE_FILES:%.mli=%.cmo) batchParser.cmo regtest.cmo $(INTERFACE_FILES:%.mli=%.cmo): $(LIBRARIES) $(INTERFACE_FILES:%.mli=%.cmx): $(LIBRARIES_OPT) @@ -47,10 +51,14 @@ depend: $(OCAMLDEP) $(DEPOBJS) > .depend gTopLevel: $(TOPLEVELOBJS) $(LIBRARIES) - $(OCAMLC) -linkpkg -o gTopLevel $(TOPLEVELOBJS) - + $(OCAMLC) -linkpkg -o $@ $(TOPLEVELOBJS) gTopLevel.opt: $(TOPLEVELOBJS:.cmo=.cmx) $(LIBRARIES_OPT) - $(OCAMLOPT) -linkpkg -o gTopLevel.opt $(TOPLEVELOBJS:.cmo=.cmx) + $(OCAMLOPT) -linkpkg -o $@ $(TOPLEVELOBJS:.cmo=.cmx) + +regtest: $(REGTESTOBJS) $(LIBRARIES) + $(OCAMLC) -linkpkg -o $@ $(REGTESTOBJS) +regtest.opt: $(REGTESTOBJS:.cmo=.cmx) $(LIBRARIES) + $(OCAMLOPT) -linkpkg -o $@ $(REGTESTOBJS:.cmo=.cmx) .SUFFIXES: .ml .mli .cmo .cmi .cmx .ml.cmo: @@ -64,15 +72,20 @@ $(TOPLEVELOBJS): $(LIBRARIES) $(TOPLEVELOBJS:.cmo=.cmx)): $(LIBRARIES_OPT) clean: - rm -f *.cm[iox] *.o gTopLevel gTopLevel.opt - + rm -f *.cm[iox] *.o gTopLevel{,.opt} regtest{,.opt} install: cp gTopLevel gTopLevel.opt $(BIN_DIR) - uninstall: rm -f $(BIN_DIR)/gTopLevel $(BIN_DIR)/gTopLevel.opt -.PHONY: install uninstall clean +.PHONY: install uninstall clean test + +TESTS := $(patsubst %, %.test, $(wildcard tests/*.cic)) +gentest: $(TESTS) +tests/%.cic.test: tests/%.cic + ./regtest -gen $< +test: + ./regtest $(TESTS) ifneq ($(MAKECMDGOALS), depend) include .depend