X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftptp_grafite%2FMakefile;h=c196dd609e418ccd733d2f51b8a00da848ae3a5b;hb=0581f3c8dc2098b82cd31a0fbed224a95652bd88;hp=c5c6e63469782de7a2a249a92201a58ef040e3b1;hpb=bc76b4d2f3c380894259b45fad52cf85ae6cee18;p=helm.git diff --git a/helm/software/components/tptp_grafite/Makefile b/helm/software/components/tptp_grafite/Makefile index c5c6e6346..c196dd609 100644 --- a/helm/software/components/tptp_grafite/Makefile +++ b/helm/software/components/tptp_grafite/Makefile @@ -7,7 +7,7 @@ IMPLEMENTATION_FILES = ast.ml lexer.ml $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = -TPTPDIR=/home/$(USER)/TPTP-v3.1.1/ +TPTPDIR= /home/$(USER)/work-area/TPTP-v3.2.0/ all: tptp2grafite clean: clean_tests @@ -32,16 +32,22 @@ testall: tptp2grafite cat $(TPTPDIR)/$$X | ./tptp2grafite || echo ERROR PARSING $$X;\ done -generate: - for X in `cat unit_equality_problems`; do\ - ./tptp2grafite -tptppath $(TPTPDIR) $$X \ - > ../../../matita/tests/TPTP/$$X.ma || echo Failed: $$X; \ +generate-%: + for X in `cat $*`; do\ + ./tptp2grafite -tptppath $(TPTPDIR) $$X.p \ + > ../../matita/tests/TPTP/$$X.ma || echo Failed: $$X; \ done -parse: - for X in `cat unit_equality_problems`; do\ +ngenerate-%: + for X in `cat $*`; do\ + ./tptp2grafite -ng -tptppath $(TPTPDIR) $$X.p \ + > ../../matita/contribs/ng_TPTP/$$X.ma || echo Failed: $$X; \ + done + +parse-%: + for X in `cat $*`; do\ echo "Parsing $$X"; \ - ./tptp2grafite -tptppath $(TPTPDIR) $$X \ + ./tptp2grafite -tptppath $(TPTPDIR) $$X.p \ > /dev/null || echo Failed: $$X; \ done