lib/scripts/getsettings
author wenzelm
Fri, 07 Aug 2020 11:46:14 +0200
changeset 72110 16fab31feadc
parent 71344 ee9998bb417b
child 72161 cf443b24ad90
permissions -rwxr-xr-x
avoid failure of "isabelle build -o skip_proofs";
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"
71344
wenzelm
parents: 71342
diff changeset
    63
if [ -z "$ISABELLE_PLATFORM_FAMILY" ]; then
48455
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
67099
3345d53e7c58 updated to official release of polyml-5.7.1;
wenzelm
parents: 62588
diff changeset
    88
#POLYML_EXE
3345d53e7c58 updated to official release of polyml-5.7.1;
wenzelm
parents: 62588
diff changeset
    89
if [ "$ISABELLE_PLATFORM_FAMILY" = "windows" ]; then
3345d53e7c58 updated to official release of polyml-5.7.1;
wenzelm
parents: 62588
diff changeset
    90
  POLYML_EXE="$ML_HOME/poly.exe"
3345d53e7c58 updated to official release of polyml-5.7.1;
wenzelm
parents: 62588
diff changeset
    91
else
3345d53e7c58 updated to official release of polyml-5.7.1;
wenzelm
parents: 62588
diff changeset
    92
  POLYML_EXE="$ML_HOME/poly"
3345d53e7c58 updated to official release of polyml-5.7.1;
wenzelm
parents: 62588
diff changeset
    93
fi
3345d53e7c58 updated to official release of polyml-5.7.1;
wenzelm
parents: 62588
diff changeset
    94
21490
2f83b11c301b added ISABELLE_IDENTIFIER;
wenzelm
parents: 21468
diff changeset
    95
#ML system identifier
6413
b2f2770ef8d9 ML_PLATFORM;
wenzelm
parents: 3185
diff changeset
    96
if [ -z "$ML_PLATFORM" ]; then
b2f2770ef8d9 ML_PLATFORM;
wenzelm
parents: 3185
diff changeset
    97
  ML_IDENTIFIER="$ML_SYSTEM"
b2f2770ef8d9 ML_PLATFORM;
wenzelm
parents: 3185
diff changeset
    98
else
b2f2770ef8d9 ML_PLATFORM;
wenzelm
parents: 3185
diff changeset
    99
  ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
b2f2770ef8d9 ML_PLATFORM;
wenzelm
parents: 3185
diff changeset
   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
b310bc57f55f support for GHC via command-line tools;
wenzelm
parents: 69135
diff changeset
   113
fi
b310bc57f55f support for GHC via command-line tools;
wenzelm
parents: 69135
diff changeset
   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