]> matita.cs.unibo.it Git - helm.git/blob - helm/software/lambda-delta/Makefile
683e422a41313570582265e7fe0e2f5662b2d671
[helm.git] / helm / software / lambda-delta / Makefile
1 MAIN = helena
2
3 SRC  = src
4
5 REQUIRES = unix str helm-ng_kernel
6
7 OCAMLOPTIONS = -rectypes 
8
9 KEEP = README
10
11 CLEAN = etc/log.txt etc/profile.txt
12
13 TAGS = test-si test-si-fast hal xml-si-crg xml-si profile
14
15 XMLS = xml/brg-si/grundlagen/l/not.ld.xml \
16        xml/brg-si/grundlagen/l/et.ld.xml \
17        xml/brg-si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \
18        xml/brg-si/grundlagen/l/e/pairis1.ld.xml \
19        xml/crg-si/grundlagen/l/not.ld.xml \
20        xml/crg-si/grundlagen/l/et.ld.xml \
21        xml/crg-si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \
22        xml/crg-si/grundlagen/l/e/pairis1.ld.xml
23
24 include Makefile.common
25
26 HOME = .
27
28 INPUT = examples/grundlagen/grundlagen.aut
29
30 test-si: $(MAIN).opt etc
31         @echo "  HELENA -p -u $(INPUT)"
32         $(H)./$(MAIN).opt -p -u -S 3 $(O) $(INPUT) > etc/log.txt
33
34 test-si-fast: $(MAIN).opt etc
35         @echo "  HELENA -u -q $(INPUT)"
36         $(H)./$(MAIN).opt -u -q -S 1 $(O) $(INPUT) > etc/log.txt
37
38 profile: $(MAIN).opt etc
39         @echo "  HELENA -u -q $(INPUT) (30 TIMES)"
40         $(H)rm etc/log.txt
41         $(H)for T in `seq 30`; do ./$(MAIN).opt -u -q -s 3 -S 1 $(O) $(INPUT) >> etc/log.txt; done
42         $(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile-new.txt
43
44 xml-si: $(MAIN).opt etc
45         @echo "  HELENA -u -x -s 2 $(INPUT)"
46         $(H)./$(MAIN).opt -u -x $(HOME) -s 2 -S 1 $(INPUT) > etc/log.txt
47
48 xml-si-crg: $(MAIN).opt etc
49         @echo "  HELENA -u -x -s 1 $(INPUT)"
50         $(H)./$(MAIN).opt -u -x $(HOME) -s 1 -S 1 $(INPUT) > etc/log.txt
51
52 etc:
53         @echo "  MKDIR etc"
54         $(H)mkdir etc
55
56 %.ld: BASEURL = --stringparam baseurl $(LDDLURL)
57
58 %.ld:
59         @echo "  XSLT $@"
60         $(H)mkdir -p $(LOCALLDDLDIR)/$(@D)
61         $(H)$(XSLT) -o $(LOCALLDDLDIR)/$@.html $(BASEURL) xml/ld-html.xsl xml/$@.xml
62
63 etc/make-html.sh xml/index.txt index:
64         @echo "  GENERATE INDEXES"
65         $(H)find xml -name "*.ld.xml" | sed s/.xml//g | sed s/xml/ld:/g > xml/index.txt
66         $(H)sed "s/^/make --no-print-directory /" xml/index.txt | sed s.ld:/.. > etc/make-html.sh
67
68 html: etc/make-html.sh
69         @echo "  MAKE */*.ld"
70         $(H). $<
71
72 test-html:
73         @$(MAKE) --no-print-directory $(XMLS:xml/%.xml=%)
74
75 install-html: etc/make-html.sh
76         @echo "  INSTALL xml"
77         $(H)scp -r $(LOCALLDDLDIR)/* $(LDDLDIR)
78
79 install-lddl: index
80         @echo "  INSTALL lddl.tar.bz2"
81         $(H)tar -cjf $(DOWNDIR)/lddl.tar.bz2 -X etc/exclude.txt xml
82
83 install-dtd: xml/ld.dtd
84         @echo "  INSTALL $<"
85         $(H)scp $< $(XMLDIR) 
86
87 install-xml: etc/make-html.sh
88         @echo "  INSTALL xml"
89         $(H)scp -r xml/index.txt xml/ld.dtd xml/brg-si/ xml/crg-si/ $(XMLDIR)
90
91 # old targets ##########################################################
92
93 test: $(MAIN).opt etc
94         @echo "  HELENA -o -p $(INPUT)"
95         $(H)./$(MAIN).opt -o -p -S 3 $(O) $(INPUT) > etc/log.txt
96
97 test-si-old: $(MAIN).opt etc
98         @echo "  HELENA -o -p -u $(INPUT)"
99         $(H)./$(MAIN).opt -o -p -u -S 3 $(O) $(INPUT) > etc/log.txt
100
101 test-si-fast-old: $(MAIN).opt etc
102         @echo "  HELENA -o -u -q $(INPUT)"
103         $(H)./$(MAIN).opt -o -u -q -S 1 $(O) $(INPUT) > etc/log.txt
104
105 xml-si-old: $(MAIN).opt etc
106         @echo "  HELENA -o -u -x -s 2 $(INPUT)"
107         $(H)./$(MAIN).opt -o -u -x $(HOME) -s 2 -S 1 $(INPUT) > etc/log.txt