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