author | lcp |
Wed, 27 Apr 1994 11:27:33 +0200 | |
changeset 346 | 216bc2ea1294 |
parent 338 | e3489bc1f857 |
child 468 | 3dd1dcb509ac |
permissions | -rw-r--r-- |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
1 |
############################################################################ |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
2 |
# # |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
3 |
# Makefile for Isabelle (HOLCF) # |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
4 |
# # |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
5 |
############################################################################ |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
6 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
7 |
#To make the system, cd to this directory and type |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
8 |
# make -f Makefile |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
9 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
10 |
#Environment variable ISABELLECOMP specifies the compiler. |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
11 |
#Environment variable ISABELLEBIN specifies the destination directory. |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
12 |
#For Poly/ML, ISABELLEBIN must begin with a / |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
13 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
14 |
#Makes HOL Isabelle if this file is ABSENT -- but not |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
15 |
#if it is out of date, since this Makefile does not know its dependencies! |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
16 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
17 |
BIN = $(ISABELLEBIN) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
18 |
COMP = $(ISABELLECOMP) |
346 | 19 |
FILES = ROOT.ML Holcfb.thy Holcfb.ML Void.thy Void.ML \ |
20 |
Porder0.thy Porder.thy Porder.ML Pcpo.thy \ |
|
338 | 21 |
Pcpo.ML Fun1.thy Fun1.ML Fun2.thy Fun2.ML Fun3.thy Fun3.ML \ |
22 |
Cfun1.thy Cfun1.ML Cfun2.thy Cfun2.ML Cfun3.thy Cfun3.ML \ |
|
346 | 23 |
Cont.thy Cont.ML cinfix.ML\ |
24 |
Cprod1.thy Cprod1.ML Cprod2.thy Cprod2.ML Cprod3.thy Cprod3.ML \ |
|
338 | 25 |
Sprod0.thy Sprod0.ML Sprod1.thy Sprod1.ML Sprod2.thy Sprod2.ML\ |
346 | 26 |
Sprod3.thy Sprod3.ML\ |
27 |
Ssum0.thy Ssum0.ML Ssum1.thy Ssum1.ML Ssum2.thy Ssum2.ML\ |
|
28 |
Ssum3.thy Ssum3.ML\ |
|
29 |
Lift1.thy Lift1.ML Lift2.thy Lift2.ML Lift3.thy Lift3.ML \ |
|
30 |
Fix.thy Fix.ML ccc1.thy ccc1.ML One.thy One.ML \ |
|
31 |
Tr1.thy Tr1.ML Tr2.thy Tr2.ML HOLCF.thy HOLCF.ML \ |
|
32 |
Dnat.thy Dnat.ML Dnat2.thy Dnat2.ML \ |
|
33 |
Stream.thy Stream.ML Stream2.thy Stream2.ML Dlist.thy Dlist.ML |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
34 |
|
346 | 35 |
EX_FILES = ex/Coind.thy ex/Coind.ML ex/Hoare.thy ex/Hoare.ML \ |
36 |
ex/Loop.thy ex/Loop.ML ex/Dagstuhl.thy ex/Dagstuhl.ML |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
37 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
38 |
$(BIN)/HOLCF: $(BIN)/HOL $(FILES) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
39 |
case "$(COMP)" in \ |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
40 |
poly*) echo 'make_database"$(BIN)/HOLCF"; quit();' \ |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
41 |
| $(COMP) $(BIN)/HOL ;\ |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
42 |
echo 'use"ROOT";' | $(COMP) $(BIN)/HOLCF ;;\ |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
43 |
sml*) echo 'use"ROOT.ML"; xML"$(BIN)/HOLCF" banner;' | $(BIN)/HOL ;;\ |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
44 |
*) echo Bad value for ISABELLECOMP;;\ |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
45 |
esac |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
46 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
47 |
$(BIN)/HOL: |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
48 |
cd ../HOL; $(MAKE) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
49 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
50 |
test: ex/ROOT.ML $(BIN)/HOLCF $(EX_FILES) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
51 |
case "$(COMP)" in \ |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
52 |
poly*) echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/HOLCF ;;\ |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
53 |
sml*) echo 'use"ex/ROOT.ML"' | $(BIN)/HOLCF;;\ |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
54 |
*) echo Bad value for ISABELLECOMP;;\ |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
55 |
esac |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
56 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
57 |
.PRECIOUS: $(BIN)/HOL $(BIN)/HOLCF |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
58 |