equal
deleted
inserted
replaced
|
1 # $Id$ |
1 ######################################################################### |
2 ######################################################################### |
2 # # |
3 # # |
3 # Makefile for Isabelle (Cube) # |
4 # Makefile for Isabelle (Cube) # |
4 # # |
5 # # |
5 ######################################################################### |
6 ######################################################################### |
6 |
7 |
7 #To make the system, cd to this directory and type |
8 #To make the system, cd to this directory and type |
8 # make |
9 # make |
9 #To make the system and test it on standard examples, type |
10 #To make the system and test it on standard examples, type |
10 # make test |
11 # make test |
|
12 #To generate HTML files for every theory, set the environment variable |
|
13 #MAKE_HTML or add the parameter "MAKE_HTML=". |
11 |
14 |
12 #Environment variable ISABELLECOMP specifies the compiler. |
15 #Environment variable ISABELLECOMP specifies the compiler. |
13 #Environment variable ISABELLEBIN specifies the destination directory. |
16 #Environment variable ISABELLEBIN specifies the destination directory. |
14 #For Poly/ML, ISABELLEBIN must begin with a / |
17 #For Poly/ML, ISABELLEBIN must begin with a / |
15 #WARNING: Poly/ML databases may fail if copied or moved! |
18 #WARNING: Poly/ML databases may fail if copied or moved! |
23 |
26 |
24 $(BIN)/Cube: $(BIN)/Pure $(FILES) |
27 $(BIN)/Cube: $(BIN)/Pure $(FILES) |
25 case "$(COMP)" in \ |
28 case "$(COMP)" in \ |
26 poly*) echo 'make_database"$(BIN)/Cube"; quit();' \ |
29 poly*) echo 'make_database"$(BIN)/Cube"; quit();' \ |
27 | $(COMP) $(BIN)/Pure;\ |
30 | $(COMP) $(BIN)/Pure;\ |
28 echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/Cube ;;\ |
31 if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
29 sml*) echo 'exit_use"ROOT.ML"; xML"$(BIN)/Cube" banner;' | $(BIN)/Pure ;;\ |
32 then echo 'open PolyML; init_html (); exit_use"ROOT";' \ |
|
33 | $(COMP) $(BIN)/Cube;\ |
|
34 else echo 'open PolyML; exit_use"ROOT";' \ |
|
35 | $(COMP) $(BIN)/Cube;\ |
|
36 fi;;\ |
|
37 sml*) if [ "$${MAKE_HTML-undefined}" != "undefined" ];\ |
|
38 then echo 'init_html (); exit_use"ROOT.ML"; xML"$(BIN)/Cube" banner;' | $(BIN)/Pure;\ |
|
39 else echo 'exit_use"ROOT.ML"; xML"$(BIN)/Cube" banner;' \ |
|
40 | $(BIN)/Pure;\ |
|
41 fi;;\ |
30 *) echo Bad value for ISABELLECOMP: \ |
42 *) echo Bad value for ISABELLECOMP: \ |
31 $(COMP) is not poly or sml;;\ |
43 $(COMP) is not poly or sml;;\ |
32 esac |
44 esac |
33 |
45 |
34 $(BIN)/Pure: |
46 $(BIN)/Pure: |