equal
deleted
inserted
replaced
1 # -*- shell-script -*- |
1 # -*- shell-script -*- |
2 # $Id$ |
2 # $Id$ |
3 # |
3 # |
4 # Isabelle settings -- site defaults. |
4 # Isabelle settings -- site defaults. |
5 # Do *NOT* copy this file into your personal isabelle directory!!! |
5 # |
|
6 # Important notes: |
|
7 # * See the system manual for explanations on Isabelle settings |
|
8 # * DO NOT EDIT the repository copy of this file! |
|
9 # * DO NOT COPY this file into your personal isabelle directory! |
6 |
10 |
7 ### |
11 ### |
8 ### ML compiler settings (ESSENTIAL!) |
12 ### ML compiler settings (ESSENTIAL!) |
9 ### |
13 ### |
10 |
14 |
11 # Note that ML_HOME specifies the location of the actual compiler |
15 # Note that ML_HOME specifies the location of the actual compiler |
12 # binaries. Do not invent new ML system names unless you know what |
16 # binaries. Do not invent new ML system names unless you know what |
13 # you are doing. Only one of the sections below should be activated. |
17 # you are doing. Only one of the sections below should be activated. |
14 |
|
15 |
18 |
16 # try finding the poly packages from the Isabelle site in the usual places |
19 # try finding the poly packages from the Isabelle site in the usual places |
17 POLYML_HOME=$(choosefrom \ |
20 POLYML_HOME=$(choosefrom \ |
18 "$ISABELLE_HOME/contrib/polyml" \ |
21 "$ISABELLE_HOME/contrib/polyml" \ |
19 "$ISABELLE_HOME/../polyml" \ |
22 "$ISABELLE_HOME/../polyml" \ |
61 |
64 |
62 ### |
65 ### |
63 ### Compilation options (cf. isatool usedir) |
66 ### Compilation options (cf. isatool usedir) |
64 ### |
67 ### |
65 |
68 |
66 ISABELLE_USEDIR_OPTIONS="-v true -i true" |
69 ISABELLE_USEDIR_OPTIONS="-v true" |
67 |
70 |
68 # Specifically for the HOL image |
71 # Specifically for the HOL image |
69 HOL_USEDIR_OPTIONS="" |
72 HOL_USEDIR_OPTIONS="" |
70 |
73 |
71 |
74 |
118 [ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \ |
121 [ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \ |
119 { echo >&2 "### Isabelle site settings already present! Maybe copied etc/settings in full?"; } |
122 { echo >&2 "### Isabelle site settings already present! Maybe copied etc/settings in full?"; } |
120 |
123 |
121 |
124 |
122 ### |
125 ### |
123 ### default logic (users may want to override this in their own settings file) |
126 ### default logic |
124 ### |
127 ### |
125 |
128 |
126 ISABELLE_LOGIC=HOL |
129 ISABELLE_LOGIC=HOL |
127 |
130 |
128 |
131 |
173 |
176 |
174 # Options to pass to Isabelle command when PG is selected as interface |
177 # Options to pass to Isabelle command when PG is selected as interface |
175 PROOFGENERAL_OPTIONS="" |
178 PROOFGENERAL_OPTIONS="" |
176 #PROOFGENERAL_OPTIONS="-m no_brackets -m no_type_brackets -x true" |
179 #PROOFGENERAL_OPTIONS="-m no_brackets -m no_type_brackets -x true" |
177 |
180 |
178 # try xemacs first, else emacs |
181 type -path xemacs >/dev/null || \ |
179 type -path xemacs >/dev/null || PROOFGENERAL_OPTIONS="-p emacs $PROOFGENERAL_OPTIONS" |
182 PROOFGENERAL_OPTIONS="-p emacs $PROOFGENERAL_OPTIONS" |
180 |
183 |
181 |
184 # Executed before xemacs with ProofGeneral is called; required for remote fonts. |
182 # X-Symbol installation location (for Proof General, obsolete for PG >= 3.5) |
|
183 XSYMBOL_HOME=$(choosefrom \ |
|
184 "$ISABELLE_HOME/contrib/x-symbol" \ |
|
185 "$ISABELLE_HOME/../x-symbol" \ |
|
186 "/usr/share/x-symbol" \ |
|
187 "/usr/local/x-symbol" \ |
|
188 "/opt/x-symbol" \ |
|
189 "") |
|
190 |
|
191 # Executed before xemacs with ProofGeneral is called. |
|
192 # Required for remote fonts only. |
|
193 #XSYMBOL_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200" |
185 #XSYMBOL_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200" |
194 |
186 |
195 |
187 |
196 ### |
188 ### |
197 ### External reasoning tools |
189 ### External reasoning tools |
226 # HOL4 proof objects (cf. Isabelle/src/HOL/Import) |
218 # HOL4 proof objects (cf. Isabelle/src/HOL/Import) |
227 HOL4_PROOFS="$PROOF_DIRS:$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs" |
219 HOL4_PROOFS="$PROOF_DIRS:$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs" |
228 |
220 |
229 # For configuring HOL/Matrix/cplex |
221 # For configuring HOL/Matrix/cplex |
230 # First option: use the commercial cplex solver |
222 # First option: use the commercial cplex solver |
231 # LP_SOLVER_NAME=CPLEX |
223 #LP_SOLVER_NAME=CPLEX |
232 # LP_SOLVER_PATH=cplex |
224 #LP_SOLVER_PATH=cplex |
233 # Second option: use the open source glpk solver |
225 # Second option: use the open source glpk solver |
234 # LP_SOLVER_NAME=GLPK |
226 #LP_SOLVER_NAME=GLPK |
235 # LP_SOLVER_PATH=glpsol |
227 #LP_SOLVER_PATH=glpsol |
236 |
|
237 # toogles the detail of the error message in case of a cyclic definition |
|
238 DEFS_CHAIN_HISTORY=ON |
|
239 #DEFS_CHAIN_HISTORY=OFF |
|