author | paulson |
Mon, 21 Oct 1996 11:18:34 +0200 | |
changeset 2117 | 292df12bace5 |
parent 2094 | 2061df98aab5 |
child 2235 | 866dbb04816c |
permissions | -rw-r--r-- |
1307 | 1 |
# $Id$ |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
2 |
############################################################################ |
2094 | 3 |
# # |
4 |
# Makefile for Isabelle (HOLCF) # |
|
5 |
# # |
|
243
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 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
8 |
#To make the system, cd to this directory and type |
1307 | 9 |
# make |
10 |
#To make the system and test it on standard examples, type |
|
11 |
# make test |
|
12 |
#To generate HTML files for every theory, set the environment variable |
|
13 |
#MAKE_HTML or add the parameter "MAKE_HTML=". |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
14 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
15 |
#Environment variable ISABELLECOMP specifies the compiler. |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
16 |
#Environment variable ISABELLEBIN specifies the destination directory. |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
17 |
#For Poly/ML, ISABELLEBIN must begin with a / |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
18 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
19 |
#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
|
20 |
#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
|
21 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
22 |
BIN = $(ISABELLEBIN) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
23 |
COMP = $(ISABELLECOMP) |
918
7ecdff86a5f0
Uses "suffix substitution" to shorten macro definitions.
lcp
parents:
752
diff
changeset
|
24 |
THYS = Holcfb.thy Void.thy Porder.thy Pcpo.thy \ |
7ecdff86a5f0
Uses "suffix substitution" to shorten macro definitions.
lcp
parents:
752
diff
changeset
|
25 |
Fun1.thy Fun2.thy Fun3.thy \ |
7ecdff86a5f0
Uses "suffix substitution" to shorten macro definitions.
lcp
parents:
752
diff
changeset
|
26 |
Cfun1.thy Cfun2.thy Cfun3.thy Cont.thy \ |
7ecdff86a5f0
Uses "suffix substitution" to shorten macro definitions.
lcp
parents:
752
diff
changeset
|
27 |
Cprod1.thy Cprod2.thy Cprod3.thy \ |
7ecdff86a5f0
Uses "suffix substitution" to shorten macro definitions.
lcp
parents:
752
diff
changeset
|
28 |
Sprod0.thy Sprod1.thy Sprod2.thy Sprod3.thy \ |
7ecdff86a5f0
Uses "suffix substitution" to shorten macro definitions.
lcp
parents:
752
diff
changeset
|
29 |
Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \ |
7ecdff86a5f0
Uses "suffix substitution" to shorten macro definitions.
lcp
parents:
752
diff
changeset
|
30 |
Lift1.thy Lift2.thy Lift3.thy Fix.thy ccc1.thy One.thy \ |
1274 | 31 |
Tr1.thy Tr2.thy HOLCF.thy |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
32 |
|
918
7ecdff86a5f0
Uses "suffix substitution" to shorten macro definitions.
lcp
parents:
752
diff
changeset
|
33 |
FILES = ROOT.ML Porder0.thy $(THYS) $(THYS:.thy=.ML) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
34 |
|
1307 | 35 |
#Uses cp rather than make_database because Poly/ML allows only 3 levels |
2094 | 36 |
$(BIN)/HOLCF: $(BIN)/HOL $(FILES) |
2117 | 37 |
@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \ |
2094 | 38 |
poly*) cp $(BIN)/HOL $(BIN)/HOLCF; chmod u+w $(BIN)/HOLCF;\ |
39 |
if [ "$${MAKE_HTML}" = "true" ]; \ |
|
40 |
then echo 'open PolyML; make_html := true; exit_use_dir".";' \ |
|
41 |
| $(COMP) $(BIN)/HOLCF;\ |
|
1491 | 42 |
elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
2094 | 43 |
then echo 'open PolyML; make_html := true; exit_use_dir"."; make_html := false;' | $(COMP) $(BIN)/HOLCF;\ |
44 |
else echo 'open PolyML; exit_use_dir".";' \ |
|
1307 | 45 |
| $(COMP) $(BIN)/HOLCF;\ |
2094 | 46 |
fi;\ |
2023
aa25f20c5d8b
Calls discgarb -c to realize dramatic space savings!
paulson
parents:
1675
diff
changeset
|
47 |
discgarb -c $(BIN)/HOLCF;;\ |
1491 | 48 |
sml*) if [ "$${MAKE_HTML}" = "true" ]; \ |
2094 | 49 |
then echo 'make_html := true; exit_use_dir"."; xML"$(BIN)/HOLCF" banner;' | $(BIN)/HOL;\ |
50 |
elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\ |
|
51 |
then echo 'make_html := true; exit_use_dir"."; make_html := false; xML"$(BIN)/HOLCF" banner;' \ |
|
52 |
| $(BIN)/HOL;\ |
|
53 |
else echo 'exit_use_dir"."; xML"$(BIN)/HOLCF" banner;' \ |
|
54 |
| $(BIN)/HOL;\ |
|
55 |
fi;;\ |
|
468 | 56 |
*) echo Bad value for ISABELLECOMP: \ |
2117 | 57 |
\"$(COMP)\" is not poly or sml;;\ |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
58 |
esac |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
59 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
60 |
$(BIN)/HOL: |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
61 |
cd ../HOL; $(MAKE) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
62 |
|
1277
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
63 |
EX_THYS = ex/Fix2.thy ex/Hoare.thy \ |
2094 | 64 |
ex/Loop.thy |
918
7ecdff86a5f0
Uses "suffix substitution" to shorten macro definitions.
lcp
parents:
752
diff
changeset
|
65 |
|
7ecdff86a5f0
Uses "suffix substitution" to shorten macro definitions.
lcp
parents:
752
diff
changeset
|
66 |
EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML) |
7ecdff86a5f0
Uses "suffix substitution" to shorten macro definitions.
lcp
parents:
752
diff
changeset
|
67 |
|
2094 | 68 |
test: ex/ROOT.ML $(BIN)/HOLCF $(EX_FILES) |
2117 | 69 |
@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \ |
1491 | 70 |
poly*) if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
2094 | 71 |
then echo 'make_html := true; exit_use_dir"ex"; quit();' \ |
72 |
| $(COMP) $(BIN)/HOLCF;\ |
|
73 |
else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/HOLCF;\ |
|
74 |
fi;;\ |
|
1491 | 75 |
sml*) if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
2094 | 76 |
then echo 'make_html := true; exit_use_dir"ex";' \ |
77 |
| $(BIN)/HOLCF;\ |
|
78 |
else echo 'exit_use_dir"ex";' | $(BIN)/HOLCF;\ |
|
79 |
fi;;\ |
|
468 | 80 |
*) echo Bad value for ISABELLECOMP: \ |
2117 | 81 |
\"$(COMP)\" is not poly or sml;;\ |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
82 |
esac |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
83 |
|
1277
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
84 |
EXPLICIT_DOMAINS_THYS = explicit_domains/Coind.thy explicit_domains/Dlist.thy \ |
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
85 |
explicit_domains/Dnat2.thy explicit_domains/Stream.thy \ |
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
86 |
explicit_domains/Dagstuhl.thy explicit_domains/Dnat.thy\ |
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
87 |
explicit_domains/Focus_ex.thy explicit_domains/Stream2.thy |
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
88 |
|
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
89 |
EXPLICIT_DOMAINS_FILES = explicit_domains/ROOT.ML $(EXPLICIT_DOMAINS_THYS)\ |
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
90 |
$(EXPLICIT_DOMAINS_THYS:.thy=.ML) |
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
91 |
|
2094 | 92 |
test2: explicit_domains/ROOT.ML $(BIN)/HOLCF $(EXPLICIT_DOMAINS_FILES) |
2117 | 93 |
@case `expr "//$(COMP)" : '[^ ]*/\(.*\)'` in \ |
1491 | 94 |
poly*) if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
2094 | 95 |
then echo 'make_html := true; exit_use_dir"explicit_domains"; quit();' | $(COMP) $(BIN)/HOLCF;\ |
96 |
else echo 'exit_use_dir"explicit_domains"; quit();' \ |
|
97 |
| $(COMP) $(BIN)/HOLCF;\ |
|
98 |
fi;;\ |
|
1491 | 99 |
sml*) if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
2094 | 100 |
then echo 'make_html := true; exit_use_dir"exlicit_domains";' \ |
101 |
| $(BIN)/HOLCF;\ |
|
102 |
else echo 'exit_use_dir"explicit_domains";' | $(BIN)/HOLCF;\ |
|
103 |
fi;;\ |
|
1277
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
104 |
*) echo Bad value for ISABELLECOMP: \ |
2117 | 105 |
\"$(COMP)\" is not poly or sml;;\ |
1277
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
106 |
esac |
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
107 |
|
2094 | 108 |
.PRECIOUS: $(BIN)/HOL $(BIN)/HOLCF |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
109 |