| author | clasohm |
| Tue, 24 Oct 1995 14:45:35 +0100 | |
| changeset 1294 | 1358dc040edb |
| parent 1277 | caef3601c0b2 |
| child 1307 | 63a5788774f7 |
| 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) |
|
918
7ecdff86a5f0
Uses "suffix substitution" to shorten macro definitions.
lcp
parents:
752
diff
changeset
|
19 |
THYS = Holcfb.thy Void.thy Porder.thy Pcpo.thy \ |
|
7ecdff86a5f0
Uses "suffix substitution" to shorten macro definitions.
lcp
parents:
752
diff
changeset
|
20 |
Fun1.thy Fun2.thy Fun3.thy \ |
|
7ecdff86a5f0
Uses "suffix substitution" to shorten macro definitions.
lcp
parents:
752
diff
changeset
|
21 |
Cfun1.thy Cfun2.thy Cfun3.thy Cont.thy \ |
|
7ecdff86a5f0
Uses "suffix substitution" to shorten macro definitions.
lcp
parents:
752
diff
changeset
|
22 |
Cprod1.thy Cprod2.thy Cprod3.thy \ |
|
7ecdff86a5f0
Uses "suffix substitution" to shorten macro definitions.
lcp
parents:
752
diff
changeset
|
23 |
Sprod0.thy Sprod1.thy Sprod2.thy Sprod3.thy \ |
|
7ecdff86a5f0
Uses "suffix substitution" to shorten macro definitions.
lcp
parents:
752
diff
changeset
|
24 |
Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \ |
|
7ecdff86a5f0
Uses "suffix substitution" to shorten macro definitions.
lcp
parents:
752
diff
changeset
|
25 |
Lift1.thy Lift2.thy Lift3.thy Fix.thy ccc1.thy One.thy \ |
| 1274 | 26 |
Tr1.thy Tr2.thy HOLCF.thy |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
27 |
|
|
918
7ecdff86a5f0
Uses "suffix substitution" to shorten macro definitions.
lcp
parents:
752
diff
changeset
|
28 |
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
|
29 |
|
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
30 |
$(BIN)/HOLCF: $(BIN)/HOL $(FILES) |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
31 |
case "$(COMP)" in \ |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
32 |
poly*) echo 'make_database"$(BIN)/HOLCF"; quit();' \ |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
33 |
| $(COMP) $(BIN)/HOL ;\ |
|
953
17d7fad9c9a2
Now calls exit_use instead of use, for prompt failure if errors are detected.
lcp
parents:
918
diff
changeset
|
34 |
echo 'exit_use"ROOT";' | $(COMP) $(BIN)/HOLCF ;;\ |
|
17d7fad9c9a2
Now calls exit_use instead of use, for prompt failure if errors are detected.
lcp
parents:
918
diff
changeset
|
35 |
sml*) echo 'exit_use"ROOT.ML"; xML"$(BIN)/HOLCF" banner;' | $(BIN)/HOL ;;\ |
| 468 | 36 |
*) echo Bad value for ISABELLECOMP: \ |
37 |
$(COMP) is not poly or sml;;\ |
|
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
38 |
esac |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
39 |
|
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
40 |
$(BIN)/HOL: |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
41 |
cd ../HOL; $(MAKE) |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
42 |
|
|
1277
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
43 |
EX_THYS = ex/Fix2.thy ex/Hoare.thy \ |
|
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
44 |
ex/Loop.thy |
|
918
7ecdff86a5f0
Uses "suffix substitution" to shorten macro definitions.
lcp
parents:
752
diff
changeset
|
45 |
|
|
7ecdff86a5f0
Uses "suffix substitution" to shorten macro definitions.
lcp
parents:
752
diff
changeset
|
46 |
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
|
47 |
|
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
48 |
test: ex/ROOT.ML $(BIN)/HOLCF $(EX_FILES) |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
49 |
case "$(COMP)" in \ |
|
953
17d7fad9c9a2
Now calls exit_use instead of use, for prompt failure if errors are detected.
lcp
parents:
918
diff
changeset
|
50 |
poly*) echo 'exit_use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/HOLCF ;;\ |
|
17d7fad9c9a2
Now calls exit_use instead of use, for prompt failure if errors are detected.
lcp
parents:
918
diff
changeset
|
51 |
sml*) echo 'exit_use"ex/ROOT.ML"' | $(BIN)/HOLCF;;\ |
| 468 | 52 |
*) echo Bad value for ISABELLECOMP: \ |
53 |
$(COMP) is not poly or sml;;\ |
|
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
54 |
esac |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
55 |
|
|
1277
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
56 |
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
|
57 |
explicit_domains/Dnat2.thy explicit_domains/Stream.thy \ |
|
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
58 |
explicit_domains/Dagstuhl.thy explicit_domains/Dnat.thy\ |
|
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
59 |
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
|
60 |
|
|
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
61 |
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
|
62 |
$(EXPLICIT_DOMAINS_THYS:.thy=.ML) |
|
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
63 |
|
|
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
64 |
test2: explicit_domains/ROOT.ML $(BIN)/HOLCF $(EXPLICIT_DOMAINS_FILES) |
|
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
65 |
case "$(COMP)" in \ |
|
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
66 |
poly*) echo 'exit_use"explicit_domains/ROOT.ML"; quit();' | $(COMP) $(BIN)/HOLCF ;;\ |
|
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
67 |
sml*) echo 'exit_use"explicit_domains/ROOT.ML"' | $(BIN)/HOLCF;;\ |
|
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
68 |
*) echo Bad value for ISABELLECOMP: \ |
|
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
69 |
$(COMP) is not poly or sml;;\ |
|
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
70 |
esac |
|
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
71 |
|
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
72 |
.PRECIOUS: $(BIN)/HOL $(BIN)/HOLCF |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
73 |