author | wenzelm |
Fri, 15 Oct 1999 16:43:05 +0200 | |
changeset 7873 | 5d1200c7a671 |
parent 7864 | 5cd5a27f5c93 |
child 8345 | e708af969264 |
permissions | -rw-r--r-- |
2294 | 1 |
# |
2 |
# $Id$ |
|
3 |
# |
|
2309 | 4 |
# Isabelle settings -- site defaults. |
5964 | 5 |
# Do *NOT* copy this file into your personal isabelle directory! |
2309 | 6 |
|
2426 | 7 |
### |
3177 | 8 |
### ML compiler settings (ESSENTIAL!) |
2426 | 9 |
### |
10 |
||
2786 | 11 |
## Uncomment and adapt one of the sections below. Note that ML_HOME |
2426 | 12 |
## specifies the location of the actual compiler binaries. |
13 |
||
5708 | 14 |
# Standard ML of New Jersey 110 or later |
6463 | 15 |
ML_SYSTEM=smlnj-110 |
7126 | 16 |
ML_HOME=$ISABELLE_HOME/../smlnj/bin |
6463 | 17 |
ML_OPTIONS="@SMLdebug=/dev/null" |
6464 | 18 |
ML_PLATFORM=$(eval $($ML_HOME/.arch-n-opsys 2>/dev/null); echo $HEAP_SUFFIX) |
5708 | 19 |
|
20 |
# MLWorks 2.0 or later |
|
21 |
#ML_SYSTEM=mlworks |
|
22 |
#ML_HOME=/usr/local/mlworks/bin |
|
23 |
#ML_OPTIONS="" |
|
6413 | 24 |
#ML_PLATFORM="" |
5708 | 25 |
|
2426 | 26 |
# Poly/ML 2.x |
2435 | 27 |
#ML_SYSTEM=polyml-2.07 |
2426 | 28 |
#ML_HOME=/usr/local/ldist/DIR/polyml/polyml/solaris2 |
29 |
#ML_OPTIONS="-h 30000" |
|
6413 | 30 |
#ML_PLATFORM="" |
2294 | 31 |
|
2426 | 32 |
# Poly/ML 3.1 |
6463 | 33 |
#ML_SYSTEM=polyml-3.1 |
34 |
#ML_HOME=/usr/local/ldist/DIR/polyml-3.1/polyml/sunos5.4 |
|
35 |
#ML_OPTIONS="-h 30000" |
|
36 |
#ML_PLATFORM="" |
|
37 |
#LM_LICENSE_FILE=$ML_HOME/license.dat |
|
2294 | 38 |
|
2426 | 39 |
# Standard ML of New Jersey 0.93 |
40 |
#ML_SYSTEM=smlnj-0.93 |
|
41 |
#ML_HOME=/usr/local/ldist/DIR/sml-0.93/src |
|
42 |
#ML_OPTIONS="" |
|
6413 | 43 |
#ML_PLATFORM="" |
2426 | 44 |
|
2294 | 45 |
|
2426 | 46 |
### |
3177 | 47 |
### Compilation options |
2435 | 48 |
### |
49 |
||
5387 | 50 |
ISABELLE_USEDIR_OPTIONS="-i false" |
7762
c98d70538033
ISABELLE_USEDIR_OPTIONS: -d pdf option (off by default);
wenzelm
parents:
7296
diff
changeset
|
51 |
#ISABELLE_USEDIR_OPTIONS="-i true -d pdf" |
2435 | 52 |
|
53 |
||
54 |
### |
|
7773 | 55 |
### Document preparation |
56 |
### |
|
57 |
||
58 |
TEXINPUTS="$ISABELLE_HOME/lib/texinputs:$TEXINPUTS" |
|
59 |
ISABELLE_LATEX="latex" |
|
60 |
ISABELLE_PDFLATEX="pdflatex" |
|
7813 | 61 |
ISABELLE_BIBTEX="bibtex" |
7773 | 62 |
ISABELLE_DVIPS="dvips -D 600" |
63 |
||
7873 | 64 |
# The thumbpdf tool is probably not generally available ... |
7864 | 65 |
#ISABELLE_THUMBPDF="thumbpdf" |
66 |
||
7773 | 67 |
|
68 |
### |
|
2968 | 69 |
### Misc path settings |
2426 | 70 |
### |
2294 | 71 |
|
2426 | 72 |
# The place for user configuration, heap files, etc. |
73 |
ISABELLE_HOME_USER=~/isabelle |
|
2294 | 74 |
|
3177 | 75 |
# Where to look for isabelle tools (multiple dirs separated by ':'). |
2786 | 76 |
ISABELLE_TOOLS=$ISABELLE_HOME/lib/Tools |
77 |
||
4334 | 78 |
# Location for temporary files (should be on a local file system). |
4708 | 79 |
ISABELLE_TMP_PREFIX=/tmp/isabelle-$USER |
4334 | 80 |
|
2786 | 81 |
|
3118 | 82 |
# Heap file locations. ML system identifier appended automatically! |
2786 | 83 |
|
3118 | 84 |
ISABELLE_PATH=$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps |
2780 | 85 |
|
4413 | 86 |
#A hack! Isabelle build tells us to store heaps etc. within the |
87 |
#distribution. |
|
2780 | 88 |
if [ "$THIS_IS_ISABELLE_BUILD" = true ]; then |
3118 | 89 |
ISABELLE_OUTPUT=$ISABELLE_HOME/heaps |
3637
02ba2acc69c3
Added new environment variable ISABELLE_BROWSER_INFO.
berghofe
parents:
3596
diff
changeset
|
90 |
ISABELLE_BROWSER_INFO=$ISABELLE_HOME/browser_info |
2780 | 91 |
else |
3118 | 92 |
ISABELLE_OUTPUT=$ISABELLE_HOME_USER/heaps |
3637
02ba2acc69c3
Added new environment variable ISABELLE_BROWSER_INFO.
berghofe
parents:
3596
diff
changeset
|
93 |
ISABELLE_BROWSER_INFO=$ISABELLE_HOME_USER/browser_info |
2780 | 94 |
fi |
95 |
||
3177 | 96 |
#Users may want to change this. |
3184 | 97 |
ISABELLE_LOGIC=HOL |
2294 | 98 |
|
2786 | 99 |
|
100 |
## Docs |
|
2294 | 101 |
|
3177 | 102 |
#Where to look for docs (multiple dirs separated by ':'). |
2345 | 103 |
ISABELLE_DOCS=$ISABELLE_HOME/doc |
104 |
||
3177 | 105 |
#The dvi file viewer |
3062 | 106 |
DVI_VIEWER=xdvi |
2426 | 107 |
#DVI_VIEWER="xdvi -geometry 498x704 -expert -s 5" |
2476 | 108 |
#DVI_VIEWER="xdvi -geometry 500x704 -expert -s 10" |
3062 | 109 |
#DVI_VIEWER="xdvi -geometry 555x782 -expert -s 9" |
2345 | 110 |
|
2294 | 111 |
|
3158 | 112 |
## Fonts -- how to install the Isabelle X11 fonts (can be tricky!). |
113 |
||
114 |
# (1) Get fonts from local (client side) directory: |
|
2577 | 115 |
ISABELLE_INSTALLFONTS="xset fp+ $ISABELLE_HOME/lib/fonts; xset fp rehash" |
3158 | 116 |
|
3689 | 117 |
# (2) Get from font server at Munich or Cambridge: |
3256 | 118 |
#ISABELLE_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200" |
3689 | 119 |
#ISABELLE_INSTALLFONTS="xset fp+ tcp/font-serv.cl.cam.ac.uk:7100" |
2577 | 120 |
|
5964 | 121 |
|
2426 | 122 |
### |
123 |
### Interfaces |
|
124 |
### |
|
125 |
||
126 |
# The null interface: pass-through to 'isabelle'. |
|
2294 | 127 |
#ISABELLE_INTERFACE=none |
128 |
||
2786 | 129 |
# Simple xterm based interface. |
2294 | 130 |
ISABELLE_INTERFACE=xterm |
5964 | 131 |
ISABELLE_XTERM_OPTIONS="" |
2968 | 132 |
|
3303 | 133 |
# Emacs running Isamode. |
2968 | 134 |
#ISABELLE_INTERFACE=emacs |
2969 | 135 |
ISAMODE_HOME=$ISABELLE_HOME/contrib/Isamode |
5964 | 136 |
ISAMODE_OPTIONS="" |
137 |
||
138 |
# Emacs running Proof General. |
|
139 |
#ISABELLE_INTERFACE=$ISABELLE_HOME/contrib/ProofGeneral/isar/interface |
|
140 |
PROOFGENERAL_OPTIONS="" |
|
7185 | 141 |
|
142 |
||
143 |
### |
|
144 |
### External reasoning tools |
|
145 |
### |
|
146 |
||
7194 | 147 |
## Set HOME only for tools you have installed! |
7185 | 148 |
|
149 |
# SVC (Stanford Validity Checker) |
|
150 |
#SVC_HOME= |
|
151 |
#SVC_MACHINE=i386-redhat-linux |
|
152 |
#SVC_MACHINE=sparc-sun-solaris |
|
7296 | 153 |
|
154 |
# Mucke (mu-calculus model checker) |
|
155 |
#MUCKE_HOME=/usr/local/bin |
|
156 |
||
157 |
# Einhoven model checker |
|
158 |
#EINDHOVEN_HOME=/usr/local/bin |