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