| author | wenzelm | 
| Wed, 17 Oct 2018 22:21:01 +0200 | |
| changeset 69156 | e8ef77b7e1a0 | 
| parent 69153 | 108beabc1bc6 | 
| child 69157 | 22ae1d926f96 | 
| permissions | -rwxr-xr-x | 
| 25434 
746677c843a7
ISABELLE_IDENTIFIER is filled in automatically, not taken from the *long* form of isatool version!
 wenzelm parents: 
21490diff
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: 
62354diff
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: 
62354diff
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: 
6413diff
changeset | 13 | if [ -z "$ISABELLE_SETTINGS_PRESENT" ] | 
| 
0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
 wenzelm parents: 
6413diff
changeset | 14 | then | 
| 
0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
 wenzelm parents: 
6413diff
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: 
62354diff
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: 
53580diff
changeset | 19 | |
| 57411 
9444489766a1
sane environment defaults for Mac OS X, based on former App1/script -- e.g. relevant for MacTeX PATH;
 wenzelm parents: 
56448diff
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: 
56448diff
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: 
56448diff
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: 
56448diff
changeset | 23 | fi | 
| 
9444489766a1
sane environment defaults for Mac OS X, based on former App1/script -- e.g. relevant for MacTeX PATH;
 wenzelm parents: 
56448diff
changeset | 24 | |
| 48838 
623ba165d059
direct support for component forests via init_components;
 wenzelm parents: 
48837diff
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: 
47254diff
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: 
47254diff
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: 
58413diff
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: 
58413diff
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: 
58413diff
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: 
58413diff
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: 
58413diff
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: 
58413diff
changeset | 35 | |
| 47661 
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
 wenzelm parents: 
47525diff
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: 
58791diff
changeset | 37 | USER_HOME="$(cygpath -u "$USERPROFILE")" | 
| 47661 
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
 wenzelm parents: 
47525diff
changeset | 38 | fi | 
| 
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
 wenzelm parents: 
47525diff
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: 
52443diff
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: 
52443diff
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: 
52443diff
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: 
47254diff
changeset | 45 | else | 
| 47661 
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
 wenzelm parents: 
47525diff
changeset | 46 | if [ -z "$USER_HOME" ]; then | 
| 
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
 wenzelm parents: 
47525diff
changeset | 47 | USER_HOME="$HOME" | 
| 
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
 wenzelm parents: 
47525diff
changeset | 48 | fi | 
| 
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
 wenzelm parents: 
47525diff
changeset | 49 | |
| 61293 
876e7eae22be
clarified ISABELLE_ROOT (platform path) vs. ISABELLE_HOME (standard path);
 wenzelm parents: 
61159diff
changeset | 50 | ISABELLE_ROOT="$ISABELLE_HOME" | 
| 
876e7eae22be
clarified ISABELLE_ROOT (platform path) vs. ISABELLE_HOME (standard path);
 wenzelm parents: 
61159diff
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: 
52443diff
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: 
52443diff
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: 
47254diff
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: 
47254diff
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: 
62354diff
changeset | 56 | #main executables | 
| 56440 | 57 | ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle" | 
| 56448 
344800503974
provide old-style ISABELLE_SCALA_SCRIPT for uniformity;
 wenzelm parents: 
56440diff
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: 
62413diff
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: 
36194diff
changeset | 61 | #platform | 
| 41758 | 62 | source "$ISABELLE_HOME/lib/scripts/isabelle-platform" | 
| 48455 | 63 | if [ -z "$ISABELLE_PLATFORM" ]; then | 
| 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: 
36194diff
changeset | 67 | |
| 25434 
746677c843a7
ISABELLE_IDENTIFIER is filled in automatically, not taken from the *long* form of isatool version!
 wenzelm parents: 
21490diff
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: 
48790diff
changeset | 70 | [ -z "$ISABELLE_IDENTIFIER" ] && ISABELLE_IDENTIFIER="" | 
| 21490 | 71 | |
| 48838 
623ba165d059
direct support for component forests via init_components;
 wenzelm parents: 
48837diff
changeset | 72 | |
| 
623ba165d059
direct support for component forests via init_components;
 wenzelm parents: 
48837diff
changeset | 73 | # components | 
| 
623ba165d059
direct support for component forests via init_components;
 wenzelm parents: 
48837diff
changeset | 74 | |
| 32305 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
 wenzelm parents: 
31520diff
changeset | 75 | ISABELLE_COMPONENTS="" | 
| 48838 
623ba165d059
direct support for component forests via init_components;
 wenzelm parents: 
48837diff
changeset | 76 | ISABELLE_COMPONENTS_MISSING="" | 
| 
623ba165d059
direct support for component forests via init_components;
 wenzelm parents: 
48837diff
changeset | 77 | |
| 32305 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
 wenzelm parents: 
31520diff
changeset | 78 | #main components | 
| 
c5523ded51d9
basic support for components (which imitate the usual Isabelle directory layout);
 wenzelm parents: 
31520diff
changeset | 79 | init_component "$ISABELLE_HOME" | 
| 48725 
e852f4d6af80
configure Admin as component, with its own lib/Tools;
 wenzelm parents: 
48551diff
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: 
61294diff
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: 
61294diff
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: 
61294diff
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: 
61294diff
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: 
61294diff
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: 
61294diff
changeset | 86 | fi | 
| 48838 
623ba165d059
direct support for component forests via init_components;
 wenzelm parents: 
48837diff
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: 
16293diff
changeset | 101 | |
| 69152 
77eede3f40e2
enforce settings that are likely to be outdated, e.g. in $ISABELLE_HOME_USER/etc/settings;
 wenzelm parents: 
69151diff
changeset | 102 | #enforce ISABELLE_OCAML | 
| 
77eede3f40e2
enforce settings that are likely to be outdated, e.g. in $ISABELLE_HOME_USER/etc/settings;
 wenzelm parents: 
69151diff
changeset | 103 | if [ -f "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin/ocaml" ]; then | 
| 69135 | 104 | ISABELLE_OCAML="$ISABELLE_HOME/lib/Tools/ocaml" | 
| 105 | fi | |
| 69152 
77eede3f40e2
enforce settings that are likely to be outdated, e.g. in $ISABELLE_HOME_USER/etc/settings;
 wenzelm parents: 
69151diff
changeset | 106 | |
| 
77eede3f40e2
enforce settings that are likely to be outdated, e.g. in $ISABELLE_HOME_USER/etc/settings;
 wenzelm parents: 
69151diff
changeset | 107 | #enforce ISABELLE_OCAMLC | 
| 
77eede3f40e2
enforce settings that are likely to be outdated, e.g. in $ISABELLE_HOME_USER/etc/settings;
 wenzelm parents: 
69151diff
changeset | 108 | if [ -f "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin/ocamlc" ]; then | 
| 69135 | 109 | ISABELLE_OCAMLC="$ISABELLE_HOME/lib/Tools/ocamlc" | 
| 110 | fi | |
| 111 | ||
| 69152 
77eede3f40e2
enforce settings that are likely to be outdated, e.g. in $ISABELLE_HOME_USER/etc/settings;
 wenzelm parents: 
69151diff
changeset | 112 | #enforce ISABELLE_GHC | 
| 69153 
108beabc1bc6
avoid strict evaluation of "isabelle_stack path --programs";
 wenzelm parents: 
69152diff
changeset | 113 | if [ -d "$ISABELLE_STACK_ROOT" ]; then | 
| 69156 | 114 | if [ -f "$(isabelle_stack path --programs)/$ISABELLE_GHC_VERSION/bin/ghc" ]; then | 
| 69153 
108beabc1bc6
avoid strict evaluation of "isabelle_stack path --programs";
 wenzelm parents: 
69152diff
changeset | 115 | ISABELLE_GHC="$ISABELLE_HOME/lib/Tools/ghc" | 
| 
108beabc1bc6
avoid strict evaluation of "isabelle_stack path --programs";
 wenzelm parents: 
69152diff
changeset | 116 | fi | 
| 69151 | 117 | fi | 
| 118 | ||
| 47748 
24550210de0b
enforce our JAVA_HOME to avoid potential conflicts with other Java installations by the user;
 wenzelm parents: 
47661diff
changeset | 119 | #enforce JAVA_HOME | 
| 68012 
6d38b4fd872e
more robust, notably for jdk-10.0.1 where jre is absent;
 wenzelm parents: 
67099diff
changeset | 120 | if [ -d "$ISABELLE_JDK_HOME/jre" ] | 
| 
6d38b4fd872e
more robust, notably for jdk-10.0.1 where jre is absent;
 wenzelm parents: 
67099diff
changeset | 121 | then | 
| 
6d38b4fd872e
more robust, notably for jdk-10.0.1 where jre is absent;
 wenzelm parents: 
67099diff
changeset | 122 | export JAVA_HOME="$ISABELLE_JDK_HOME/jre" | 
| 
6d38b4fd872e
more robust, notably for jdk-10.0.1 where jre is absent;
 wenzelm parents: 
67099diff
changeset | 123 | else | 
| 
6d38b4fd872e
more robust, notably for jdk-10.0.1 where jre is absent;
 wenzelm parents: 
67099diff
changeset | 124 | export JAVA_HOME="$ISABELLE_JDK_HOME" | 
| 
6d38b4fd872e
more robust, notably for jdk-10.0.1 where jre is absent;
 wenzelm parents: 
67099diff
changeset | 125 | fi | 
| 47748 
24550210de0b
enforce our JAVA_HOME to avoid potential conflicts with other Java installations by the user;
 wenzelm parents: 
47661diff
changeset | 126 | |
| 2299 
ed9720047d53
getsettings: bash source script to augment current env.
 wenzelm parents: diff
changeset | 127 | set +o allexport | 
| 7770 
0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
 wenzelm parents: 
6413diff
changeset | 128 | |
| 
0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
 wenzelm parents: 
6413diff
changeset | 129 | fi |