components/binaries/tptp2grafite/Makefile

   1 OCAMLC = OCAMLPATH=../../METAS ocamlfind ocamlc -package helm-grafite_parser
   2 TPTPDIR=/home/$(USER)/TPTP-v3.1.1/
   3
   4 opt all: tptp2grafite
   5         echo -n
   6
   7 tptp2grafite: ast.ml parser.mly lexer.mll main.ml
   8         $(OCAMLC) -c ast.ml
   9         ocamlyacc parser.mly
  10         $(OCAMLC) -c parser.mli
  11         $(OCAMLC) -c parser.ml
  12         ocamllex lexer.mll
  13         $(OCAMLC) -c lexer.ml
  14         $(OCAMLC) -c main.ml
  15         $(OCAMLC) -linkpkg -o tptp2grafite ast.cmo lexer.cmo parser.cmo main.cmo
  16
  17 clean:
  18         rm -f tptp2grafite *.cmo *.cmi parser.mli parser.ml lexer.ml rm *.output
  19
  20 test: tptp2grafite
  21         cat $(TPTPDIR)/`head -n 1 unit_equality_problems` | ./tptp2grafite
  22
  23 testall: tptp2grafite
  24         for X in `cat unit_equality_problems`; do\
  25                 cat $(TPTPDIR)/$$X | ./tptp2grafite || echo ERROR PARSING $$X;\
  26         done
  27
  28 generate:
  29         for X in `cat unit_equality_problems`; do\
  30                 ./tptp2grafite -tptppath $(TPTPDIR) $$X \
  31                 > ../../../matita/tests/TPTP/$$X.ma || echo Failed: $$X; \
  32         done
  33
  34 parse:
  35         for X in `cat unit_equality_problems`; do\
  36           echo "Parsing $$X"; \
  37                 ./tptp2grafite -tptppath $(TPTPDIR) $$X \
  38                 > /dev/null || echo Failed: $$X; \
  39         done