helm/software/components/tptp_grafite/Makefile

   1 PACKAGE = tptp_grafite
   2 PREDICATES =
   3
   4 INTERFACE_FILES= parser.mli tptp2grafite.mli
   5
   6 IMPLEMENTATION_FILES = ast.ml lexer.ml $(INTERFACE_FILES:%.mli=%.ml)
   7 EXTRA_OBJECTS_TO_INSTALL =
   8 EXTRA_OBJECTS_TO_CLEAN =
   9
  10 TPTPDIR=/home/$(USER)/TPTP-v3.1.1/
  11
  12 all: tptp2grafite
  13 clean: clean_tests
  14
  15 clean_tests:
  16         rm -f tptp2grafite
  17
  18 parser.mli parser.ml:parser.mly
  19         ocamlyacc parser.mly
  20 lexer.ml:
  21         ocamllex lexer.mll
  22
  23 LOCAL_LINKOPTS = -package helm-$(PACKAGE) -linkpkg
  24 tptp2grafite: main.ml tptp_grafite.cma
  25         @echo "  OCAMLC $<"
  26         @$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
  27
  28 test: tptp2grafite
  29
  30 testall: tptp2grafite
  31         for X in `cat unit_equality_problems`; do\
  32                 cat $(TPTPDIR)/$$X | ./tptp2grafite || echo ERROR PARSING $$X;\
  33         done
  34
  35 generate-%:
  36         for X in `cat $*`; do\
  37                 ./tptp2grafite -tptppath $(TPTPDIR) $$X.p \
  38                 > ../../matita/tests/TPTP/$$X.ma || echo Failed: $$X; \
  39         done
  40
  41 parse-%:
  42         for X in `cat $*`; do\
  43           echo "Parsing $$X"; \
  44                 ./tptp2grafite -tptppath $(TPTPDIR) $$X.p \
  45                 > /dev/null || echo Failed: $$X; \
  46         done
  47
  48 include ../../Makefile.defs
  49 include ../Makefile.common
  50