| author | haftmann |
| Wed, 08 Sep 2010 13:22:24 +0200 | |
| changeset 39444 | 49fc6c842d6c |
| parent 39224 | 4bf80c23320e |
| child 39814 | fe5722fce758 |
| permissions | -rw-r--r-- |
1 #
2 # IsaMakefile for Pure
3 #
5 ## targets
7 default: Pure
8 images: Pure
9 test: RAW
10 all: images test
13 ## global settings
15 SRC = $(ISABELLE_HOME)/src
16 OUT = $(ISABELLE_OUTPUT)
17 LOG = $(OUT)/log
20 ## Pure
22 BOOTSTRAP_FILES = \
23 ML-Systems/bash.ML \
24 ML-Systems/compiler_polyml-5.2.ML \
25 ML-Systems/compiler_polyml-5.3.ML \
26 ML-Systems/ml_name_space.ML \
27 ML-Systems/ml_pretty.ML \
28 ML-Systems/multithreading.ML \
29 ML-Systems/multithreading_polyml.ML \
30 ML-Systems/overloading_smlnj.ML \
31 ML-Systems/polyml-5.2.1.ML \
32 ML-Systems/polyml-5.2.ML \
33 ML-Systems/polyml.ML \
34 ML-Systems/polyml_common.ML \
35 ML-Systems/pp_dummy.ML \
36 ML-Systems/pp_polyml.ML \
37 ML-Systems/proper_int.ML \
38 ML-Systems/single_assignment.ML \
39 ML-Systems/single_assignment_polyml.ML \
40 ML-Systems/smlnj.ML \
41 ML-Systems/thread_dummy.ML \
42 ML-Systems/time_limit.ML \
43 ML-Systems/timing.ML \
44 ML-Systems/universal.ML \
45 ML-Systems/unsynchronized.ML \
46 ML-Systems/use_context.ML
48 RAW: $(OUT)/RAW
50 $(OUT)/RAW: $(BOOTSTRAP_FILES)
51 @./mk -r
54 Pure: $(OUT)/Pure
56 $(OUT)/Pure: $(BOOTSTRAP_FILES) \
57 Concurrent/cache.ML \
58 Concurrent/future.ML \
59 Concurrent/lazy.ML \
60 Concurrent/lazy_sequential.ML \
61 Concurrent/mailbox.ML \
62 Concurrent/par_list.ML \
63 Concurrent/par_list_sequential.ML \
64 Concurrent/simple_thread.ML \
65 Concurrent/single_assignment.ML \
66 Concurrent/single_assignment_sequential.ML \
67 Concurrent/synchronized.ML \
68 Concurrent/synchronized_sequential.ML \
69 Concurrent/task_queue.ML \
70 General/alist.ML \
71 General/antiquote.ML \
72 General/balanced_tree.ML \
73 General/basics.ML \
74 General/binding.ML \
75 General/buffer.ML \
76 General/exn.ML \
77 General/file.ML \
78 General/graph.ML \
79 General/heap.ML \
80 General/integer.ML \
81 General/linear_set.ML \
82 General/long_name.ML \
83 General/markup.ML \
84 General/name_space.ML \
85 General/ord_list.ML \
86 General/output.ML \
87 General/path.ML \
88 General/position.ML \
89 General/pretty.ML \
90 General/print_mode.ML \
91 General/properties.ML \
92 General/queue.ML \
93 General/same.ML \
94 General/scan.ML \
95 General/secure.ML \
96 General/seq.ML \
97 General/sha1.ML \
98 General/sha1_polyml.ML \
99 General/source.ML \
100 General/stack.ML \
101 General/symbol.ML \
102 General/symbol_pos.ML \
103 General/table.ML \
104 General/url.ML \
105 General/xml.ML \
106 General/xml_data.ML \
107 General/yxml.ML \
108 Isar/args.ML \
109 Isar/attrib.ML \
110 Isar/auto_bind.ML \
111 Isar/calculation.ML \
112 Isar/class.ML \
113 Isar/class_declaration.ML \
114 Isar/code.ML \
115 Isar/context_rules.ML \
116 Isar/element.ML \
117 Isar/expression.ML \
118 Isar/generic_target.ML \
119 Isar/isar_cmd.ML \
120 Isar/isar_syn.ML \
121 Isar/keyword.ML \
122 Isar/local_defs.ML \
123 Isar/local_syntax.ML \
124 Isar/local_theory.ML \
125 Isar/locale.ML \
126 Isar/method.ML \
127 Isar/named_target.ML \
128 Isar/object_logic.ML \
129 Isar/obtain.ML \
130 Isar/outer_syntax.ML \
131 Isar/overloading.ML \
132 Isar/parse.ML \
133 Isar/parse_spec.ML \
134 Isar/parse_value.ML \
135 Isar/proof.ML \
136 Isar/proof_context.ML \
137 Isar/proof_display.ML \
138 Isar/proof_node.ML \
139 Isar/rule_cases.ML \
140 Isar/rule_insts.ML \
141 Isar/runtime.ML \
142 Isar/skip_proof.ML \
143 Isar/spec_rules.ML \
144 Isar/specification.ML \
145 Isar/token.ML \
146 Isar/toplevel.ML \
147 Isar/typedecl.ML \
148 ML/install_pp_polyml-5.3.ML \
149 ML/install_pp_polyml.ML \
150 ML/ml_antiquote.ML \
151 ML/ml_compiler.ML \
152 ML/ml_compiler_polyml-5.3.ML \
153 ML/ml_context.ML \
154 ML/ml_env.ML \
155 ML/ml_lex.ML \
156 ML/ml_parse.ML \
157 ML/ml_syntax.ML \
158 ML/ml_thms.ML \
159 PIDE/document.ML \
160 PIDE/isar_document.ML \
161 Proof/extraction.ML \
162 Proof/proof_rewrite_rules.ML \
163 Proof/proof_syntax.ML \
164 Proof/proofchecker.ML \
165 Proof/reconstruct.ML \
166 ProofGeneral/pgip.ML \
167 ProofGeneral/pgip_input.ML \
168 ProofGeneral/pgip_isabelle.ML \
169 ProofGeneral/pgip_markup.ML \
170 ProofGeneral/pgip_output.ML \
171 ProofGeneral/pgip_parser.ML \
172 ProofGeneral/pgip_tests.ML \
173 ProofGeneral/pgip_types.ML \
174 ProofGeneral/pgml.ML \
175 ProofGeneral/preferences.ML \
176 ProofGeneral/proof_general_emacs.ML \
177 ProofGeneral/proof_general_pgip.ML \
178 Pure.thy \
179 ROOT.ML \
180 Syntax/ast.ML \
181 Syntax/lexicon.ML \
182 Syntax/mixfix.ML \
183 Syntax/parser.ML \
184 Syntax/printer.ML \
185 Syntax/simple_syntax.ML \
186 Syntax/syn_ext.ML \
187 Syntax/syn_trans.ML \
188 Syntax/syntax.ML \
189 Syntax/type_ext.ML \
190 System/isabelle_process.ML \
191 System/isar.ML \
192 System/session.ML \
193 Thy/html.ML \
194 Thy/latex.ML \
195 Thy/present.ML \
196 Thy/term_style.ML \
197 Thy/thm_deps.ML \
198 Thy/thy_header.ML \
199 Thy/thy_info.ML \
200 Thy/thy_load.ML \
201 Thy/thy_output.ML \
202 Thy/thy_syntax.ML \
203 Tools/find_consts.ML \
204 Tools/find_theorems.ML \
205 Tools/named_thms.ML \
206 Tools/xml_syntax.ML \
207 assumption.ML \
208 axclass.ML \
209 codegen.ML \
210 config.ML \
211 conjunction.ML \
212 consts.ML \
213 context.ML \
214 context_position.ML \
215 conv.ML \
216 defs.ML \
217 display.ML \
218 drule.ML \
219 envir.ML \
220 facts.ML \
221 goal.ML \
222 goal_display.ML \
223 interpretation.ML \
224 item_net.ML \
225 library.ML \
226 logic.ML \
227 meta_simplifier.ML \
228 more_thm.ML \
229 morphism.ML \
230 name.ML \
231 net.ML \
232 old_term.ML \
233 pattern.ML \
234 primitive_defs.ML \
235 proofterm.ML \
236 pure_setup.ML \
237 pure_thy.ML \
238 search.ML \
239 sign.ML \
240 simplifier.ML \
241 sorts.ML \
242 subgoal.ML \
243 tactic.ML \
244 tactical.ML \
245 term.ML \
246 term_ord.ML \
247 term_subst.ML \
248 theory.ML \
249 thm.ML \
250 type.ML \
251 type_infer.ML \
252 unify.ML \
253 variable.ML
254 @./mk
257 ## clean
259 clean:
260 @rm -f $(OUT)/Pure $(LOG)/Pure.gz $(OUT)/RAW $(LOG)/RAW.gz