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