]> matita.cs.unibo.it Git - helm.git/blob - helm/interface/Makefile
Much more modularity and some buf fixed in http_getter.pl
[helm.git] / helm / interface / Makefile
1 LABLGTK_DIR = /usr/lib/ocaml/lablgtk
2 LABLGTK_MATHVIEW_DIR = /usr/lib/ocaml/lablgtk/mathview
3 MINIDOM_DIR = /usr/lib/ocaml/lablgtk/mathview/minidom
4 PXP_DIR = /usr/lib/ocaml/site-lib/pxp
5 NETSTRING_DIR = /usr/lib/ocaml/site-lib/netstring
6 OCAMLC = ocamlc -I $(LABLGTK_DIR) -I $(LABLGTK_MATHVIEW_DIR) -I $(PXP_DIR) -I $(NETSTRING_DIR) -I $(MINIDOM_DIR) -I mlmathview
7 OCAMLOPT = ocamlopt -I $(LABLGTK_DIR) -I $(LABLGTK_MATHVIEW_DIR) -I mlgtk_devel -I $(PXP_DIR) -I $(NETSTRING_DIR) -I $(MINIDOM_DIR) -I mlmathview
8 OCAMLDEP = ocamldep
9
10 all: experiment reduction fix_params mmlinterface
11 opt: experiment.opt reduction.opt fix_params.opt mmlinterface.opt
12
13 PXPLIBS = netstring.cma netmappings_iso.cmo netmappings_other.cmo \
14           pxp_types.cma \
15           pxp_lex_iso88591.cma pxp_lex_utf8.cma pxp_engine.cma \
16           pxp_utf8.cmo
17
18 PXPLIBSOPT = netstring.cmxa netmappings_iso.cmx netmappings_other.cmx \
19              pxp_types.cmxa \
20              pxp_lex_iso88591.cmxa pxp_lex_utf8.cmxa pxp_engine.cmxa \
21              pxp_utf8.cmx
22
23
24 DEPOBJS = experiment.ml cicCache.ml cicCache.mli cicPp.ml cicPp.mli \
25           cicParser.ml cicParser.mli cicParser2.ml cicParser2.mli \
26           cicParser3.ml cicParser3.mli cic.ml getter.ml getter.mli \
27           gtkInterface.ml cicReduction.ml cicReduction.mli cicTypeChecker.ml \
28           cicTypeChecker.mli reduction.ml tgtkInterface.ml theory.ml \
29           theoryParser.ml theoryParser2.ml theoryPp.ml theoryTypeChecker.ml \
30           cicCooking.ml cicCooking.mli cicFindParameters.ml theoryCache.ml \
31           fix_params.ml cic2Xml.ml xml.ml uriManager.ml uriManager.mli \
32           cicSubstitution.ml cicSubstitution.mli mml.ml \
33           mmlinterface.ml configuration.ml \
34           xsltProcessor.ml deannotate.ml cicXPath.ml pxpUriResolver.ml \
35           annotationParser.ml annotationParser2.ml annotation2Xml.ml \
36           cicAnnotationHinter.ml
37
38 MMLINTERFACEOBJS = configuration.cmo uriManager.cmo getter.cmo cic.cmo \
39                    pxpUriResolver.cmo \
40                    cicParser3.cmo cicParser2.cmo cicParser.cmo deannotate.cmo \
41                    cicSubstitution.cmo annotationParser2.cmo \
42                    annotationParser.cmo cicCache.cmo cicCooking.cmo cicPp.cmo \
43                    cicReduction.cmo cicTypeChecker.cmo mml.cmo \
44                    xml.cmo \
45                    xsltProcessor.cmo cic2Xml.cmo annotation2Xml.cmo \
46                    cicXPath.cmo theory.cmo theoryParser2.cmo theoryParser.cmo \
47                    theoryCache.cmo theoryTypeChecker.cmo \
48                    cicAnnotationHinter.cmo mmlinterface.cmo
49
50 MMLINTERFACEOPTOBJS = configuration.cmx uriManager.cmx getter.cmx cic.cmx \
51                       pxpUriResolver.cmx \
52                       cicParser3.cmx cicParser2.cmx cicParser.cmx \
53                       deannotate.cmx cicSubstitution.cmx annotationParser2.cmx \
54                       annotationParser.cmx cicCache.cmx \
55                       cicCooking.cmx cicPp.cmx cicReduction.cmx \
56                       cicTypeChecker.cmx mml.cmx \
57                       xml.cmx xsltProcessor.cmx \
58                       cic2Xml.cmx annotation2Xml.cmx cicXPath.cmx \
59                       theory.cmx theoryParser2.cmx theoryParser.cmx \
60                       theoryCache.cmx theoryTypeChecker.cmx \
61                       cicAnnotationHinter.cmx mmlinterface.cmx
62
63 FIX_PARAMSOBJS = configuration.cmo uriManager.cmo getter.cmo cic.cmo \
64                  pxpUriResolver.cmo \
65                  cicParser3.cmo cicParser2.cmo cicParser.cmo deannotate.cmo \
66                  cicSubstitution.cmo annotationParser2.cmo \
67                  annotationParser.cmo  cicCache.cmo cicPp.cmo xml.cmo \
68                  cic2Xml.cmo cicFindParameters.cmo fix_params.cmo
69
70 FIX_PARAMSOPTOBJS = configuration.cmx uriManager.cmx getter.cmx cic.cmx \
71                     pxpUriResolver.cmx \
72                     cicParser3.cmx cicParser2.cmx cicParser.cmx deannotate.cmx \
73                     cicSubstitution.cmx annotationParser2.cmx \
74                     annotationParser.cmx cicCache.cmx cicPp.cmx xml.cmx \
75                     cic2Xml.cmx cicFindParameters.cmx fix_params.cmx
76
77 REDUCTIONOBJS = configuration.cmo uriManager.cmo getter.cmo cic.cmo \
78                 pxpUriResolver.cmo \
79                 cicParser3.cmo cicParser2.cmo cicParser.cmo deannotate.cmo \
80                 cicSubstitution.cmo annotationParser2.cmo annotationParser.cmo \
81                 cicCache.cmo cicPp.cmo cicCooking.cmo \
82                 cicReduction.cmo cicTypeChecker.cmo reduction.cmo
83
84 REDUCTIONOPTOBJS = configuration.cmx uriManager.cmx getter.cmx cic.cmx \
85                    pxpUriResolver.cmx \
86                    cicParser3.cmx cicParser2.cmx cicParser.cmx deannotate.cmx \
87                    cicSubstitution.cmx annotationParser2.cmx \
88                    annotationParser.cmx cicCache.cmx cicPp.cmx cicCooking.cmx \
89                    cicReduction.cmx cicTypeChecker.cmx reduction.cmx
90
91 EXPERIMENTOBJS = configuration.cmo uriManager.cmo getter.cmo cic.cmo \
92                  pxpUriResolver.cmo \
93                  cicParser3.cmo cicParser2.cmo cicParser.cmo deannotate.cmo \
94                  cicSubstitution.cmo annotationParser2.cmo \
95                  annotationParser.cmo cicCache.cmo cicPp.cmo experiment.cmo
96
97 EXPERIMENTOPTOBJS = configuration.cmx uriManager.cmx getter.cmx cic.cmx \
98                     pxpUriResolver.cmx \
99                     cicParser3.cmx cicParser2.cmx cicParser.cmx deannotate.cmx \
100                     cicSubstitution.cmx annotationParser2.cmx \
101                     annotationParser.cmx cicCache.cmx cicPp.cmx experiment.cmx
102
103 depend:
104         $(OCAMLDEP) $(DEPOBJS) > .depend
105
106 mmlinterface: $(MMLINTERFACEOBJS)
107         $(OCAMLC) -custom -o mmlinterface str.cma unix.cma $(PXPLIBS) dbm.cma \
108                   lablgtk.cma gtkInit.cmo \
109                   $(LABLGTK_MATHVIEW_DIR)/lablgtkmathview.cma \
110                   $(MINIDOM_DIR)/minidom.cmo \
111                   $(MMLINTERFACEOBJS) \
112                   -cclib "-lstr -L/usr/lib -L/usr/X11R6/lib -lgtk -lgdk \
113                   -rdynamic -lgmodule -lglib -ldl -lXi -lXext -lX11 -lm \
114                   -lunix -L/usr/local/lib/gtkmathview -lgtkmathview \
115                   $(LABLGTK_MATHVIEW_DIR)/ml_gtk_mathview.o \
116                   $(MINIDOM_DIR)/ml_minidom.o" \
117                   -cclib -lmldbm -cclib -lndbm
118
119 mmlinterface.opt: $(MMLINTERFACEOPTOBJS)
120         $(OCAMLOPT) -o mmlinterface.opt str.cmxa $(PXPLIBSOPT) unix.cmxa \
121                     dbm.cmxa lablgtk.cmxa gtkInit.cmx \
122                     $(LABLGTK_MATHVIEW_DIR)/lablgtkmathview.cmxa \
123                     $(MINIDOM_DIR)/minidom.cmx \
124                     $(MMLINTERFACEOPTOBJS) \
125                     -cclib "-lstr -L/usr/lib -L/usr/X11R6/lib -lgtk -lgdk \
126                     -rdynamic -lgmodule -lglib -ldl -lXi -lXext -lX11 -lm \
127                     -lunix -L/usr/local/lib/gtkmathview -lgtkmathview \
128                     $(LABLGTK_MATHVIEW_DIR)/ml_gtk_mathview.o \
129                     $(MINIDOM_DIR)/ml_minidom.o" \
130                     -cclib -lmldbm -cclib -lndbm
131
132 fix_params: $(FIX_PARAMSOBJS)
133         $(OCAMLC) -custom -o fix_params str.cma $(PXPLIBS) dbm.cma \
134                   $(FIX_PARAMSOBJS) -cclib -lstr -cclib -lmldbm -cclib -lndbm
135
136 fix_params.opt: $(FIX_PARAMSOPTOBJS)
137         $(OCAMLOPT) -o fix_params.opt str.cmxa $(PXPLIBSOPT) dbm.cmxa \
138                     $(FIX_PARAMSOPTOBJS) -cclib -lstr -cclib -lmldbm \
139                     -cclib -lndbm
140
141 reduction: $(REDUCTIONOBJS)
142         $(OCAMLC) -custom -o reduction str.cma $(PXPLIBS) dbm.cma \
143                   $(REDUCTIONOBJS) -cclib -lstr -cclib -lmldbm -cclib -lndbm
144
145 reduction.opt: $(REDUCTIONOPTOBJS)
146         $(OCAMLOPT) -o reduction.opt str.cmxa $(PXPLIBSOPT) dbm.cmxa \
147                     $(REDUCTIONOPTOBJS) -cclib -lstr -cclib -lmldbm \
148                     -cclib -lndbm
149
150 experiment: $(EXPERIMENTOBJS)
151         $(OCAMLC) -custom -o experiment str.cma $(PXPLIBS) dbm.cma \
152                   $(EXPERIMENTOBJS) -cclib -lstr -cclib -lmldbm -cclib -lndbm
153
154 experiment.opt: $(EXPERIMENTOPTOBJS)
155         $(OCAMLOPT) -o experiment.opt str.cmxa $(PXPLIBSOPT) dbm.cmxa \
156                     $(EXPERIMENTOPTOBJS) -cclib -lstr -cclib -lmldbm \
157                     -cclib -lndbm
158
159 .SUFFIXES: .ml .mli .cmo .cmi .cmx
160 .ml.cmo:
161         $(OCAMLC) -c $<
162 .mli.cmi:
163         $(OCAMLC) -c $<
164 .ml.cmx:
165         $(OCAMLOPT) -c $<
166
167 clean:
168         rm -f *.cm[iox] *.o experiment experiment.opt reduction \
169            reduction.opt fix_params fix_params.opt mmlinterface \
170            mmlinterface.opt mmlinterface2 mmlinterface2.opt
171
172 start-xaland:
173         java -ss1024K -oss8192K \
174            xaland 12345 12346 \
175            $(COQV)/examples/style/rootcontent.xsl \
176            $(COQV)/examples/style/annotatedpres.xsl \
177            $(COQV)/examples/style/theory_content.xsl \
178            $(COQV)/examples/style/theory_pres.xsl
179
180 start-xaland-2:
181         java -ss1024K -oss8192K \
182            xaland2 12345 12346 \
183            $(COQV)/examples/style/rootcontent.xsl \
184            $(COQV)/examples/style/annotatedpres.xsl \
185            $(COQV)/examples/style/theory_content.xsl \
186            $(COQV)/examples/style/theory_pres.xsl
187
188 start-xaland-old:
189         java xaland 12345 12346 \
190          $(COQV)/examples/style/style_prima_del_linguaggio_naturale/rootcontent.xsl \
191          $(COQV)/examples/style/style_prima_del_linguaggio_naturale/annotatedpres.xsl \
192          $(COQV)/examples/style/style_prima_del_linguaggio_naturale/theory_content.xsl \
193          $(COQV)/examples/style/style_prima_del_linguaggio_naturale/theory_pres.xsl
194
195 start-xaland3:
196         java xaland 12347 12348 \
197            $(COQV)/examples/style/rootcontent.xsl \
198            $(COQV)/examples/style/annotatedpres.xsl \
199            $(COQV)/examples/style/theory_content.xsl \
200            $(COQV)/examples/style/theory_pres.xsl
201
202 start-http-getter:
203         http_getter/http_getter.pl
204
205 include .depend