author  wenzelm 
Thu, 18 Sep 2008 22:30:17 +0200  
changeset 28295  3fb78d2068b0 
parent 28288  09c812966e7f 
child 28299  14ab7a17e92b 
permissions  rwrr 
2431  1 
# 
4518  2 
# $Id$ 
2431  3 
# 
4518  4 
# IsaMakefile for Pure 
2431  5 
# 
6 

4518  7 
## targets 
8 

9 
default: Pure 

10 
images: Pure 

24880
c827d25b2983
added PureProofGeneral target (dummy session with outer syntax keyword initialization);
wenzelm
parents:
24830
diff
changeset

11 
test: RAW PureProofGeneral 
4518  12 
all: images test 
13 

14 

15 
## global settings 

16 

17 
SRC = $(ISABELLE_HOME)/src 

3118  18 
OUT = $(ISABELLE_OUTPUT) 
4518  19 
LOG = $(OUT)/log 
20 

2431  21 

4518  22 
## Pure 
23 

27204  24 
Pure: $(OUT)/Pure 
2431  25 

28155  26 
$(OUT)/Pure: Concurrent/future.ML Concurrent/mailbox.ML \ 
28198  27 
Concurrent/par_list.ML Concurrent/schedule.ML \ 
28240  28 
Concurrent/simple_thread.ML Concurrent/task_queue.ML General/ROOT.ML \ 
29 
General/alist.ML General/balanced_tree.ML General/basics.ML \ 

30 
General/buffer.ML General/file.ML General/graph.ML General/heap.ML \ 

31 
General/integer.ML General/markup.ML General/name_space.ML \ 

32 
General/ord_list.ML General/output.ML General/path.ML \ 

33 
General/position.ML General/pretty.ML General/print_mode.ML \ 

34 
General/properties.ML General/queue.ML General/scan.ML \ 

35 
General/secure.ML General/seq.ML General/source.ML General/stack.ML \ 

36 
General/susp.ML General/symbol.ML General/symbol_pos.ML \ 

37 
General/table.ML General/url.ML General/xml.ML General/yxml.ML \ 

38 
Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML Isar/attrib.ML \ 

39 
Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML Isar/code.ML \ 

40 
Isar/code_unit.ML Isar/constdefs.ML Isar/context_rules.ML \ 

41 
Isar/element.ML Isar/find_theorems.ML Isar/instance.ML Isar/isar.ML \ 

42 
Isar/isar_cmd.ML Isar/isar_syn.ML Isar/local_defs.ML \ 

43 
Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML \ 

44 
Isar/method.ML Isar/net_rules.ML Isar/object_logic.ML Isar/obtain.ML \ 

45 
Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML \ 

46 
Isar/outer_syntax.ML Isar/overloading.ML Isar/proof.ML \ 

47 
Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML \ 

48 
Isar/rule_cases.ML Isar/rule_insts.ML Isar/session.ML \ 

49 
Isar/skip_proof.ML Isar/spec_parse.ML Isar/specification.ML \ 

50 
Isar/subclass.ML Isar/theory_target.ML Isar/toplevel.ML \ 

28266  51 
MLSystems/alice.ML MLSystems/exn.ML MLSystems/ml_name_space.ML \ 
52 
MLSystems/multithreading.ML MLSystems/mosml.ML \ 

53 
MLSystems/multithreading_polyml.ML MLSystems/overloading_smlnj.ML \ 

54 
MLSystems/polyml4.1.3.ML MLSystems/polyml4.1.4.ML \ 

55 
MLSystems/polyml4.2.0.ML MLSystems/polyml5.0.ML \ 

56 
MLSystems/polyml5.1.ML MLSystems/polyml_common.ML \ 

57 
MLSystems/polyml.ML MLSystems/polyml_old_compiler4.ML \ 

27204  58 
MLSystems/polyml_old_compiler5.ML MLSystems/proper_int.ML \ 
59 
MLSystems/smlnj.ML MLSystems/system_shell.ML \ 

28146  60 
MLSystems/time_limit.ML MLSystems/thread_dummy.ML \ 
61 
MLSystems/universal.ML ML/ml_context.ML ML/ml_antiquote.ML \ 

62 
ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML ML/ml_thms.ML \ 

63 
Proof/extraction.ML Proof/proof_rewrite_rules.ML \ 

27339  64 
Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML \ 
65 
ProofGeneral/ROOT.ML ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML \ 

26097
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

66 
ProofGeneral/pgip_isabelle.ML ProofGeneral/pgip_markup.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

67 
ProofGeneral/pgip_output.ML ProofGeneral/pgip_parser.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

68 
ProofGeneral/pgip_tests.ML ProofGeneral/pgip_types.ML \ 
28030  69 
ProofGeneral/preferences.ML ProofGeneral/proof_general_emacs.ML \ 
26097
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

70 
ProofGeneral/proof_general_pgip.ML Pure.thy ROOT.ML Syntax/ast.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

71 
Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

72 
Syntax/printer.ML Syntax/simple_syntax.ML Syntax/syn_ext.ML \ 
943582a2d1e2
removed General/system_process.ML (back to multithreaded version);
wenzelm
parents:
26077
diff
changeset

73 
Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML Thy/html.ML \ 
26419
945d8d7a66ec
removed obsolete Thy/thm_database.ML (cf. ML/ml_context.ML);
wenzelm
parents:
26384
diff
changeset

74 
Thy/latex.ML Thy/present.ML Thy/term_style.ML Thy/thm_deps.ML \ 
945d8d7a66ec
removed obsolete Thy/thm_database.ML (cf. ML/ml_context.ML);
wenzelm
parents:
26384
diff
changeset

75 
Thy/thy_edit.ML Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML \ 
28266  76 
Thy/thy_output.ML Tools/ROOT.ML Tools/invoke.ML Tools/quickcheck.ML \ 
77 
Tools/value.ML Tools/isabelle_process.ML Tools/named_thms.ML \ 

78 
Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML config.ML \ 

28288
09c812966e7f
added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
28266
diff
changeset

79 
conjunction.ML consts.ML context.ML conv.ML defs.ML deriv.ML \ 
09c812966e7f
added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
28266
diff
changeset

80 
display.ML drule.ML envir.ML facts.ML goal.ML interpretation.ML \ 
09c812966e7f
added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
28266
diff
changeset

81 
library.ML logic.ML meta_simplifier.ML more_thm.ML morphism.ML \ 
09c812966e7f
added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
28266
diff
changeset

82 
name.ML net.ML old_goals.ML pattern.ML primitive_defs.ML \ 
09c812966e7f
added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
28266
diff
changeset

83 
proofterm.ML pure_setup.ML pure_thy.ML search.ML sign.ML \ 
09c812966e7f
added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
28266
diff
changeset

84 
simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML term.ML \ 
09c812966e7f
added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
28266
diff
changeset

85 
term_subst.ML theory.ML thm.ML type.ML type_infer.ML unify.ML \ 
09c812966e7f
added deriv.ML: Abstract derivations based on raw proof terms.
wenzelm
parents:
28266
diff
changeset

86 
variable.ML 
2431  87 
@./mk 
88 

4518  89 

10102  90 
## special targets 
91 

24880
c827d25b2983
added PureProofGeneral target (dummy session with outer syntax keyword initialization);
wenzelm
parents:
24830
diff
changeset

92 
PureProofGeneral: Pure $(LOG)/PureProofGeneral.gz 
c827d25b2983
added PureProofGeneral target (dummy session with outer syntax keyword initialization);
wenzelm
parents:
24830
diff
changeset

93 

27204  94 
$(LOG)/PureProofGeneral.gz: $(OUT)/Pure ProofGeneral/proof_general_keywords.ML 
24880
c827d25b2983
added PureProofGeneral target (dummy session with outer syntax keyword initialization);
wenzelm
parents:
24830
diff
changeset

95 
@$(ISATOOL) usedir f proof_general_keywords.ML $(OUT)/Pure ProofGeneral 
c827d25b2983
added PureProofGeneral target (dummy session with outer syntax keyword initialization);
wenzelm
parents:
24830
diff
changeset

96 

c827d25b2983
added PureProofGeneral target (dummy session with outer syntax keyword initialization);
wenzelm
parents:
24830
diff
changeset

97 

21995  98 
RAW: $(OUT)/RAW 
4518  99 

28266  100 
$(OUT)/RAW: MLSystems/alice.ML MLSystems/exn.ML \ 
101 
MLSystems/ml_name_space.ML MLSystems/multithreading.ML \ 

102 
MLSystems/mosml.ML MLSystems/multithreading_polyml.ML \ 

103 
MLSystems/overloading_smlnj.ML MLSystems/polyml4.1.3.ML \ 

104 
MLSystems/polyml4.1.4.ML MLSystems/polyml4.2.0.ML \ 

105 
MLSystems/polyml5.0.ML MLSystems/polyml5.1.ML \ 

106 
MLSystems/polyml_common.ML MLSystems/polyml.ML \ 

107 
MLSystems/polyml_old_compiler4.ML \ 

108 
MLSystems/polyml_old_compiler5.ML MLSystems/proper_int.ML \ 

109 
MLSystems/smlnj.ML MLSystems/system_shell.ML \ 

110 
MLSystems/time_limit.ML MLSystems/thread_dummy.ML \ 

28146  111 
MLSystems/universal.ML 
3774  112 
@./mk r 
113 

4518  114 

115 
## clean 

4441  116 

117 
clean: 

27204  118 
@rm f $(OUT)/Pure $(LOG)/Pure.gz $(LOG)/PureProofGeneral.gz \ 
24880
c827d25b2983
added PureProofGeneral target (dummy session with outer syntax keyword initialization);
wenzelm
parents:
24830
diff
changeset

119 
$(OUT)/RAW $(LOG)/RAW.gz 
27902  120 

121 

122 
## Scala material 

123 

27967  124 
SCALA_FILES = General/markup.scala General/position.scala \ 
125 
General/symbol.scala General/xml.scala General/yxml.scala \ 

126 
Tools/isabelle_process.scala Tools/isabelle_syntax.scala \ 

127 
Tools/isabelle_system.scala 

27950
dbb93a5e6e6a
added Tools/isabelle_process.scala, Tools/isabelle_syntax.scala;
wenzelm
parents:
27929
diff
changeset

128 

dbb93a5e6e6a
added Tools/isabelle_process.scala, Tools/isabelle_syntax.scala;
wenzelm
parents:
27929
diff
changeset

129 

27902  130 
SCALA_TARGET = $(ISABELLE_HOME)/lib/classes/Pure.jar 
131 

132 
jar: $(SCALA_TARGET) 

133 

134 
$(SCALA_TARGET): $(SCALA_FILES) 

135 
@rm rf classes && mkdir classes 

27950
dbb93a5e6e6a
added Tools/isabelle_process.scala, Tools/isabelle_syntax.scala;
wenzelm
parents:
27929
diff
changeset

136 
scalac deprecation d classes target jvm1.5 $(SCALA_FILES) 
27925  137 
scaladoc d classes $(SCALA_FILES) 
28295  138 
@cp $(SCALA_FILES) classes/isabelle 
27902  139 
@mkdir p `dirname $@` 
27922
ddf74e16ab01
jar target: removed jvmpath  does not work on Linux!?
wenzelm
parents:
27920
diff
changeset

140 
@cd classes; jar cf $@ isabelle 
28003  141 
@rm rf classes 
27902  142 

143 
cleanjar: 

144 
@rm f $(SCALA_TARGET) 