author  wenzelm 
Sun, 22 Mar 2009 19:11:00 +0100  
changeset 30639  fe40d740d7c1 
parent 30633  cc18ae3c1c7f 
child 30672  beaadd5af500 
permissions  rwrr 
2431  1 
# 
4518  2 
# IsaMakefile for Pure 
2431  3 
# 
4 

4518  5 
## targets 
6 

7 
default: Pure 

8 
images: Pure 

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

9 
test: RAW PureProofGeneral 
4518  10 
all: images test 
11 

12 

13 
## global settings 

14 

15 
SRC = $(ISABELLE_HOME)/src 

3118  16 
OUT = $(ISABELLE_OUTPUT) 
4518  17 
LOG = $(OUT)/log 
18 

2431  19 

4518  20 
## Pure 
21 

30189
3633f560f4c3
discontinued experimental support for Alice  too hard to maintain its many language incompatibilities, never really worked anyway;
wenzelm
parents:
30178
diff
changeset

22 
BOOTSTRAP_FILES = MLSystems/exn.ML MLSystems/ml_name_space.ML \ 
30619  23 
MLSystems/ml_pretty.ML MLSystems/mosml.ML \ 
24 
MLSystems/multithreading.ML MLSystems/multithreading_polyml.ML \ 

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

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

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

28 
MLSystems/polymlexperimental.ML MLSystems/polyml.ML \ 

29 
MLSystems/polyml_common.ML MLSystems/polyml_old_compiler4.ML \ 

30627
fb9e73c01603
added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
30619
diff
changeset

30 
MLSystems/polyml_old_compiler5.ML MLSystems/polyml_pp.ML \ 
fb9e73c01603
added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
30619
diff
changeset

31 
MLSystems/proper_int.ML MLSystems/smlnj.ML \ 
fb9e73c01603
added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
30619
diff
changeset

32 
MLSystems/system_shell.ML MLSystems/thread_dummy.ML \ 
fb9e73c01603
added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
wenzelm
parents:
30619
diff
changeset

33 
MLSystems/time_limit.ML MLSystems/universal.ML 
30141  34 

35 
RAW: $(OUT)/RAW 

36 

37 
$(OUT)/RAW: $(BOOTSTRAP_FILES) 

38 
@./mk r 

39 

40 

27204  41 
Pure: $(OUT)/Pure 
2431  42 

30141  43 
$(OUT)/Pure: $(BOOTSTRAP_FILES) ../Tools/auto_solve.ML \ 
44 
../Tools/quickcheck.ML Concurrent/ROOT.ML Concurrent/future.ML \ 

28632  45 
Concurrent/mailbox.ML Concurrent/par_list.ML \ 
29118  46 
Concurrent/par_list_dummy.ML Concurrent/simple_thread.ML \ 
47 
Concurrent/synchronized.ML Concurrent/task_queue.ML General/ROOT.ML \ 

30587
ad19c99529eb
moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
wenzelm
parents:
30559
diff
changeset

48 
General/alist.ML General/antiquote.ML General/balanced_tree.ML \ 
ad19c99529eb
moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
wenzelm
parents:
30559
diff
changeset

49 
General/basics.ML General/binding.ML General/buffer.ML \ 
ad19c99529eb
moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
wenzelm
parents:
30559
diff
changeset

50 
General/file.ML General/graph.ML General/heap.ML General/integer.ML \ 
ad19c99529eb
moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
wenzelm
parents:
30559
diff
changeset

51 
General/lazy.ML General/long_name.ML General/markup.ML \ 
ad19c99529eb
moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
wenzelm
parents:
30559
diff
changeset

52 
General/name_space.ML General/ord_list.ML General/output.ML \ 
ad19c99529eb
moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
wenzelm
parents:
30559
diff
changeset

53 
General/path.ML General/position.ML General/pretty.ML \ 
ad19c99529eb
moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
wenzelm
parents:
30559
diff
changeset

54 
General/print_mode.ML General/properties.ML General/queue.ML \ 
ad19c99529eb
moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
wenzelm
parents:
30559
diff
changeset

55 
General/scan.ML General/secure.ML General/seq.ML General/source.ML \ 
ad19c99529eb
moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
wenzelm
parents:
30559
diff
changeset

56 
General/stack.ML General/symbol.ML General/symbol_pos.ML \ 
ad19c99529eb
moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
wenzelm
parents:
30559
diff
changeset

57 
General/table.ML General/url.ML General/xml.ML General/yxml.ML \ 
ad19c99529eb
moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
wenzelm
parents:
30559
diff
changeset

58 
Isar/ROOT.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML \ 
30360  59 
Isar/calculation.ML Isar/class.ML Isar/class_target.ML Isar/code.ML \ 
60 
Isar/code_unit.ML Isar/constdefs.ML Isar/context_rules.ML \ 

61 
Isar/element.ML Isar/expression.ML Isar/isar_cmd.ML \ 

62 
Isar/isar_document.ML Isar/isar_syn.ML Isar/local_defs.ML \ 

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

30559
e5987a7ac5df
turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents:
30360
diff
changeset

64 
Isar/method.ML Isar/object_logic.ML Isar/obtain.ML \ 
30360  65 
Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML \ 
66 
Isar/outer_syntax.ML Isar/overloading.ML Isar/proof.ML \ 

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

68 
Isar/rule_cases.ML Isar/rule_insts.ML Isar/skip_proof.ML \ 

69 
Isar/spec_parse.ML Isar/specification.ML Isar/theory_target.ML \ 

70 
Isar/toplevel.ML Isar/value_parse.ML ML/ml_antiquote.ML \ 

71 
ML/ml_context.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML \ 

30639
fe40d740d7c1
ML/ml_test.ML: test of advanced ML compiler invocation in Poly/ML 5.3;
wenzelm
parents:
30633
diff
changeset

72 
ML/ml_test.ML ML/ml_thms.ML MLSystems/install_pp_polyml.ML \ 
30633
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
30627
diff
changeset

73 
MLSystems/install_pp_polymlexperimental.ML Proof/extraction.ML \ 
30141  74 
Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \ 
75 
Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/ROOT.ML \ 

76 
ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML \ 

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

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

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

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

81 
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

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

83 
Syntax/printer.ML Syntax/simple_syntax.ML Syntax/syn_ext.ML \ 
30173
eabece26b89b
moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents:
30142
diff
changeset

84 
Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML \ 
eabece26b89b
moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents:
30142
diff
changeset

85 
System/isabelle_process.ML System/isar.ML System/session.ML \ 
eabece26b89b
moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents:
30142
diff
changeset

86 
Thy/html.ML Thy/latex.ML Thy/present.ML Thy/term_style.ML \ 
eabece26b89b
moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents:
30142
diff
changeset

87 
Thy/thm_deps.ML Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML \ 
eabece26b89b
moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents:
30142
diff
changeset

88 
Thy/thy_output.ML Thy/thy_syntax.ML Tools/ROOT.ML \ 
eabece26b89b
moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents:
30142
diff
changeset

89 
Tools/find_consts.ML Tools/find_theorems.ML Tools/named_thms.ML \ 
30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
30141
diff
changeset

90 
Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML config.ML \ 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
30141
diff
changeset

91 
conjunction.ML consts.ML context.ML context_position.ML conv.ML \ 
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
30141
diff
changeset

92 
defs.ML display.ML drule.ML envir.ML facts.ML goal.ML \ 
30559
e5987a7ac5df
turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents:
30360
diff
changeset

93 
interpretation.ML item_net.ML library.ML logic.ML meta_simplifier.ML \ 
e5987a7ac5df
turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents:
30360
diff
changeset

94 
more_thm.ML morphism.ML name.ML net.ML old_goals.ML old_term.ML \ 
e5987a7ac5df
turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents:
30360
diff
changeset

95 
pattern.ML primitive_defs.ML proofterm.ML pure_setup.ML pure_thy.ML \ 
e5987a7ac5df
turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents:
30360
diff
changeset

96 
search.ML sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML \ 
e5987a7ac5df
turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents:
30360
diff
changeset

97 
tctical.ML term.ML term_ord.ML term_subst.ML theory.ML thm.ML \ 
e5987a7ac5df
turned structure NetRules into general Item_Net, which is loaded earlier;
wenzelm
parents:
30360
diff
changeset

98 
type.ML type_infer.ML unify.ML variable.ML 
2431  99 
@./mk 
100 

4518  101 

30141  102 
## Proof General keywords 
10102  103 

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

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

105 

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

108 

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

109 

4518  110 
## clean 
4441  111 

112 
clean: 

30141  113 
@rm f $(OUT)/Pure $(LOG)/Pure.gz $(OUT)/RAW $(LOG)/RAW.gz \ 
114 
$(LOG)/PureProofGeneral.gz 

27902  115 

116 

117 
## Scala material 

118 

29202  119 
SCALA_FILES = General/event_bus.scala General/markup.scala \ 
120 
General/position.scala General/swing.scala General/symbol.scala \ 

121 
General/xml.scala General/yxml.scala Isar/isar.scala \ 

29553  122 
Isar/isar_document.scala Isar/outer_keyword.scala \ 
30174  123 
System/isabelle_process.scala System/isabelle_system.scala \ 
124 
Thy/thy_header.scala Tools/isabelle_syntax.scala 

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

125 

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

126 

27902  127 
SCALA_TARGET = $(ISABELLE_HOME)/lib/classes/Pure.jar 
128 

129 
jar: $(SCALA_TARGET) 

130 

131 
$(SCALA_TARGET): $(SCALA_FILES) 

132 
@rm rf classes && mkdir classes 

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

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

137 
@cd classes; jar cf $@ isabelle 
28003  138 
@rm rf classes 
27902  139 

140 
cleanjar: 

141 
@rm f $(SCALA_TARGET) 