equal
deleted
inserted
replaced
|
1 # $Id$ |
1 ######################################################################### |
2 ######################################################################### |
2 # # |
3 # # |
3 # Makefile for Isabelle (HOL) # |
4 # Makefile for Isabelle (HOL) # |
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 -f Makefile |
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 -f Makefile 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 |
18 |
34 $(BIN) is the Isabelle source directory; \ |
37 $(BIN) is the Isabelle source directory; \ |
35 exit 1; \ |
38 exit 1; \ |
36 fi;\ |
39 fi;\ |
37 case "$(COMP)" in \ |
40 case "$(COMP)" in \ |
38 poly*) echo 'make_database"$(BIN)/HOL"; quit();' \ |
41 poly*) echo 'make_database"$(BIN)/HOL"; quit();' \ |
39 | $(COMP) $(BIN)/Pure;\ |
42 | $(COMP) $(BIN)/Pure;\ |
40 echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/HOL ;;\ |
43 if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
41 sml*) echo 'exit_use"ROOT.ML"; xML"$(BIN)/HOL" banner;' | $(BIN)/Pure ;;\ |
44 then echo 'open PolyML; init_html (); exit_use"ROOT";' \ |
|
45 | $(COMP) $(BIN)/HOL;\ |
|
46 else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/HOL;\ |
|
47 fi;;\ |
|
48 sml*) if [ "$${MAKE_HTML-undefined}" != "undefined" ];\ |
|
49 then echo 'init_html (); exit_use"ROOT.ML"; xML"$(BIN)/HOL" banner;' | $(BIN)/Pure;\ |
|
50 else echo 'exit_use"ROOT.ML"; xML"$(BIN)/HOL" banner;' \ |
|
51 | $(BIN)/Pure;\ |
|
52 fi;;\ |
42 *) echo Bad value for ISABELLECOMP: \ |
53 *) echo Bad value for ISABELLECOMP: \ |
43 $(COMP) is not poly or sml; exit 1;;\ |
54 $(COMP) is not poly or sml; exit 1;;\ |
44 esac |
55 esac |
45 |
56 |
46 $(BIN)/Pure: |
57 $(BIN)/Pure: |