author | clasohm |
Tue, 21 Nov 1995 15:10:12 +0100 | |
changeset 1361 | 90d615b599d9 |
parent 1296 | ae31bb7774a7 |
child 1491 | 38a14548baad |
permissions | -rw-r--r-- |
1296 | 1 |
# $Id$ |
0 | 2 |
######################################################################### |
3 |
# # |
|
4 |
# Makefile for Isabelle (Cube) # |
|
5 |
# # |
|
6 |
######################################################################### |
|
7 |
||
8 |
#To make the system, cd to this directory and type |
|
9 |
# make |
|
10 |
#To make the system and test it on standard examples, type |
|
11 |
# make test |
|
1296 | 12 |
#To generate HTML files for every theory, set the environment variable |
13 |
#MAKE_HTML or add the parameter "MAKE_HTML=". |
|
0 | 14 |
|
15 |
#Environment variable ISABELLECOMP specifies the compiler. |
|
16 |
#Environment variable ISABELLEBIN specifies the destination directory. |
|
17 |
#For Poly/ML, ISABELLEBIN must begin with a / |
|
18 |
#WARNING: Poly/ML databases may fail if copied or moved! |
|
19 |
||
20 |
#Makes pure Isabelle (Pure) if this file is ABSENT -- but not |
|
21 |
#if it is out of date, since this Makefile does not know its dependencies! |
|
22 |
||
23 |
BIN = $(ISABELLEBIN) |
|
24 |
COMP = $(ISABELLECOMP) |
|
335 | 25 |
FILES = ROOT.ML Cube.thy Cube.ML |
0 | 26 |
|
27 |
$(BIN)/Cube: $(BIN)/Pure $(FILES) |
|
28 |
case "$(COMP)" in \ |
|
29 |
poly*) echo 'make_database"$(BIN)/Cube"; quit();' \ |
|
30 |
| $(COMP) $(BIN)/Pure;\ |
|
1296 | 31 |
if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
1361 | 32 |
then echo 'open PolyML; make_html := true; exit_use_dir".";' \ |
1296 | 33 |
| $(COMP) $(BIN)/Cube;\ |
1361 | 34 |
else echo 'open PolyML; exit_use_dir".";' \ |
1296 | 35 |
| $(COMP) $(BIN)/Cube;\ |
36 |
fi;;\ |
|
37 |
sml*) if [ "$${MAKE_HTML-undefined}" != "undefined" ];\ |
|
1361 | 38 |
then echo 'make_html := true; exit_use_dir"."; xML"$(BIN)/Cube" banner;' | $(BIN)/Pure;\ |
39 |
else echo 'exit_use_dir"."; xML"$(BIN)/Cube" banner;' \ |
|
1296 | 40 |
| $(BIN)/Pure;\ |
41 |
fi;;\ |
|
468 | 42 |
*) echo Bad value for ISABELLECOMP: \ |
43 |
$(COMP) is not poly or sml;;\ |
|
0 | 44 |
esac |
45 |
||
46 |
$(BIN)/Pure: |
|
47 |
cd ../Pure; $(MAKE) |
|
48 |
||
49 |
test: ex.ML $(BIN)/Cube |
|
50 |
case "$(COMP)" in \ |
|
953
17d7fad9c9a2
Now calls exit_use instead of use, for prompt failure if errors are detected.
lcp
parents:
468
diff
changeset
|
51 |
poly*) echo 'exit_use"ex.ML"; quit();' | $(COMP) $(BIN)/Cube ;;\ |
17d7fad9c9a2
Now calls exit_use instead of use, for prompt failure if errors are detected.
lcp
parents:
468
diff
changeset
|
52 |
sml*) echo 'exit_use"ex.ML";' | $(BIN)/Cube;;\ |
468 | 53 |
*) echo Bad value for ISABELLECOMP: \ |
54 |
$(COMP) is not poly or sml;;\ |
|
0 | 55 |
esac |
56 |
||
57 |
.PRECIOUS: $(BIN)/Pure $(BIN)/Cube |