X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftptp2grafite%2FMakefile;h=d79c2661dbcdea785e51ae4af7f599e5a8cb090e;hb=15b42d9cdb401538a9ba8d9ab82d2ad046596e8b;hp=e96134e5d22449008767ef0fca95a291ea22ebf0;hpb=39029e4dd766589e69b7f72580e7051cad99d3da;p=helm.git

diff --git a/helm/software/components/binaries/tptp2grafite/Makefile b/helm/software/components/binaries/tptp2grafite/Makefile
index e96134e5d..d79c2661d 100644
--- a/helm/software/components/binaries/tptp2grafite/Makefile
+++ b/helm/software/components/binaries/tptp2grafite/Makefile
@@ -1,19 +1,39 @@
-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 $(TPTPDIR)/$$X | ./tptp2grafite || echo ERROR PARSING $$X;\
+	done
+
+generate:
+	for X in `cat unit_equality_problems`; do\
+		./tptp2grafite -tptppath /home/tassi/TPTP-v3.1.1/ $$X \
+		> ../../../matita/tests/TPTP/$$X.ma || echo Failed: $$X; \
+	done
+
+parse:
 	for X in `cat unit_equality_problems`; do\
-		cat ~/TPTP-v3.1.1/$$X | ./tptp2grafite || echo ERROR PARSING $$X;\
+	  echo "Parsing $$X"; \
+		./tptp2grafite -tptppath /home/tassi/TPTP-v3.1.1/ $$X \
+		> /dev/null || echo Failed: $$X; \
 	done