4 INTERFACE_FILES= parser.mli parserTHF.mli tptp2grafite.mli
6 IMPLEMENTATION_FILES = ast.ml lexer.ml astTHF.ml lexerTHF.ml $(INTERFACE_FILES:%.mli=%.ml)
7 EXTRA_OBJECTS_TO_INSTALL =
8 EXTRA_OBJECTS_TO_CLEAN =
10 TPTPDIR= /home/$(USER)/work-area/TPTP-v4.0.1/
12 all: tptp2grafite mainTHF
13 clean: clean_tests clean_generated
16 rm -f parser.mli parser.ml parserTHF.mli parserTHF.ml
17 rm -f lexer.ml lexerTHF.ml
24 lexerTHF.cmo: parserTHF.cmi
25 lexerTHF.cmx: parserTHF.cmi
32 LOCAL_LINKOPTS = -package helm-$(PACKAGE) -linkpkg
33 tptp2grafite: main.ml tptp_grafite.cma
35 @$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
37 mainTHF: mainTHF.ml tptp_grafite.cma
39 @$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
41 test: tptp2grafite mainTHF
44 for X in `cat unit_equality_problems`; do\
45 cat $(TPTPDIR)/$$X | ./tptp2grafite || echo ERROR PARSING $$X;\
49 for X in `cat $*`; do\
50 ./tptp2grafite -tptppath $(TPTPDIR) $$X.p \
51 > ../../matita/tests/TPTP/$$X.ma || echo Failed: $$X; \
55 for X in `cat $*`; do\
56 ./tptp2grafite -ng -tptppath $(TPTPDIR) $$X.p \
57 > ../../matita/contribs/ng_TPTP/$$X.ma || echo Failed: $$X; \
61 for X in `cat $*`; do\
63 ./tptp2grafite -tptppath $(TPTPDIR) $$X.p \
64 > /dev/null || echo Failed: $$X; \
70 for x in `cat thf_problems`; do\
72 ./mainTHF -tptppath $(TPTPDIR) $$x.p > THF/$$x.ma;\
75 include ../../Makefile.defs
76 include ../Makefile.common