lib/scripts/getsettings
author wenzelm
Wed, 17 May 2017 13:47:19 +0200
changeset 65851 c103358a5559
parent 62588 cd266473b81b
child 67099 3345d53e7c58
permissions -rwxr-xr-x
tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
b1c6f4563df7 removed Ids;
wenzelm
parents: 28504
diff changeset
     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
cb6c4e307b1c slightly more robust re-initialization;
wenzelm
parents: 62414
diff changeset
     7
export ISABELLE_HOME
cb6c4e307b1c slightly more robust re-initialization;
wenzelm
parents: 62414
diff changeset
     8
cb6c4e307b1c slightly more robust re-initialization;
wenzelm
parents: 62414
diff changeset
     9
export BASH_ENV="$ISABELLE_HOME/lib/scripts/getfunctions"
cb6c4e307b1c slightly more robust re-initialization;
wenzelm
parents: 62414
diff changeset
    10
source "$BASH_ENV"
cb6c4e307b1c slightly more robust re-initialization;
wenzelm
parents: 62414
diff changeset
    11
cb6c4e307b1c slightly more robust re-initialization;
wenzelm
parents: 62414
diff changeset
    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
c6111df4a4f8 avoid global state change;
wenzelm
parents: 62412
diff changeset
    16
export ISABELLE_SETTINGS_PRESENT=true
3185
wenzelm
parents: 3118
diff changeset
    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
eee1863c565a remove remains from WinRun4J;
wenzelm
parents: 53967
diff changeset
    28
  unset INI_DIR
eee1863c565a remove remains from WinRun4J;
wenzelm
parents: 53967
diff changeset
    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
2d3d26e9b191 renamed jvmpath to platform_path;
wenzelm
parents: 61293
diff changeset
    40
  CYGWIN_ROOT="$(platform_path "/")"
2d3d26e9b191 renamed jvmpath to platform_path;
wenzelm
parents: 61293
diff changeset
    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
aab984137bcd shell functions for all Isabelle executables;
wenzelm
parents: 56439
diff changeset
    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
aab984137bcd shell functions for all Isabelle executables;
wenzelm
parents: 56439
diff changeset
    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
wenzelm
parents: 41623
diff changeset
    62
source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
48455
a509f19d4cc6 provide explicit ISABELLE_PLATFORM32 as well;
wenzelm
parents: 48448
diff changeset
    63
if [ -z "$ISABELLE_PLATFORM" ]; then
a509f19d4cc6 provide explicit ISABELLE_PLATFORM32 as well;
wenzelm
parents: 48448
diff changeset
    64
  echo 1>&2 "Failed to determine hardware and operating system type!"
a509f19d4cc6 provide explicit ISABELLE_PLATFORM32 as well;
wenzelm
parents: 48448
diff changeset
    65
  exit 2
a509f19d4cc6 provide explicit ISABELLE_PLATFORM32 as well;
wenzelm
parents: 48448
diff changeset
    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
2fe62d602681 isabelle version -i;
wenzelm
parents: 40570
diff changeset
    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
2f83b11c301b added ISABELLE_IDENTIFIER;
wenzelm
parents: 21468
diff changeset
    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
21490
2f83b11c301b added ISABELLE_IDENTIFIER;
wenzelm
parents: 21468
diff changeset
    88
#ML system identifier
6413
b2f2770ef8d9 ML_PLATFORM;
wenzelm
parents: 3185
diff changeset
    89
if [ -z "$ML_PLATFORM" ]; then
b2f2770ef8d9 ML_PLATFORM;
wenzelm
parents: 3185
diff changeset
    90
  ML_IDENTIFIER="$ML_SYSTEM"
b2f2770ef8d9 ML_PLATFORM;
wenzelm
parents: 3185
diff changeset
    91
else
b2f2770ef8d9 ML_PLATFORM;
wenzelm
parents: 3185
diff changeset
    92
  ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
b2f2770ef8d9 ML_PLATFORM;
wenzelm
parents: 3185
diff changeset
    93
fi
21468
c7892915ed10 add ISABELLE_VERSION to ML_IDENTIFIER, unless this is repository or build;
wenzelm
parents: 16293
diff changeset
    94
48838
623ba165d059 direct support for component forests via init_components;
wenzelm
parents: 48837
diff changeset
    95
ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
623ba165d059 direct support for component forests via init_components;
wenzelm
parents: 48837
diff changeset
    96
47748
24550210de0b enforce our JAVA_HOME to avoid potential conflicts with other Java installations by the user;
wenzelm
parents: 47661
diff changeset
    97
#enforce JAVA_HOME
58791
00916b0dd596 clarified ISABELLE_JDK_HOME vs. JAVA_HOME;
wenzelm
parents: 58640
diff changeset
    98
export JAVA_HOME="$ISABELLE_JDK_HOME/jre"
47748
24550210de0b enforce our JAVA_HOME to avoid potential conflicts with other Java installations by the user;
wenzelm
parents: 47661
diff changeset
    99
2299
ed9720047d53 getsettings: bash source script to augment current env.
wenzelm
parents:
diff changeset
   100
set +o allexport
7770
0497323c1f0b ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
wenzelm
parents: 6413
diff changeset
   101
0497323c1f0b ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
wenzelm
parents: 6413
diff changeset
   102
fi