X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftptp_grafite%2FMakefile;h=e452480d8430ec07a2d6b919628c563e49f55e9e;hb=e62111335574a6ec78e5a4367a540e0529a00404;hp=1e239837307960cb4c778766d5500ea0597dde25;hpb=fedecee9c4b10a2469c10fe09ec091d2dc6fc56a;p=helm.git

diff --git a/helm/software/components/tptp_grafite/Makefile b/helm/software/components/tptp_grafite/Makefile
index 1e2398373..e452480d8 100644
--- a/helm/software/components/tptp_grafite/Makefile
+++ b/helm/software/components/tptp_grafite/Makefile
@@ -7,14 +7,23 @@ IMPLEMENTATION_FILES = ast.ml lexer.ml astTHF.ml lexerTHF.ml $(INTERFACE_FILES:%
 EXTRA_OBJECTS_TO_INSTALL = 
 EXTRA_OBJECTS_TO_CLEAN =
 
-TPTPDIR= /home/$(USER)/work-area/TPTP-v3.2.0/
+TPTPDIR= /home/$(USER)/work-area/TPTP-v4.0.1/
 
 all: tptp2grafite mainTHF
-clean: clean_tests
+clean: clean_tests clean_generated
+
+clean_generated:
+	rm -f parser.mli parser.ml parserTHF.mli parserTHF.ml 
+	rm -f lexer.ml lexerTHF.ml
 
 clean_tests:
 	rm -f tptp2grafite
 
+lexer.cmo: parser.cmi
+lexer.cmx: parser.cmi
+lexerTHF.cmo: parserTHF.cmi
+lexerTHF.cmx: parserTHF.cmi
+
 %.mli %.ml: %.mly
 	ocamlyacc $*.mly
 %.ml:%.mll
@@ -55,6 +64,14 @@ parse-%:
 		> /dev/null || echo Failed: $$X; \
 	done
 
+thf:
+	rm -rf THF
+	mkdir THF
+	for x in `cat thf_problems`; do\
+		echo $$x;\
+		./mainTHF -tptppath $(TPTPDIR) $$x.p > THF/$$x.ma;\
+	done
+
 include ../../Makefile.defs
 include ../Makefile.common