author | wenzelm |
Fri, 07 Aug 2020 11:46:14 +0200 | |
changeset 72110 | 16fab31feadc |
parent 71344 | ee9998bb417b |
child 72161 | cf443b24ad90 |
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 |
|
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
|
20 |
#sane environment defaults (notably on Mac OS X) |
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 |
||
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
|
30 |
if [ -n "$TEMP_WINDOWS" ]; then |
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
|
31 |
TMPDIR="$(cygpath -u "$TEMP_WINDOWS")" |
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
|
32 |
TMP="$TMPDIR" |
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 |
TEMP="$TMPDIR" |
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
|
34 |
fi |
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
|
35 |
|
47661
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
47525
diff
changeset
|
36 |
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
|
37 |
USER_HOME="$(cygpath -u "$USERPROFILE")" |
47661
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
47525
diff
changeset
|
38 |
fi |
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
47525
diff
changeset
|
39 |
|
61294 | 40 |
CYGWIN_ROOT="$(platform_path "/")" |
41 |
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
|
42 |
|
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
|
43 |
ISABELLE_CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")" |
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
|
44 |
unset 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
|
45 |
else |
47661
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
47525
diff
changeset
|
46 |
if [ -z "$USER_HOME" ]; then |
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
47525
diff
changeset
|
47 |
USER_HOME="$HOME" |
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
47525
diff
changeset
|
48 |
fi |
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
47525
diff
changeset
|
49 |
|
61293
876e7eae22be
clarified ISABELLE_ROOT (platform path) vs. ISABELLE_HOME (standard path);
wenzelm
parents:
61159
diff
changeset
|
50 |
ISABELLE_ROOT="$ISABELLE_HOME" |
876e7eae22be
clarified ISABELLE_ROOT (platform path) vs. ISABELLE_HOME (standard path);
wenzelm
parents:
61159
diff
changeset
|
51 |
|
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
|
52 |
ISABELLE_CLASSPATH="$CLASSPATH" |
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
|
53 |
unset 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
|
54 |
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
|
55 |
|
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
|
56 |
#main executables |
56440 | 57 |
ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle" |
56448
344800503974
provide old-style ISABELLE_SCALA_SCRIPT for uniformity;
wenzelm
parents:
56440
diff
changeset
|
58 |
ISABELLE_SCALA_SCRIPT="$ISABELLE_HOME/bin/isabelle_scala_script" |
62414
1abd90afe387
within the Isabelle environment, main executables are always within PATH;
wenzelm
parents:
62413
diff
changeset
|
59 |
PATH="$ISABELLE_HOME/bin:$PATH" |
56440 | 60 |
|
36196
cbb9ee265cdd
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
wenzelm
parents:
36194
diff
changeset
|
61 |
#platform |
41758 | 62 |
source "$ISABELLE_HOME/lib/scripts/isabelle-platform" |
71344 | 63 |
if [ -z "$ISABELLE_PLATFORM_FAMILY" ]; then |
48455 | 64 |
echo 1>&2 "Failed to determine hardware and operating system type!" |
65 |
exit 2 |
|
66 |
fi |
|
36196
cbb9ee265cdd
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;
wenzelm
parents:
36194
diff
changeset
|
67 |
|
25434
746677c843a7
ISABELLE_IDENTIFIER is filled in automatically, not taken from the *long* form of isatool version!
wenzelm
parents:
21490
diff
changeset
|
68 |
#Isabelle distribution identifier -- filled in automatically! |
41511 | 69 |
ISABELLE_ID="" |
48837
d1d806a42c91
allow to provide external ISABELLE_IDENTIFIER for repository clone -- potentially relevant for isatest and mira;
wenzelm
parents:
48790
diff
changeset
|
70 |
[ -z "$ISABELLE_IDENTIFIER" ] && ISABELLE_IDENTIFIER="" |
21490 | 71 |
|
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
72 |
|
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
73 |
# components |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
74 |
|
32305
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
75 |
ISABELLE_COMPONENTS="" |
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
76 |
ISABELLE_COMPONENTS_MISSING="" |
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
77 |
|
32305
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
78 |
#main components |
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset
|
79 |
init_component "$ISABELLE_HOME" |
48725
e852f4d6af80
configure Admin as component, with its own lib/Tools;
wenzelm
parents:
48551
diff
changeset
|
80 |
[ -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
|
81 |
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
|
82 |
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
|
83 |
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
|
84 |
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
|
85 |
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
|
86 |
fi |
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset
|
87 |
|
67099 | 88 |
#POLYML_EXE |
89 |
if [ "$ISABELLE_PLATFORM_FAMILY" = "windows" ]; then |
|
90 |
POLYML_EXE="$ML_HOME/poly.exe" |
|
91 |
else |
|
92 |
POLYML_EXE="$ML_HOME/poly" |
|
93 |
fi |
|
94 |
||
21490 | 95 |
#ML system identifier |
6413 | 96 |
if [ -z "$ML_PLATFORM" ]; then |
97 |
ML_IDENTIFIER="$ML_SYSTEM" |
|
98 |
else |
|
99 |
ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}" |
|
100 |
fi |
|
21468
c7892915ed10
add ISABELLE_VERSION to ML_IDENTIFIER, unless this is repository or build;
wenzelm
parents:
16293
diff
changeset
|
101 |
|
69926
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69910
diff
changeset
|
102 |
#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
|
103 |
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
|
104 |
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
|
105 |
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
|
106 |
|
69152
77eede3f40e2
enforce settings that are likely to be outdated, e.g. in $ISABELLE_HOME_USER/etc/settings;
wenzelm
parents:
69151
diff
changeset
|
107 |
#enforce ISABELLE_GHC |
69930
b5286c564861
more robust reference to ghc exe (with multi-platform support);
wenzelm
parents:
69926
diff
changeset
|
108 |
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
|
109 |
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
|
110 |
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
|
111 |
ISABELLE_GHC_STACK=true |
69153
108beabc1bc6
avoid strict evaluation of "isabelle_stack path --programs";
wenzelm
parents:
69152
diff
changeset
|
112 |
fi |
69151 | 113 |
fi |
114 |
||
47748
24550210de0b
enforce our JAVA_HOME to avoid potential conflicts with other Java installations by the user;
wenzelm
parents:
47661
diff
changeset
|
115 |
#enforce JAVA_HOME |
68012
6d38b4fd872e
more robust, notably for jdk-10.0.1 where jre is absent;
wenzelm
parents:
67099
diff
changeset
|
116 |
if [ -d "$ISABELLE_JDK_HOME/jre" ] |
6d38b4fd872e
more robust, notably for jdk-10.0.1 where jre is absent;
wenzelm
parents:
67099
diff
changeset
|
117 |
then |
6d38b4fd872e
more robust, notably for jdk-10.0.1 where jre is absent;
wenzelm
parents:
67099
diff
changeset
|
118 |
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
|
119 |
else |
6d38b4fd872e
more robust, notably for jdk-10.0.1 where jre is absent;
wenzelm
parents:
67099
diff
changeset
|
120 |
export JAVA_HOME="$ISABELLE_JDK_HOME" |
6d38b4fd872e
more robust, notably for jdk-10.0.1 where jre is absent;
wenzelm
parents:
67099
diff
changeset
|
121 |
fi |
47748
24550210de0b
enforce our JAVA_HOME to avoid potential conflicts with other Java installations by the user;
wenzelm
parents:
47661
diff
changeset
|
122 |
|
2299
ed9720047d53
getsettings: bash source script to augment current env.
wenzelm
parents:
diff
changeset
|
123 |
set +o allexport |
7770
0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
wenzelm
parents:
6413
diff
changeset
|
124 |
|
0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
wenzelm
parents:
6413
diff
changeset
|
125 |
fi |