author | wenzelm |
Sat, 19 Oct 2024 16:27:00 +0200 | |
changeset 81197 | 794b10baf0de |
parent 79556 | 0631dfc0db07 |
permissions | -rwxr-xr-x |
25434
746677c843a7
ISABELLE_IDENTIFIER is filled in automatically, not taken from the *long* form of isatool version!
wenzelm
parents:
21490
diff
changeset
|
1 |
# -*- shell-script -*- :mode=shellscript: |
29145 | 2 |
# |
62412
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
62354
diff
changeset
|
3 |
# Author: Makarius |
2299
ed9720047d53
getsettings: bash source script to augment current env.
wenzelm
parents:
diff
changeset
|
4 |
# |
62412
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
62354
diff
changeset
|
5 |
# Static Isabelle environment for root of process tree. |
2299
ed9720047d53
getsettings: bash source script to augment current env.
wenzelm
parents:
diff
changeset
|
6 |
|
62416 | 7 |
export ISABELLE_HOME |
8 |
||
9 |
export BASH_ENV="$ISABELLE_HOME/lib/scripts/getfunctions" |
|
10 |
source "$BASH_ENV" |
|
11 |
||
12 |
||
7770
0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
wenzelm
parents:
6413
diff
changeset
|
13 |
if [ -z "$ISABELLE_SETTINGS_PRESENT" ] |
0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
wenzelm
parents:
6413
diff
changeset
|
14 |
then |
0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
wenzelm
parents:
6413
diff
changeset
|
15 |
|
62413 | 16 |
export ISABELLE_SETTINGS_PRESENT=true |
3185 | 17 |
|
62412
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
62354
diff
changeset
|
18 |
set -o allexport |
53913
5ff12177a067
prefer GNU tar for Isabelle to avoid odd extended header keywords produced by Apple's bsdtar (see also 8f6046b7f850);
wenzelm
parents:
53580
diff
changeset
|
19 |
|
72894
bd2269b6cd99
updated "macOS" terminology: current Big Sur is already version 11;
wenzelm
parents:
72162
diff
changeset
|
20 |
#sane environment defaults (notably on macOS) |
57411
9444489766a1
sane environment defaults for Mac OS X, based on former App1/script -- e.g. relevant for MacTeX PATH;
wenzelm
parents:
56448
diff
changeset
|
21 |
if [ "$ISABELLE_APP" = true -a -x /usr/libexec/path_helper ]; then |
9444489766a1
sane environment defaults for Mac OS X, based on former App1/script -- e.g. relevant for MacTeX PATH;
wenzelm
parents:
56448
diff
changeset
|
22 |
eval $(/usr/libexec/path_helper -s) |
9444489766a1
sane environment defaults for Mac OS X, based on former App1/script -- e.g. relevant for MacTeX PATH;
wenzelm
parents:
56448
diff
changeset
|
23 |
fi |
9444489766a1
sane environment defaults for Mac OS X, based on former App1/script -- e.g. relevant for MacTeX PATH;
wenzelm
parents:
56448
diff
changeset
|
24 |
|
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
25 |
#Cygwin vs. POSIX |
47461
5a7903ba2dac
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
wenzelm
parents:
47254
diff
changeset
|
26 |
if [ "$OSTYPE" = cygwin ] |
5a7903ba2dac
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
wenzelm
parents:
47254
diff
changeset
|
27 |
then |
53970 | 28 |
unset INI_DIR |
29 |
||
78627
fa18208fd7bd
more robust $TMPDIR on windows, e.g. for repository snapshot: do not depend on $TEMP_WINDOWS provided by official distribution;a
wenzelm
parents:
78623
diff
changeset
|
30 |
TMPDIR="$(cygpath -u "$LOCALAPPDATA")/Temp" |
fa18208fd7bd
more robust $TMPDIR on windows, e.g. for repository snapshot: do not depend on $TEMP_WINDOWS provided by official distribution;a
wenzelm
parents:
78623
diff
changeset
|
31 |
TMP="$TMPDIR" |
fa18208fd7bd
more robust $TMPDIR on windows, e.g. for repository snapshot: do not depend on $TEMP_WINDOWS provided by official distribution;a
wenzelm
parents:
78623
diff
changeset
|
32 |
TEMP="$TMPDIR" |
58640
37f852399a32
prefer original TEMP from Windows, e.g. relevant for Isabelle distribution within read-only directory (due to its bundled Cygwin and /tmp inside of it);
wenzelm
parents:
58413
diff
changeset
|
33 |
|
47661
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
47525
diff
changeset
|
34 |
if [ -z "$USER_HOME" ]; then |
60531
9cc91b8a6489
less ambitious USER_HOME on Windows: avoid potentially disconnected share, agree with guess of JVM user.home;
wenzelm
parents:
58791
diff
changeset
|
35 |
USER_HOME="$(cygpath -u "$USERPROFILE")" |
47661
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
47525
diff
changeset
|
36 |
fi |
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
47525
diff
changeset
|
37 |
|
61294 | 38 |
CYGWIN_ROOT="$(platform_path "/")" |
39 |
ISABELLE_ROOT="$(platform_path "$ISABELLE_HOME")" |
|
53576
793a429c63e7
maintain classpath in more elementary manner: turn ISABELLE_CLASSPATH into -classpath option, so that all jars are covered by sun.misc.Launcher.AppClassLoader (e.g. relevant for loading add-on resources);
wenzelm
parents:
52443
diff
changeset
|
40 |
|
793a429c63e7
maintain classpath in more elementary manner: turn ISABELLE_CLASSPATH into -classpath option, so that all jars are covered by sun.misc.Launcher.AppClassLoader (e.g. relevant for loading add-on resources);
wenzelm
parents:
52443
diff
changeset
|
41 |
ISABELLE_CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")" |
76343
6a6f650cc5a2
more robust reset of CLASSPATH: unset variable means "." in certain situations, e.g. scalac;
wenzelm
parents:
76326
diff
changeset
|
42 |
export CLASSPATH="" |
47461
5a7903ba2dac
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
wenzelm
parents:
47254
diff
changeset
|
43 |
else |
47661
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
47525
diff
changeset
|
44 |
if [ -z "$USER_HOME" ]; then |
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
47525
diff
changeset
|
45 |
USER_HOME="$HOME" |
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
47525
diff
changeset
|
46 |
fi |
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
47525
diff
changeset
|
47 |
|
61293
876e7eae22be
clarified ISABELLE_ROOT (platform path) vs. ISABELLE_HOME (standard path);
wenzelm
parents:
61159
diff
changeset
|
48 |
ISABELLE_ROOT="$ISABELLE_HOME" |
876e7eae22be
clarified ISABELLE_ROOT (platform path) vs. ISABELLE_HOME (standard path);
wenzelm
parents:
61159
diff
changeset
|
49 |
|
53576
793a429c63e7
maintain classpath in more elementary manner: turn ISABELLE_CLASSPATH into -classpath option, so that all jars are covered by sun.misc.Launcher.AppClassLoader (e.g. relevant for loading add-on resources);
wenzelm
parents:
52443
diff
changeset
|
50 |
ISABELLE_CLASSPATH="$CLASSPATH" |
76343
6a6f650cc5a2
more robust reset of CLASSPATH: unset variable means "." in certain situations, e.g. scalac;
wenzelm
parents:
76326
diff
changeset
|
51 |
export CLASSPATH="" |
47461
5a7903ba2dac
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
wenzelm
parents:
47254
diff
changeset
|
52 |
fi |
5a7903ba2dac
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
wenzelm
parents:
47254
diff
changeset
|
53 |
|
72161 | 54 |
#init cumulative settings |
55 |
ISABELLE_FONTS="" |
|
56 |
ISABELLE_FONTS_HIDDEN="" |
|
57 |
ISABELLE_SCALA_SERVICES="" |
|
72162 | 58 |
ISABELLE_DIRECTORIES="" |
72161 | 59 |
|
62412
ffdc5cf36dc5
more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash;
wenzelm
parents:
62354
diff
changeset
|
60 |
#main executables |
56440 | 61 |
ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle" |
62414
1abd90afe387
within the Isabelle environment, main executables are always within PATH;
wenzelm
parents:
62413
diff
changeset
|
62 |
PATH="$ISABELLE_HOME/bin:$PATH" |
56440 | 63 |
|
36196
cbb9ee265cdd
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
wenzelm
parents:
36194
diff
changeset
|
64 |
#platform |
41758 | 65 |
source "$ISABELLE_HOME/lib/scripts/isabelle-platform" |
71344 | 66 |
if [ -z "$ISABELLE_PLATFORM_FAMILY" ]; then |
48455 | 67 |
echo 1>&2 "Failed to determine hardware and operating system type!" |
68 |
exit 2 |
|
69 |
fi |
|
36196
cbb9ee265cdd
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
wenzelm
parents:
36194
diff
changeset
|
70 |
|
73523
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73520
diff
changeset
|
71 |
if [ -z "$ISABELLE_IDENTIFIER" -a -f "$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER" ] |
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73520
diff
changeset
|
72 |
then |
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73520
diff
changeset
|
73 |
ISABELLE_IDENTIFIER="$(cat "$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER")" |
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73520
diff
changeset
|
74 |
fi |
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73520
diff
changeset
|
75 |
|
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
73520
diff
changeset
|
76 |
ISABELLE_NAME="${ISABELLE_IDENTIFIER:-Isabelle}" |
21490 | 77 |
|
78623
b96b73a79da3
more robust: "hostname" command might be absent, notably on Arch Linux (and other systemd-based distributions);
wenzelm
parents:
77373
diff
changeset
|
78 |
ISABELLE_HOSTNAME="$(hostname -s 2>/dev/null || uname -n)" |
77373
eaf234b0c849
proper settings for hostname: allow to adjust it in user space;
wenzelm
parents:
76343
diff
changeset
|
79 |
|
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
80 |
|
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
81 |
# components |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
82 |
|
32305
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
83 |
ISABELLE_COMPONENTS="" |
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
84 |
ISABELLE_COMPONENTS_MISSING="" |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
85 |
|
32305
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
86 |
#main components |
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
87 |
init_component "$ISABELLE_HOME" |
48725
e852f4d6af80
configure Admin as component, with its own lib/Tools;
wenzelm
parents:
48551
diff
changeset
|
88 |
[ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin" |
61319
d84b4d39bce1
more explicit umask for important directories: e.g. relevant for Windows 10, where implicit g=rwx leads to odd failure of chmod -w for heap images;
wenzelm
parents:
61294
diff
changeset
|
89 |
if [ -d "$ISABELLE_HOME_USER" ]; then |
d84b4d39bce1
more explicit umask for important directories: e.g. relevant for Windows 10, where implicit g=rwx leads to odd failure of chmod -w for heap images;
wenzelm
parents:
61294
diff
changeset
|
90 |
init_component "$ISABELLE_HOME_USER" |
d84b4d39bce1
more explicit umask for important directories: e.g. relevant for Windows 10, where implicit g=rwx leads to odd failure of chmod -w for heap images;
wenzelm
parents:
61294
diff
changeset
|
91 |
else |
d84b4d39bce1
more explicit umask for important directories: e.g. relevant for Windows 10, where implicit g=rwx leads to odd failure of chmod -w for heap images;
wenzelm
parents:
61294
diff
changeset
|
92 |
mkdir -p "$ISABELLE_HOME_USER" |
d84b4d39bce1
more explicit umask for important directories: e.g. relevant for Windows 10, where implicit g=rwx leads to odd failure of chmod -w for heap images;
wenzelm
parents:
61294
diff
changeset
|
93 |
chmod $(umask -S) "$ISABELLE_HOME_USER" |
d84b4d39bce1
more explicit umask for important directories: e.g. relevant for Windows 10, where implicit g=rwx leads to odd failure of chmod -w for heap images;
wenzelm
parents:
61294
diff
changeset
|
94 |
fi |
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
95 |
|
67099 | 96 |
#POLYML_EXE |
79556
0631dfc0db07
more robust check of ISABELLE_PLATFORM_FAMILY within settings environment, to support its reunification with Isabelle/Scala (see also a33a6e541cbb, f3a356c64193);
wenzelm
parents:
79059
diff
changeset
|
97 |
case "$ISABELLE_PLATFORM_FAMILY" in |
0631dfc0db07
more robust check of ISABELLE_PLATFORM_FAMILY within settings environment, to support its reunification with Isabelle/Scala (see also a33a6e541cbb, f3a356c64193);
wenzelm
parents:
79059
diff
changeset
|
98 |
windows*) |
0631dfc0db07
more robust check of ISABELLE_PLATFORM_FAMILY within settings environment, to support its reunification with Isabelle/Scala (see also a33a6e541cbb, f3a356c64193);
wenzelm
parents:
79059
diff
changeset
|
99 |
POLYML_EXE="$ML_HOME/poly.exe" |
0631dfc0db07
more robust check of ISABELLE_PLATFORM_FAMILY within settings environment, to support its reunification with Isabelle/Scala (see also a33a6e541cbb, f3a356c64193);
wenzelm
parents:
79059
diff
changeset
|
100 |
;; |
0631dfc0db07
more robust check of ISABELLE_PLATFORM_FAMILY within settings environment, to support its reunification with Isabelle/Scala (see also a33a6e541cbb, f3a356c64193);
wenzelm
parents:
79059
diff
changeset
|
101 |
*) |
0631dfc0db07
more robust check of ISABELLE_PLATFORM_FAMILY within settings environment, to support its reunification with Isabelle/Scala (see also a33a6e541cbb, f3a356c64193);
wenzelm
parents:
79059
diff
changeset
|
102 |
POLYML_EXE="$ML_HOME/poly" |
0631dfc0db07
more robust check of ISABELLE_PLATFORM_FAMILY within settings environment, to support its reunification with Isabelle/Scala (see also a33a6e541cbb, f3a356c64193);
wenzelm
parents:
79059
diff
changeset
|
103 |
;; |
0631dfc0db07
more robust check of ISABELLE_PLATFORM_FAMILY within settings environment, to support its reunification with Isabelle/Scala (see also a33a6e541cbb, f3a356c64193);
wenzelm
parents:
79059
diff
changeset
|
104 |
esac |
67099 | 105 |
|
21490 | 106 |
#ML system identifier |
6413 | 107 |
if [ -z "$ML_PLATFORM" ]; then |
108 |
ML_IDENTIFIER="$ML_SYSTEM" |
|
109 |
else |
|
110 |
ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}" |
|
111 |
fi |
|
21468
c7892915ed10
add ISABELLE_VERSION to ML_IDENTIFIER, unless this is repository or build;
wenzelm
parents:
16293
diff
changeset
|
112 |
|
69926
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69910
diff
changeset
|
113 |
#enforce ISABELLE_OCAMLFIND |
69910
0c0f7b4a72bf
dedicated environment setting for ocaml environment: ISABELLE_OPAM_ROOT is always present even if no envionrment is available
haftmann
parents:
69444
diff
changeset
|
114 |
if [ -d "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin" ]; then |
69926
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69910
diff
changeset
|
115 |
ISABELLE_OCAMLFIND="$ISABELLE_HOME/lib/scripts/ocamlfind" |
69910
0c0f7b4a72bf
dedicated environment setting for ocaml environment: ISABELLE_OPAM_ROOT is always present even if no envionrment is available
haftmann
parents:
69444
diff
changeset
|
116 |
fi |
0c0f7b4a72bf
dedicated environment setting for ocaml environment: ISABELLE_OPAM_ROOT is always present even if no envionrment is available
haftmann
parents:
69444
diff
changeset
|
117 |
|
69152
77eede3f40e2
enforce settings that are likely to be outdated, e.g. in $ISABELLE_HOME_USER/etc/settings;
wenzelm
parents:
69151
diff
changeset
|
118 |
#enforce ISABELLE_GHC |
69930
b5286c564861
more robust reference to ghc exe (with multi-platform support);
wenzelm
parents:
69926
diff
changeset
|
119 |
if [ -f "$ISABELLE_STACK_ROOT/ISABELLE_GHC_EXE-$ISABELLE_PLATFORM_FAMILY" ]; then |
b5286c564861
more robust reference to ghc exe (with multi-platform support);
wenzelm
parents:
69926
diff
changeset
|
120 |
if [ -f "$(cat "$ISABELLE_STACK_ROOT/ISABELLE_GHC_EXE-$ISABELLE_PLATFORM_FAMILY")" ]; then |
69268
c1a27fce2076
clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents:
69242
diff
changeset
|
121 |
ISABELLE_GHC="$ISABELLE_HOME/lib/scripts/ghc" |
69444
c3c9440cbf9b
more formal Haskell project setup, with dependencies on packages from "stackage";
wenzelm
parents:
69268
diff
changeset
|
122 |
ISABELLE_GHC_STACK=true |
69153
108beabc1bc6
avoid strict evaluation of "isabelle_stack path --programs";
wenzelm
parents:
69152
diff
changeset
|
123 |
fi |
69151 | 124 |
fi |
125 |
||
47748
24550210de0b
enforce our JAVA_HOME to avoid potential conflicts with other Java installations by the user;
wenzelm
parents:
47661
diff
changeset
|
126 |
#enforce JAVA_HOME |
68012
6d38b4fd872e
more robust, notably for jdk-10.0.1 where jre is absent;
wenzelm
parents:
67099
diff
changeset
|
127 |
if [ -d "$ISABELLE_JDK_HOME/jre" ] |
6d38b4fd872e
more robust, notably for jdk-10.0.1 where jre is absent;
wenzelm
parents:
67099
diff
changeset
|
128 |
then |
6d38b4fd872e
more robust, notably for jdk-10.0.1 where jre is absent;
wenzelm
parents:
67099
diff
changeset
|
129 |
export JAVA_HOME="$ISABELLE_JDK_HOME/jre" |
6d38b4fd872e
more robust, notably for jdk-10.0.1 where jre is absent;
wenzelm
parents:
67099
diff
changeset
|
130 |
else |
6d38b4fd872e
more robust, notably for jdk-10.0.1 where jre is absent;
wenzelm
parents:
67099
diff
changeset
|
131 |
export JAVA_HOME="$ISABELLE_JDK_HOME" |
6d38b4fd872e
more robust, notably for jdk-10.0.1 where jre is absent;
wenzelm
parents:
67099
diff
changeset
|
132 |
fi |
47748
24550210de0b
enforce our JAVA_HOME to avoid potential conflicts with other Java installations by the user;
wenzelm
parents:
47661
diff
changeset
|
133 |
|
74000 | 134 |
if [ -e "$ISABELLE_SETUP_JAR" ]; then |
76326
a39fa81929d4
avoid spurious error messages, e.g. when scala is missing;
wenzelm
parents:
75654
diff
changeset
|
135 |
ISABELLE_SETUP_CLASSPATH="$(isabelle_jdk java -classpath "$(platform_path "$SCALA_INTERFACES:$ISABELLE_SETUP_JAR")" isabelle.setup.Setup classpath 2>/dev/null)" |
74000 | 136 |
fi |
73988 | 137 |
|
2299
ed9720047d53
getsettings: bash source script to augment current env.
wenzelm
parents:
diff
changeset
|
138 |
set +o allexport |
7770
0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
wenzelm
parents:
6413
diff
changeset
|
139 |
|
0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
wenzelm
parents:
6413
diff
changeset
|
140 |
fi |