isabelle: lib/scripts/getsettings@9a28fc03c3fe (annotated)

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 7a6c933d51d0 tuned; 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 a231e6110f9b tuned; 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

author	wenzelm
	Fri, 26 May 2017 11:09:16 +0200
changeset 65930	9a28fc03c3fe
parent 62588	cd266473b81b
child 67099	3345d53e7c58
permissions	-rwxr-xr-x