| author | lcp |
| Tue, 09 Nov 1993 16:32:24 +0100 | |
| changeset 102 | e04cb6295a3f |
| parent 0 | a5a9c433f639 |
| child 338 | e3489bc1f857 |
| permissions | -rw-r--r-- |
| clasohm@0 | 1 |
######################################################################### |
| clasohm@0 | 2 |
# # |
| clasohm@0 | 3 |
# Makefile for Isabelle (LCF) # |
| 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 |
| clasohm@0 | 9 |
#To make the system and test it on standard examples, type |
| clasohm@0 | 10 |
# make 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 FOL 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) |
| lcp@102 | 21 |
FILES = ROOT.ML lcf.thy lcf.ML simpdata.ML pair.ML fix.ML |
| clasohm@0 | 22 |
|
| clasohm@0 | 23 |
#Uses cp rather than make_database because Poly/ML allows only 3 levels |
| clasohm@0 | 24 |
$(BIN)/LCF: $(BIN)/FOL $(FILES) |
| clasohm@0 | 25 |
case "$(COMP)" in \ |
| clasohm@0 | 26 |
poly*) cp $(BIN)/FOL $(BIN)/LCF;\ |
| clasohm@0 | 27 |
echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/LCF ;;\ |
| clasohm@0 | 28 |
sml*) echo 'use"ROOT.ML"; xML"$(BIN)/LCF" banner;' | $(BIN)/FOL;;\ |
| clasohm@0 | 29 |
*) echo Bad value for ISABELLECOMP;;\ |
| clasohm@0 | 30 |
esac |
| clasohm@0 | 31 |
|
| clasohm@0 | 32 |
(BIN)/FOL: |
| clasohm@0 | 33 |
cd ../FOL; $(MAKE) |
| clasohm@0 | 34 |
|
| clasohm@0 | 35 |
test: ex.ML $(BIN)/LCF |
| clasohm@0 | 36 |
case "$(COMP)" in \ |
| clasohm@0 | 37 |
poly*) echo 'use"ex.ML"; quit();' | $(COMP) $(BIN)/LCF ;;\ |
| clasohm@0 | 38 |
sml*) echo 'use"ex.ML";' | $(BIN)/LCF;;\ |
| clasohm@0 | 39 |
*) echo Bad value for ISABELLECOMP;;\ |
| clasohm@0 | 40 |
esac |
| clasohm@0 | 41 |
|
| clasohm@0 | 42 |
.PRECIOUS: $(BIN)/FOL $(BIN)/LCF |