]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/binaries/tptp2grafite/Makefile
fixed some pp stuff
[helm.git] / helm / software / components / binaries / tptp2grafite / Makefile
index e96134e5d22449008767ef0fca95a291ea22ebf0..c8ea0ebf2f00858592a090117b057ba977b195dd 100644 (file)
@@ -1,19 +1,26 @@
-all: tptp2grafite
+OCAMLC = OCAMLPATH=../../METAS ocamlfind ocamlc -package helm-grafite_parser
+TPTPDIR=/home/tassi/helm/trunk/TPTP-v3.1.1/
+
+opt all: tptp2grafite
+       echo -n
 
 tptp2grafite: ast.ml parser.mly lexer.mll main.ml
-       ocamlc -c ast.ml
+       $(OCAMLC) -c ast.ml
        ocamlyacc parser.mly
-       ocamlc -c parser.mli
-       ocamlc -c parser.ml
+       $(OCAMLC) -c parser.mli
+       $(OCAMLC) -c parser.ml
        ocamllex lexer.mll
-       ocamlc -c lexer.ml
-       ocamlc -c main.ml
-       ocamlc -o tptp2grafite ast.cmo lexer.cmo parser.cmo main.cmo
+       $(OCAMLC) -c lexer.ml
+       $(OCAMLC) -c main.ml
+       $(OCAMLC) -linkpkg -o tptp2grafite ast.cmo lexer.cmo parser.cmo main.cmo
 
 clean:
        rm -f tptp2grafite *.cmo *.cmi parser.mli parser.ml lexer.ml rm *.output
 
 test: tptp2grafite
+       cat $(TPTPDIR)/`head -n 1 unit_equality_problems` | ./tptp2grafite
+
+testall: tptp2grafite
        for X in `cat unit_equality_problems`; do\
-               cat ~/TPTP-v3.1.1/$$X | ./tptp2grafite || echo ERROR PARSING $$X;\
+               cat $(TPTPDIR)/$$X | ./tptp2grafite || echo ERROR PARSING $$X;\
        done