advances on exportation to prolog

[helm.git] / helm / software / helena / Makefile

diff --git a/helm/software/helena/Makefile b/helm/software/helena/Makefile
index 42cf240fc78f25f60104f67c15c6ef8182a55259..8ae171cd05fc12e247bd7200d8125b048fef8c80 100644 (file)
--- a/helm/software/helena/Makefile
+++ b/helm/software/helena/Makefile
@@ -13,7 +13,8 @@ CLEAN = etc/log.txt etc/profile.txt
 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
@@ -30,13 +31,16 @@ INPUT = examples/automath/grundlagen_2.aut
 
 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)"
@@ -75,20 +79,28 @@ xml-v3: $(MAIN).opt etc
        $(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)"