|
1 ######################################################################### |
|
2 # # |
|
3 # Makefile for Isabelle (Pure) # |
|
4 # # |
|
5 ######################################################################### |
|
6 |
|
7 #The pure part is common to all systems. |
|
8 #Object-logics (like FOL) are loaded on top of it. |
|
9 |
|
10 #To make the system, cd to this directory and type |
|
11 # make -f Makefile |
|
12 |
|
13 #Environment variable ML_DBASE specifies the initial Poly/ML database, from |
|
14 # the Poly/ML distribution directory. |
|
15 #WARNING: Poly/ML parent databases should not be moved! |
|
16 |
|
17 #Environment variable ISABELLECOMP specifies the compiler. |
|
18 #Environment variable ISABELLEBIN specifies the destination directory. |
|
19 #For Poly/ML, ISABELLEBIN must begin with a / |
|
20 |
|
21 BIN = $(ISABELLEBIN) |
|
22 COMP = $(ISABELLECOMP) |
|
23 FILES = POLY.ML NJ.ML ROOT.ML library.ML term.ML symtab.ML type.ML sign.ML\ |
|
24 sequence.ML envir.ML pattern.ML unify.ML logic.ML thm.ML net.ML\ |
|
25 drule.ML tctical.ML tactic.ML goals.ML |
|
26 |
|
27 SYNTAX_FILES = Syntax/ROOT.ML Syntax/ast.ML Syntax/xgram.ML\ |
|
28 Syntax/extension.ML Syntax/lexicon.ML Syntax/parse_tree.ML\ |
|
29 Syntax/earley0A.ML Syntax/type_ext.ML Syntax/sextension.ML\ |
|
30 Syntax/pretty.ML Syntax/printer.ML Syntax/syntax.ML |
|
31 |
|
32 THY_FILES = Thy/ROOT.ML Thy/scan.ML Thy/parse.ML Thy/syntax.ML Thy/read.ML |
|
33 |
|
34 #Uses cp rather than make_database because Poly/ML allows only 3 levels |
|
35 $(BIN)/Pure: $(FILES) $(SYNTAX_FILES) $(THY_FILES) $(ML_DBASE) |
|
36 case "$(COMP)" in \ |
|
37 poly*) echo database=$${ML_DBASE:?'No Poly/ML database specified'};\ |
|
38 cp $(ML_DBASE) $(BIN)/Pure; chmod u+w $(BIN)/Pure;\ |
|
39 echo 'PolyML.use"POLY";use"ROOT";' | $(COMP) $(BIN)/Pure;;\ |
|
40 sml*) if [ ! '(' -d $${ISABELLEBIN:?} -a -w $${ISABELLEBIN:?} ')' ];\ |
|
41 then echo Bad value for ISABELLEBIN : \ |
|
42 $(BIN) is not a writable directory; \ |
|
43 exit 1; \ |
|
44 fi;\ |
|
45 echo 'use"NJ.ML"; use"ROOT.ML"; xML"$(BIN)/Pure" banner;'\ |
|
46 | $(COMP);;\ |
|
47 *) echo Bad value for ISABELLECOMP;;\ |
|
48 esac |
|
49 |
|
50 .PRECIOUS: $(BIN)/Pure |