]> matita.cs.unibo.it Git - helm.git/blob - components/tptp_grafite/Makefile
Level-1/LambdaDelta now compiles fine
[helm.git] / 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 unit_equality_problems`; do\
37                 ./tptp2grafite -tptppath $(TPTPDIR) $$X \
38                 > ../../../matita/tests/TPTP/$$X.ma || echo Failed: $$X; \
39         done
40
41 parse:
42         for X in `cat unit_equality_problems`; do\
43           echo "Parsing $$X"; \
44                 ./tptp2grafite -tptppath $(TPTPDIR) $$X \
45                 > /dev/null || echo Failed: $$X; \
46         done
47
48 include ../../Makefile.defs
49 include ../Makefile.common
50