1 # |
1 # |
2 # $Id$ |
2 # $Id$ |
3 # |
3 # |
4 # IsaMakefile for Pure Isabelle |
4 # IsaMakefile for Pure |
5 # |
|
6 # The Pure part is common to all systems. Object-logics (like FOL) |
|
7 # are loaded on top of it. |
|
8 # |
5 # |
9 |
6 |
|
7 ## targets |
|
8 |
|
9 default: Pure |
|
10 images: Pure |
|
11 test: |
|
12 all: images test |
|
13 |
|
14 |
|
15 ## global settings |
|
16 |
|
17 SRC = $(ISABELLE_HOME)/src |
10 OUT = $(ISABELLE_OUTPUT) |
18 OUT = $(ISABELLE_OUTPUT) |
|
19 LOG = $(OUT)/log |
11 |
20 |
12 FILES = ML-Systems/mlworks.ML ML-Systems/polyml.ML ML-Systems/smlnj-0.93.ML \ |
|
13 ML-Systems/smlnj.ML ROOT.ML Syntax/ROOT.ML Syntax/ast.ML \ |
|
14 Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML Syntax/pretty.ML \ |
|
15 Syntax/printer.ML Syntax/symbol_font.ML Syntax/syn_ext.ML \ |
|
16 Syntax/syn_trans.ML Syntax/syntax.ML Syntax/token_trans.ML \ |
|
17 Syntax/type_ext.ML Thy/ROOT.ML Thy/browser_info.ML Thy/context.ML Thy/file.ML \ |
|
18 Thy/path.ML Thy/thm_database.ML Thy/thy_info.ML Thy/thy_parse.ML \ |
|
19 Thy/thy_read.ML Thy/thy_scan.ML Thy/thy_syn.ML Thy/use.ML \ |
|
20 axclass.ML basis.ML deriv.ML display.ML drule.ML envir.ML \ |
|
21 goals.ML install_pp.ML library.ML logic.ML name_space.ML net.ML \ |
|
22 pattern.ML pure_thy.ML search.ML section_utils.ML seq.ML sign.ML \ |
|
23 sorts.ML table.ML tactic.ML tctical.ML term.ML theory.ML thm.ML \ |
|
24 type.ML type_infer.ML unify.ML |
|
25 |
21 |
26 $(OUT)/Pure: $(FILES) |
22 ## Pure |
|
23 |
|
24 Pure: $(OUT)/Pure |
|
25 |
|
26 $(OUT)/Pure: ML-Systems/mlworks.ML ML-Systems/polyml.ML \ |
|
27 ML-Systems/smlnj-0.93.ML ML-Systems/smlnj.ML ROOT.ML Syntax/ROOT.ML \ |
|
28 Syntax/ast.ML Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML \ |
|
29 Syntax/pretty.ML Syntax/printer.ML Syntax/symbol_font.ML \ |
|
30 Syntax/syn_ext.ML Syntax/syn_trans.ML Syntax/syntax.ML \ |
|
31 Syntax/token_trans.ML Syntax/type_ext.ML Thy/ROOT.ML \ |
|
32 Thy/browser_info.ML Thy/context.ML Thy/file.ML Thy/path.ML \ |
|
33 Thy/thm_database.ML Thy/thy_info.ML Thy/thy_parse.ML Thy/thy_read.ML \ |
|
34 Thy/thy_scan.ML Thy/thy_syn.ML Thy/use.ML axclass.ML basis.ML deriv.ML \ |
|
35 display.ML drule.ML envir.ML goals.ML install_pp.ML library.ML \ |
|
36 logic.ML name_space.ML net.ML pattern.ML pure_thy.ML search.ML \ |
|
37 section_utils.ML seq.ML sign.ML sorts.ML table.ML tactic.ML tctical.ML \ |
|
38 term.ML theory.ML thm.ML type.ML type_infer.ML unify.ML |
27 @./mk |
39 @./mk |
28 |
40 |
29 RAW: $(FILES) |
41 |
|
42 ## RAW |
|
43 |
|
44 RAW: |
30 @./mk -r |
45 @./mk -r |
31 |
46 |
32 test: $(OUT)/Pure |
47 |
|
48 ## clean |
33 |
49 |
34 clean: |
50 clean: |
35 @rm -f $(OUT)/Pure $(OUT)/RAW |
51 @rm -f $(OUT)/Pure $(LOG)/Pure.gz $(OUT)/RAW $(LOG)/RAW.gz |
36 |
|
37 |
|
38 .PRECIOUS: $(OUT)/Pure $(OUT)/RAW |
|