helena: updated prolog exportation to ld3 and ALT-0/PTS

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

diff --git a/helm/software/helena/Makefile b/helm/software/helena/Makefile
index 38dab9e6b1d929f8d26cb76b11f385e30c2ff0c3..71abf95d220da622c340d38188eadf646cd8666f 100644 (file)
--- a/helm/software/helena/Makefile
+++ b/helm/software/helena/Makefile
@@ -24,7 +24,7 @@ TARGETS = test-si-fast test-si test2-opt test2-byte test3 test6 \
           profile-fast profile profile-coq profile-coq-byte \
           xml-si xml-si-v3 xml xml-v3 \
           export-coq export-matita \
-          export-lp1 export-lp2 export-tj2 export-tj3 export-lyp \
+          export-lp1 export-lp2 export-tj2 export-tj3 export-pts export-lyp \
           matita matitac
 
 include Makefile.common
@@ -49,11 +49,11 @@ OUTPUT = scripts
 
 MA  = grundlagen_2.ma
 V   = grundlagen_2.v
-LP1 = grundlagen_21.elpi
-LP2 = grundlagen_22.elpi
-TJ2 = grundlagen_22.mod
-TJ3 = grundlagen_23.mod
-CC0 = grundlagen_20.elpi
+LP1 = grundlagen_2a_ld3.elpi
+LP2 = grundlagen_2b_ld3.elpi
+TJ2 = grundlagen_2b_ld3.mod
+TJ3 = grundlagen_2c_ld3.mod
+PTS = grundlagen_2b_pts.elpi
 LYP = grundlagen_2b_lyp.elpi
 
 PREAMBLE_MA = ../matita/matita.ma.templ
@@ -146,34 +146,34 @@ xml-v3: $(EXEC).native etc
 
 export-coq $(OUTPUT)/coq/$(V): $(EXEC).native etc
        @echo "  HELENA -m V8 -q $(INPUT)"
-       $(H)./$(EXEC).native -M $(OUTPUT) -a n -m V8 -p $(PREAMBLE_V) -q $(TEST1) > etc/log.txt
+       $(H)./$(EXEC).native -M $(OUTPUT) -a n -m V8 -p $(PREAMBLE_V) -q $(O) $(TEST1) > etc/log.txt
 
 export-matita $(OUTPUT)/matita/$(MA): $(EXEC).native etc
        @echo "  HELENA -m MA2 -q $(INPUT)"
-       $(H)./$(EXEC).native -M $(OUTPUT) -a n -m MA2 -p $(PREAMBLE_MA) -q $(TEST1) > etc/log.txt
+       $(H)./$(EXEC).native -M $(OUTPUT) -a n -m MA2 -p $(PREAMBLE_MA) -q $(O) $(TEST1) > etc/log.txt
 
 export-lp1 $(OUTPUT)/lp/$(LP1): $(EXEC).native etc
        @echo "  HELENA -m LP1 -q $(INPUT)"
-       $(H)./$(EXEC).native -M $(OUTPUT) -a n -m LP1 -p $(PREAMBLE_LP) -q $(TEST1) > etc/log.txt
+       $(H)./$(EXEC).native -M $(OUTPUT) -a n -m LP1 -p $(PREAMBLE_LP) -q $(O) $(TEST1) > etc/log.txt
 
 export-lp2 $(OUTPUT)/lp/$(LP2): $(EXEC).native etc
        @echo "  HELENA -m LP2 -q $(INPUT)"
-       $(H)./$(EXEC).native -M $(OUTPUT) -a n -m LP2 -p $(PREAMBLE_LP) -q $(TEST1) > etc/log.txt
+       $(H)./$(EXEC).native -M $(OUTPUT) -a n -m LP2 -p $(PREAMBLE_LP) -q $(O) $(TEST1) > etc/log.txt
 
 export-tj2 $(OUTPUT)/lp/$(TJ2): $(EXEC).native etc
        @echo "  HELENA -m TJ2 -q $(INPUT)"
-       $(H)./$(EXEC).native -M $(OUTPUT) -a n -m TJ2 -p $(PREAMBLE_LP) -q $(TEST1) > etc/log.txt
+       $(H)./$(EXEC).native -M $(OUTPUT) -a n -m TJ2 -p $(PREAMBLE_LP) -q $(O) $(TEST1) > etc/log.txt
 
 export-tj3 $(OUTPUT)/lp/$(TJ3): $(EXEC).native etc
        @echo "  HELENA -m TJ3 -q $(INPUT)"
-       $(H)./$(EXEC).native -M $(OUTPUT) -a n -m TJ3 -p $(PREAMBLE_LP) -q $(TEST1) > etc/log.txt
+       $(H)./$(EXEC).native -M $(OUTPUT) -a n -m TJ3 -p $(PREAMBLE_LP) -q $(O) $(TEST1) > etc/log.txt
 
-export-cc0 $(OUTPUT)/cc/$(CC0): $(EXEC).native etc
-       @echo "  HELENA -m CC0 -q $(INPUT)"
-       $(H)./$(EXEC).native -M $(OUTPUT) -a n -m CC0 -p $(PREAMBLE_LP) -q $(TEST1) > etc/log.txt
+export-pts $(OUTPUT)/lp/$(PTS): $(EXEC).native etc
+       @echo "  HELENA -m PTS -c -q $(INPUT)"
+       $(H)./$(EXEC).native -M $(OUTPUT) -a n -m PTS -p $(PREAMBLE_LP) -c -q $(O) $(TEST1) > etc/log.txt
 
 export-lyp $(OUTPUT)/lp/$(LYP): $(EXEC).native etc
-       @echo "  HELENA -m lyp -q $(INPUT)"
+       @echo "  HELENA -m lyp -c -q $(INPUT)"
        $(H)./$(EXEC).native -M $(OUTPUT) -a n -m lyp -p $(PREAMBLE_LP) -c -q $(O) $(TEST1) > etc/log.txt
 
 matita: $(OUTPUT)/matita/$(MA)