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