author  wenzelm 
Thu, 15 Jul 2021 22:09:45 +0200  
changeset 74000  4313e6c9969a 
parent 73992  fecbf83ab281 
permissions  rwxrxrx 
25434
746677c843a7
ISABELLE_IDENTIFIER is filled in automatically, not taken from the *long* form of isatool version!
wenzelm
parents:
21490
diff
changeset

1 
# * shellscript * :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 

58640
37f852399a32
prefer original TEMP from Windows, e.g. relevant for Isabelle distribution within readonly 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 readonly 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 readonly 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 readonly 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 readonly 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 readonly 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 crossplatform 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 crossplatform user home directory;
wenzelm
parents:
47525
diff
changeset

38 
fi 
012a887997f3
USER_HOME settings variable points to crossplatform 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 addon 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 addon 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 addon 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 crossplatform user home directory;
wenzelm
parents:
47525
diff
changeset

46 
if [ z "$USER_HOME" ]; then 
012a887997f3
USER_HOME settings variable points to crossplatform user home directory;
wenzelm
parents:
47525
diff
changeset

47 
USER_HOME="$HOME" 
012a887997f3
USER_HOME settings variable points to crossplatform user home directory;
wenzelm
parents:
47525
diff
changeset

48 
fi 
012a887997f3
USER_HOME settings variable points to crossplatform 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 addon 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 addon 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 

72161  56 
#init cumulative settings 
57 
ISABELLE_FONTS="" 

58 
ISABELLE_FONTS_HIDDEN="" 

59 
ISABELLE_SCALA_SERVICES="" 

72162  60 
ISABELLE_DIRECTORIES="" 
72161  61 

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

62 
#main executables 
56440  63 
ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle" 
56448
344800503974
provide oldstyle ISABELLE_SCALA_SCRIPT for uniformity;
wenzelm
parents:
56440
diff
changeset

64 
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

65 
PATH="$ISABELLE_HOME/bin:$PATH" 
56440  66 

36196
cbb9ee265cdd
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64  NB: ML and JVM may have a different idea;
wenzelm
parents:
36194
diff
changeset

67 
#platform 
41758  68 
source "$ISABELLE_HOME/lib/scripts/isabelleplatform" 
71344  69 
if [ z "$ISABELLE_PLATFORM_FAMILY" ]; then 
48455  70 
echo 1>&2 "Failed to determine hardware and operating system type!" 
71 
exit 2 

72 
fi 

36196
cbb9ee265cdd
added ISABELLE_PLATFORM and ISABELLE_PLATFORM64  NB: ML and JVM may have a different idea;
wenzelm
parents:
36194
diff
changeset

73 

73523
2cd23d587db9
further clarification of Isabelle distribution identification  avoid odd patching of sources;
wenzelm
parents:
73520
diff
changeset

74 
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

75 
then 
2cd23d587db9
further clarification of Isabelle distribution identification  avoid odd patching of sources;
wenzelm
parents:
73520
diff
changeset

76 
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

77 
fi 
2cd23d587db9
further clarification of Isabelle distribution identification  avoid odd patching of sources;
wenzelm
parents:
73520
diff
changeset

78 

2cd23d587db9
further clarification of Isabelle distribution identification  avoid odd patching of sources;
wenzelm
parents:
73520
diff
changeset

79 
ISABELLE_NAME="${ISABELLE_IDENTIFIER:Isabelle}" 
21490  80 

48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

81 

623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

82 
# components 
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

83 

32305
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset

84 
ISABELLE_COMPONENTS="" 
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

85 
ISABELLE_COMPONENTS_MISSING="" 
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

86 

32305
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset

87 
#main components 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
wenzelm
parents:
31520
diff
changeset

88 
init_component "$ISABELLE_HOME" 
48725
e852f4d6af80
configure Admin as component, with its own lib/Tools;
wenzelm
parents:
48551
diff
changeset

89 
[ 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

90 
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

91 
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

92 
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

93 
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

94 
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

95 
fi 
48838
623ba165d059
direct support for component forests via init_components;
wenzelm
parents:
48837
diff
changeset

96 

67099  97 
#POLYML_EXE 
98 
if [ "$ISABELLE_PLATFORM_FAMILY" = "windows" ]; then 

99 
POLYML_EXE="$ML_HOME/poly.exe" 

100 
else 

101 
POLYML_EXE="$ML_HOME/poly" 

102 
fi 

103 

21490  104 
#ML system identifier 
6413  105 
if [ z "$ML_PLATFORM" ]; then 
106 
ML_IDENTIFIER="$ML_SYSTEM" 

107 
else 

108 
ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}" 

109 
fi 

21468
c7892915ed10
add ISABELLE_VERSION to ML_IDENTIFIER, unless this is repository or build;
wenzelm
parents:
16293
diff
changeset

110 

69926
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69910
diff
changeset

111 
#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

112 
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

113 
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

114 
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

115 

69152
77eede3f40e2
enforce settings that are likely to be outdated, e.g. in $ISABELLE_HOME_USER/etc/settings;
wenzelm
parents:
69151
diff
changeset

116 
#enforce ISABELLE_GHC 
69930
b5286c564861
more robust reference to ghc exe (with multiplatform support);
wenzelm
parents:
69926
diff
changeset

117 
if [ f "$ISABELLE_STACK_ROOT/ISABELLE_GHC_EXE$ISABELLE_PLATFORM_FAMILY" ]; then 
b5286c564861
more robust reference to ghc exe (with multiplatform support);
wenzelm
parents:
69926
diff
changeset

118 
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

119 
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

120 
ISABELLE_GHC_STACK=true 
69153
108beabc1bc6
avoid strict evaluation of "isabelle_stack path programs";
wenzelm
parents:
69152
diff
changeset

121 
fi 
69151  122 
fi 
123 

47748
24550210de0b
enforce our JAVA_HOME to avoid potential conflicts with other Java installations by the user;
wenzelm
parents:
47661
diff
changeset

124 
#enforce JAVA_HOME 
68012
6d38b4fd872e
more robust, notably for jdk10.0.1 where jre is absent;
wenzelm
parents:
67099
diff
changeset

125 
if [ d "$ISABELLE_JDK_HOME/jre" ] 
6d38b4fd872e
more robust, notably for jdk10.0.1 where jre is absent;
wenzelm
parents:
67099
diff
changeset

126 
then 
6d38b4fd872e
more robust, notably for jdk10.0.1 where jre is absent;
wenzelm
parents:
67099
diff
changeset

127 
export JAVA_HOME="$ISABELLE_JDK_HOME/jre" 
6d38b4fd872e
more robust, notably for jdk10.0.1 where jre is absent;
wenzelm
parents:
67099
diff
changeset

128 
else 
6d38b4fd872e
more robust, notably for jdk10.0.1 where jre is absent;
wenzelm
parents:
67099
diff
changeset

129 
export JAVA_HOME="$ISABELLE_JDK_HOME" 
6d38b4fd872e
more robust, notably for jdk10.0.1 where jre is absent;
wenzelm
parents:
67099
diff
changeset

130 
fi 
47748
24550210de0b
enforce our JAVA_HOME to avoid potential conflicts with other Java installations by the user;
wenzelm
parents:
47661
diff
changeset

131 

74000  132 
if [ e "$ISABELLE_SETUP_JAR" ]; then 
133 
ISABELLE_SETUP_CLASSPATH="$(isabelle_java java jar "$(platform_path "$ISABELLE_SETUP_JAR")" classpath)" 

134 
fi 

73988  135 

2299
ed9720047d53
getsettings: bash source script to augment current env.
wenzelm
parents:
diff
changeset

136 
set +o allexport 
7770
0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
wenzelm
parents:
6413
diff
changeset

137 

0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
wenzelm
parents:
6413
diff
changeset

138 
fi 