Release 0.5.9.

[helm.git] / helm / software / components / tptp_grafite / Makefile

diff --git a/helm/software/components/tptp_grafite/Makefile b/helm/software/components/tptp_grafite/Makefile
index e452480d8430ec07a2d6b919628c563e49f55e9e..c196dd609e418ccd733d2f51b8a00da848ae3a5b 100644 (file)
--- a/helm/software/components/tptp_grafite/Makefile
+++ b/helm/software/components/tptp_grafite/Makefile
@@ -1,44 +1,31 @@
 PACKAGE = tptp_grafite
 PREDICATES = 
 
-INTERFACE_FILES= parser.mli parserTHF.mli tptp2grafite.mli
+INTERFACE_FILES= parser.mli tptp2grafite.mli
 
-IMPLEMENTATION_FILES = ast.ml lexer.ml astTHF.ml lexerTHF.ml $(INTERFACE_FILES:%.mli=%.ml)
+IMPLEMENTATION_FILES = ast.ml lexer.ml $(INTERFACE_FILES:%.mli=%.ml)
 EXTRA_OBJECTS_TO_INSTALL = 
 EXTRA_OBJECTS_TO_CLEAN =
 
-TPTPDIR= /home/$(USER)/work-area/TPTP-v4.0.1/
+TPTPDIR= /home/$(USER)/work-area/TPTP-v3.2.0/
 
-all: tptp2grafite mainTHF
-clean: clean_tests clean_generated
-
-clean_generated:
-       rm -f parser.mli parser.ml parserTHF.mli parserTHF.ml 
-       rm -f lexer.ml lexerTHF.ml
+all: tptp2grafite
+clean: clean_tests
 
 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
-       ocamllex $*.mll
+parser.mli parser.ml:parser.mly
+       ocamlyacc parser.mly
+lexer.ml:
+       ocamllex lexer.mll
 
 LOCAL_LINKOPTS = -package helm-$(PACKAGE) -linkpkg
 tptp2grafite: main.ml tptp_grafite.cma
        @echo "  OCAMLC $<"
        @$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
 
-mainTHF: mainTHF.ml tptp_grafite.cma 
-       @echo "  OCAMLC $<"
-       @$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
-
-test: tptp2grafite mainTHF
+test: tptp2grafite
 
 testall: tptp2grafite
        for X in `cat unit_equality_problems`; do\
@@ -64,14 +51,6 @@ 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