author | wenzelm |
Mon, 09 Dec 1996 16:05:41 +0100 | |
changeset 2339 | 2d5551c8dec0 |
parent 2235 | 866dbb04816c |
child 2692 | 484ec6ca0c50 |
permissions | -rw-r--r-- |
1012 | 1 |
# $Id$ |
0 | 2 |
######################################################################### |
3 |
# # |
|
2094 | 4 |
# Makefile for Isabelle (Pure) # |
0 | 5 |
# # |
6 |
######################################################################### |
|
7 |
||
8 |
#The pure part is common to all systems. |
|
9 |
#Object-logics (like FOL) are loaded on top of it. |
|
10 |
||
11 |
#To make the system, cd to this directory and type |
|
12 |
# make -f Makefile |
|
13 |
||
14 |
#Environment variable ML_DBASE specifies the initial Poly/ML database, from |
|
15 |
# the Poly/ML distribution directory. |
|
16 |
#WARNING: Poly/ML parent databases should not be moved! |
|
17 |
||
18 |
#Environment variable ISABELLECOMP specifies the compiler. |
|
19 |
#Environment variable ISABELLEBIN specifies the destination directory. |
|
20 |
#For Poly/ML, ISABELLEBIN must begin with a / |
|
21 |
||
22 |
BIN = $(ISABELLEBIN) |
|
23 |
COMP = $(ISABELLECOMP) |
|
2235
866dbb04816c
Makefile improvements by Thomas Santen and Stephan Herrmann
paulson
parents:
2195
diff
changeset
|
24 |
FILES = POLY.ML NJ.ML NJ093.ML NJ1xx.ML ROOT.ML basis.ML library.ML\ |
866dbb04816c
Makefile improvements by Thomas Santen and Stephan Herrmann
paulson
parents:
2195
diff
changeset
|
25 |
term.ML symtab.ML type.ML sign.ML\ |
1527 | 26 |
sequence.ML envir.ML pattern.ML unify.ML logic.ML theory.ML thm.ML\ |
1594 | 27 |
net.ML display.ML deriv.ML drule.ML tctical.ML search.ML tactic.ML\ |
2094 | 28 |
goals.ML axclass.ML install_pp.ML\ |
29 |
NJ093.ML NJ1xx.ML ../Provers/simplifier.ML |
|
0 | 30 |
|
2094 | 31 |
SYNTAX_FILES = Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML\ |
566 | 32 |
Syntax/parser.ML Syntax/type_ext.ML Syntax/syn_trans.ML\ |
57 | 33 |
Syntax/pretty.ML Syntax/printer.ML Syntax/syntax.ML\ |
2195 | 34 |
Syntax/syn_ext.ML Syntax/mixfix.ML Syntax/symbol_font.ML |
0 | 35 |
|
415
e5470bf81350
added axclass.ML, Syntax/mixfix.ML, Thy/thy_syn.ML;
wenzelm
parents:
408
diff
changeset
|
36 |
THY_FILES = Thy/ROOT.ML Thy/thy_scan.ML Thy/thy_parse.ML\ |
1140 | 37 |
Thy/thy_syn.ML Thy/thy_read.ML Thy/thm_database.ML |
0 | 38 |
|
39 |
#Uses cp rather than make_database because Poly/ML allows only 3 levels |
|
2094 | 40 |
$(BIN)/Pure: $(FILES) $(SYNTAX_FILES) $(THY_FILES) $(ML_DBASE) |
2235
866dbb04816c
Makefile improvements by Thomas Santen and Stephan Herrmann
paulson
parents:
2195
diff
changeset
|
41 |
@case `basename "$(COMP)"` in \ |
0 | 42 |
poly*) echo database=$${ML_DBASE:?'No Poly/ML database specified'};\ |
43 |
cp $(ML_DBASE) $(BIN)/Pure; chmod u+w $(BIN)/Pure;\ |
|
1480 | 44 |
echo 'PolyML.use"POLY";use"ROOT" handle _=> exit 1;' \ |
2094 | 45 |
| $(COMP) $(BIN)/Pure;\ |
2023
aa25f20c5d8b
Calls discgarb -c to realize dramatic space savings!
paulson
parents:
1671
diff
changeset
|
46 |
discgarb -c $(BIN)/Pure;;\ |
0 | 47 |
sml*) if [ ! '(' -d $${ISABELLEBIN:?} -a -w $${ISABELLEBIN:?} ')' ];\ |
2094 | 48 |
then echo Bad value for ISABELLEBIN: \ |
49 |
$(BIN) is not a writable directory; \ |
|
50 |
exit 1; \ |
|
51 |
fi;\ |
|
52 |
echo 'use"NJ.ML"; use"ROOT.ML" handle _=> exit 1; xML"$(BIN)/Pure" banner;' | $(COMP);;\ |
|
2235
866dbb04816c
Makefile improvements by Thomas Santen and Stephan Herrmann
paulson
parents:
2195
diff
changeset
|
53 |
*) echo Bad value for ISABELLECOMP: $(COMP); \ |
866dbb04816c
Makefile improvements by Thomas Santen and Stephan Herrmann
paulson
parents:
2195
diff
changeset
|
54 |
echo " " \"`basename "$(COMP)"`\" is not poly or sml;;\ |
0 | 55 |
esac |
56 |
||
1671 | 57 |
|
58 |
test: $(BIN)/Pure |
|
59 |
||
2094 | 60 |
.PRECIOUS: $(BIN)/Pure |