0
|
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\
|
57
|
25 |
drule.ML tctical.ML tactic.ML goals.ML install_pp.ML
|
0
|
26 |
|
|
27 |
SYNTAX_FILES = Syntax/ROOT.ML Syntax/ast.ML Syntax/xgram.ML\
|
223
|
28 |
Syntax/extension.ML Syntax/lexicon.ML\
|
57
|
29 |
Syntax/parser.ML Syntax/type_ext.ML Syntax/sextension.ML\
|
|
30 |
Syntax/pretty.ML Syntax/printer.ML Syntax/syntax.ML\
|
|
31 |
Syntax/earley0A.ML
|
0
|
32 |
|
|
33 |
THY_FILES = Thy/ROOT.ML Thy/scan.ML Thy/parse.ML Thy/syntax.ML Thy/read.ML
|
|
34 |
|
|
35 |
#Uses cp rather than make_database because Poly/ML allows only 3 levels
|
|
36 |
$(BIN)/Pure: $(FILES) $(SYNTAX_FILES) $(THY_FILES) $(ML_DBASE)
|
|
37 |
case "$(COMP)" in \
|
|
38 |
poly*) echo database=$${ML_DBASE:?'No Poly/ML database specified'};\
|
|
39 |
cp $(ML_DBASE) $(BIN)/Pure; chmod u+w $(BIN)/Pure;\
|
|
40 |
echo 'PolyML.use"POLY";use"ROOT";' | $(COMP) $(BIN)/Pure;;\
|
|
41 |
sml*) if [ ! '(' -d $${ISABELLEBIN:?} -a -w $${ISABELLEBIN:?} ')' ];\
|
|
42 |
then echo Bad value for ISABELLEBIN : \
|
|
43 |
$(BIN) is not a writable directory; \
|
|
44 |
exit 1; \
|
|
45 |
fi;\
|
|
46 |
echo 'use"NJ.ML"; use"ROOT.ML"; xML"$(BIN)/Pure" banner;'\
|
|
47 |
| $(COMP);;\
|
|
48 |
*) echo Bad value for ISABELLECOMP;;\
|
|
49 |
esac
|
|
50 |
|
|
51 |
.PRECIOUS: $(BIN)/Pure
|