author | clasohm |
Sun, 17 Oct 1993 18:03:47 +0100 | |
changeset 60 | 379872528c16 |
parent 0 | a5a9c433f639 |
child 102 | e04cb6295a3f |
permissions | -rw-r--r-- |
0 | 1 |
######################################################################### |
2 |
# # |
|
3 |
# Makefile for Isabelle (Modal) # |
|
4 |
# # |
|
5 |
######################################################################### |
|
6 |
||
7 |
#To make the system, cd to this directory and type |
|
8 |
# make -f Makefile |
|
9 |
#To make the system and test it on standard examples, type |
|
10 |
# make -f Makefile test |
|
11 |
||
12 |
#Environment variable ISABELLECOMP specifies the compiler. |
|
13 |
#Environment variable ISABELLEBIN specifies the destination directory. |
|
14 |
#For Poly/ML, ISABELLEBIN must begin with a / |
|
15 |
||
16 |
#Makes LK if this file is ABSENT -- but not |
|
17 |
#if it is out of date, since this Makefile does not know its dependencies! |
|
18 |
||
19 |
BIN = $(ISABELLEBIN) |
|
20 |
COMP = $(ISABELLECOMP) |
|
60
379872528c16
renamed: S4.thy to s4.thy, S43.thy to s43.thy, T.thy to t.thy
clasohm
parents:
0
diff
changeset
|
21 |
FILES = ROOT.ML modal0.thy prover.ML t.thy s4.thy s43.thy |
0 | 22 |
|
23 |
#Uses cp rather than make_database because Poly/ML allows only 3 levels |
|
24 |
$(BIN)/Modal: $(BIN)/LK $(FILES) |
|
25 |
case "$(COMP)" in \ |
|
26 |
poly*) cp $(BIN)/LK $(BIN)/Modal;\ |
|
27 |
echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/Modal ;;\ |
|
28 |
sml*) echo 'use"ROOT.ML"; xML"$(BIN)/Modal" banner;' | $(BIN)/LK;;\ |
|
29 |
*) echo Bad value for ISABELLECOMP;;\ |
|
30 |
esac |
|
31 |
||
32 |
$(BIN)/LK: |
|
33 |
cd ../LK; $(MAKE) |
|
34 |
||
35 |
test: ex/ROOT.ML $(BIN)/Modal |
|
36 |
case "$(COMP)" in \ |
|
37 |
poly*) echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/Modal ;;\ |
|
38 |
sml*) echo 'use"ex/ROOT.ML";' | $(BIN)/Modal;;\ |
|
39 |
*) echo Bad value for ISABELLECOMP;;\ |
|
40 |
esac |
|
41 |
||
42 |
.PRECIOUS: $(BIN)/LK $(BIN)/Modal |