1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
|
--- etc/settings.orig Tue Jun 8 10:29:49 2004
+++ etc/settings Fri Aug 12 17:22:30 2005
@@ -13,61 +13,12 @@
# binaries. Do not invent new ML system names unless you know what
# you are doing. Only one of the sections below should be activated.
-
-# try finding the poly packages from the Isabelle site in the usual places
-POLYML_HOME=$(choosefrom \
- "$ISABELLE_HOME/contrib/polyml" \
- "$ISABELLE_HOME/../polyml" \
- "/usr/share/polyml" \
- "/usr/local/polyml" \
- "/opt/polyml")
-
-if [ -n "$POLYML_HOME" -a -e "$POLYML_HOME/bin/polyml-version" ]; then
- # looks like Isabelle poly packages
- ML_SYSTEM=$("$POLYML_HOME/bin/polyml-version" 2>/dev/null || echo polyml)
- ML_PLATFORM=$("$POLYML_HOME/bin/polyml-platform" 2>/dev/null || echo unknown-platform)
- ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="-h 15000"
-elif [ -e /usr/bin/poly -a -e /usr/lib/poly ]; then
- # maybe a shrink-wrapped polyml on x86-linux ...
-
- # Poly/ML 4.0, 4.1, 4.1.x
- # include version number, needed for choosing right options
- ML_SYSTEM=polyml-4.1.3
- # processor/OS type
- ML_PLATFORM=x86-linux
- # where to find binaries
- ML_HOME=/usr/bin
- # where to find the standard database
- ML_DBASE=/usr/lib/poly/ML_dbase
- # options to pass to poly
- ML_OPTIONS="-h 15000"
-fi
-
-# Standard ML of New Jersey 110 or later
-#ML_SYSTEM=smlnj-110
-#ML_HOME="$ISABELLE_HOME/../smlnj/bin"
-#ML_OPTIONS="@SMLdebug=/dev/null"
-#ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
-
-# MLWorks 2.0
-#ML_SYSTEM=mlworks
-#ML_HOME="$ISABELLE_HOME/../mlworks/bin"
-#ML_OPTIONS=""
-#ML_PLATFORM=""
-
-# Moscow ML 2.00 or later (experimental!)
-#ML_SYSTEM=mosml
-#ML_HOME="$ISABELLE_HOME/../mosml/bin"
-#ML_PLATFORM=""
-#ML_OPTIONS=""
-
-# Standard ML of New Jersey 0.93
-#ML_SYSTEM=smlnj-0.93
-#ML_HOME=/usr/local/ldist/DIR/sml-0.93/src
-#ML_OPTIONS=""
-#ML_PLATFORM=""
-
+# %%ML_COMMENT%%
+ML_SYSTEM=%%ML_SYSTEM%%
+ML_HOME=%%ML_HOME%%
+ML_OPTIONS=%%ML_OPTIONS%%
+ML_PLATFORM=x86-bsd
+ML_DBASE=%%ML_DBASE%%
###
### Compilation options for isatool usedir
@@ -79,7 +30,6 @@
# for overriding proof objects in HOL image
HOL_PROOF_OBJECTS=""
-
###
### Document preparation
###
@@ -155,7 +105,7 @@
###
#Where to look for docs (multiple dirs separated by ':').
-ISABELLE_DOCS="$ISABELLE_HOME/doc"
+ISABELLE_DOCS="%%PREFIX%%/share/doc/isabelle"
#The dvi file viewer
DVI_VIEWER=xdvi
@@ -181,12 +131,7 @@
# Proof General path, look in a variety of places
ISABELLE_INTERFACE=$(choosefrom \
- "$ISABELLE_HOME/contrib/ProofGeneral/isar/interface" \
- "$ISABELLE_HOME/../ProofGeneral/isar/interface" \
- "/usr/share/ProofGeneral/isar/interface" \
- "/usr/local/ProofGeneral/isar/interface" \
- "/opt/ProofGeneral/isar/interface" \
- "/usr/share/emacs/ProofGeneral/isar/interface" \
+ "%%PREFIX%%/bin/proofgeneral" \
"$ISABELLE_INTERFACE")
# Options to pass to Isabelle command when PG is selected as interface
@@ -196,20 +141,9 @@
# try xemacs first, else emacs
type -path xemacs >/dev/null || PROOFGENERAL_OPTIONS="-p emacs $PROOFGENERAL_OPTIONS"
-
-# X-Symbol installation location (for Proof General, obsolete for PG >= 3.5)
-XSYMBOL_HOME=$(choosefrom \
- "$ISABELLE_HOME/contrib/x-symbol" \
- "$ISABELLE_HOME/../x-symbol" \
- "/usr/share/x-symbol" \
- "/usr/local/x-symbol" \
- "/opt/x-symbol" \
- "")
-
# Executed before xemacs with ProofGeneral is called.
# Required for remote fonts only.
#XSYMBOL_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"
-
###
### External reasoning tools
|
