1 OCAMLC = OCAMLPATH=../../METAS ocamlfind ocamlc -package helm-grafite_parser
2 TPTPDIR=/home/$(USER)/TPTP-v3.1.1/
7 tptp2grafite: ast.ml parser.mly lexer.mll main.ml
10 $(OCAMLC) -c parser.mli
11 $(OCAMLC) -c parser.ml
15 $(OCAMLC) -linkpkg -o tptp2grafite ast.cmo lexer.cmo parser.cmo main.cmo
18 rm -f tptp2grafite *.cmo *.cmi parser.mli parser.ml lexer.ml rm *.output
21 cat $(TPTPDIR)/`head -n 1 unit_equality_problems` | ./tptp2grafite
24 for X in `cat unit_equality_problems`; do\
25 cat $(TPTPDIR)/$$X | ./tptp2grafite || echo ERROR PARSING $$X;\
29 for X in `cat unit_equality_problems`; do\
30 ./tptp2grafite -tptppath $(TPTPDIR) $$X \
31 > ../../../matita/tests/TPTP/$$X.ma || echo Failed: $$X; \
35 for X in `cat unit_equality_problems`; do\
37 ./tptp2grafite -tptppath $(TPTPDIR) $$X \
38 > /dev/null || echo Failed: $$X; \