TAGS = test-si-fast test-si test2 test3 test6 \
profile-fast profile profile-coq \
xml-si xml-si-v3 xml xml-v3 \
- export-coq export-matita export-elpi \
+ export-coq export-matita \
+ export-lp1 export-lp2 export-tj2 export-tj3 \
matita matitac
include Makefile.common
INPUTFAST = examples/automath/grundlagen_1.aut
-MA = grundlagen_2.ma
-V = grundlagen_2.v
-ELPI = grundlagen_2.elpi
+MA = grundlagen_2.ma
+V = grundlagen_2.v
+LP1 = grundlagen_21.elpi
+LP2 = grundlagen_22.elpi
+TJ2 = grundlagen_22.mod
+TJ2 = grundlagen_23.mod
-PREAMBLE_MA = ../matita/matita.ma.templ
-PREAMBLE_V = coq/grundlagen.template
-PREAMBLE_ELPI = elpi/elpi.template
+PREAMBLE_MA = ../matita/matita.ma.templ
+PREAMBLE_V = coq/grundlagen.template
+PREAMBLE_LP = lp/lp.template
test-si-fast: $(MAIN).opt etc
@echo " HELENA -q -u -x -1 $(INPUTFAST)"
$(H)./$(MAIN).opt -l -u $(INPUT) -X -O $(XMLDIR) -T 1 -l -o -s 2 $(INPUT) > etc/log.txt
export-coq coq/$(V): $(MAIN).opt etc
- $(H)mkdir -p coq
@echo " HELENA -l -m V8 -u $(INPUT)"
$(H)./$(MAIN).opt -T 1 -a n -l -m V8 -p $(PREAMBLE_V) -u $(O) $(INPUT) > etc/log.txt
export-matita matita/$(MA): $(MAIN).opt etc
@echo " HELENA -l -m MA2 -u $(INPUT)"
- $(H)mkdir -p matita
$(H)./$(MAIN).opt -T 1 -a n -l -m MA2 -p $(PREAMBLE_MA) -u $(O) $(INPUT) > etc/log.txt
-export-elpi elpi/$(ELPI): $(MAIN).opt etc
- @echo " HELENA -l -m ELPI -u $(INPUT)"
- $(H)mkdir -p elpi
- $(H)./$(MAIN).opt -T 1 -a n -l -m ELPI1 -p $(PREAMBLE_ELPI) -u $(O) $(INPUT) > etc/log.txt
- $(H)./$(MAIN).opt -T 1 -a n -l -m ELPI2 -p $(PREAMBLE_ELPI) -u $(O) $(INPUT) >> etc/log.txt
+export-lp1 lp/$(LP1): $(MAIN).opt etc
+ @echo " HELENA -l -m LP1 -u $(INPUT)"
+ $(H)./$(MAIN).opt -T 1 -a n -l -m LP1 -p $(PREAMBLE_LP) -u $(O) $(INPUT) > etc/log.txt
+
+export-lp2 lp/$(LP2): $(MAIN).opt etc
+ @echo " HELENA -l -m LP2 -u $(INPUT)"
+ $(H)./$(MAIN).opt -T 1 -a n -l -m LP2 -p $(PREAMBLE_LP) -u $(O) $(INPUT) > etc/log.txt
+
+export-tj2 lp/$(TJ2): $(MAIN).opt etc
+ @echo " HELENA -l -m TJ2 -u $(INPUT)"
+ $(H)./$(MAIN).opt -T 1 -a n -e 253 -l -m TJ2 -p $(PREAMBLE_LP) -u $(O) $(INPUT) > etc/log.txt
+
+export-tj3 lp/$(TJ3): $(MAIN).opt etc
+ @echo " HELENA -l -m TJ3 -u $(INPUT)"
+ $(H)./$(MAIN).opt -T 1 -a n -l -m TJ3 -p $(PREAMBLE_LP) -u $(O) $(INPUT) > etc/log.txt
profile-fast: $(MAIN).opt etc
@echo " HELENA -q -u -x $(INPUTFAST) (31 TIMES)"