# HG changeset patch # User wenzelm # Date 1530124282 -7200 # Node ID ccacc84e02518a177b0db087bab0526071f43313 # Parent d9cbc1e8644d354dc6211f8ef08d04cd9a9f503f clarified settings -- avoid hard-wired directories; tuned documentation; diff -r d9cbc1e8644d -r ccacc84e0251 NEWS --- a/NEWS Wed Jun 27 11:16:43 2018 +0200 +++ b/NEWS Wed Jun 27 20:31:22 2018 +0200 @@ -474,10 +474,16 @@ * The command-line tool "isabelle mkroot -I" initializes a Mercurial repository for the generated session files. +* Settings ISABELLE_HEAPS + ISABELLE_BROWSER_INFO (or +ISABELLE_HEAPS_SYSTEM + ISABELLE_BROWSER_INFO_SYSTEM in "system build +mode") determine the directory locations of the main build artefacts -- +instead of hard-wired directories in ISABELLE_HOME_USER (or +ISABELLE_HOME). + * Settings ISABELLE_PATH and ISABELLE_OUTPUT have been discontinued: heap images and session databases are always stored in -$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER (command-line default) or -$ISABELLE_HOME/heaps/$ML_IDENTIFIER (main Isabelle application or +$ISABELLE_HEAPS/$ML_IDENTIFIER (command-line default) or +$ISABELLE_HEAPS_SYSTEM/$ML_IDENTIFIER (main Isabelle application or "isabelle jedit -s" or "isabelle build -s"). * ISABELLE_LATEX and ISABELLE_PDFLATEX now include platform-specific diff -r d9cbc1e8644d -r ccacc84e0251 etc/settings --- a/etc/settings Wed Jun 27 11:16:43 2018 +0200 +++ b/etc/settings Wed Jun 27 20:31:22 2018 +0200 @@ -77,8 +77,13 @@ # Location for temporary files (should be on a local file system). ISABELLE_TMP_PREFIX="${TMPDIR:-/tmp}/isabelle-$USER" +# Heap locations. +ISABELLE_HEAPS="$ISABELLE_HOME_USER/heaps" +ISABELLE_HEAPS_SYSTEM="$ISABELLE_HOME/heaps" + # HTML browser info. ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" +ISABELLE_BROWSER_INFO_SYSTEM="$ISABELLE_HOME/browser_info" # Site settings check -- just to make it a little bit harder to copy this file verbatim! [ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \ diff -r d9cbc1e8644d -r ccacc84e0251 src/Doc/System/Environment.thy --- a/src/Doc/System/Environment.thy Wed Jun 27 11:16:43 2018 +0200 +++ b/src/Doc/System/Environment.thy Wed Jun 27 20:31:22 2018 +0200 @@ -175,9 +175,17 @@ always the (native) 64 bit variant: \<^verbatim>\x86_64-linux\, \<^verbatim>\x86_64-darwin\, \<^verbatim>\x86_64-windows\. - \<^descr>[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where theory - browser information is stored as HTML and PDF (see also \secref{sec:info}). - The default value is @{path "$ISABELLE_HOME_USER/browser_info"}. + \<^descr>[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where HTML and PDF + browser information is stored (see also \secref{sec:info}); its default is + @{path "$ISABELLE_HOME_USER/browser_info"}. For ``system build mode'' (see + \secref{sec:tool-build}), @{setting_def ISABELLE_BROWSER_INFO_SYSTEM} is + used instead; its default is @{path "$ISABELLE_HOME/browser_info"}. + + \<^descr>[@{setting_def ISABELLE_HEAPS}] is the directory where session heap images, + log files, and build databases are stored; its default is @{path + "$ISABELLE_HOME_USER/heaps"}. For ``system build mode'' (see + \secref{sec:tool-build}), @{setting_def ISABELLE_HEAPS_SYSTEM} is used + instead; its default is @{path "$ISABELLE_HOME/heaps"}. \<^descr>[@{setting_def ISABELLE_LOGIC}] specifies the default logic to load if none is given explicitely by the user. The default value is \<^verbatim>\HOL\. diff -r d9cbc1e8644d -r ccacc84e0251 src/Doc/System/Server.thy --- a/src/Doc/System/Server.thy Wed Jun 27 11:16:43 2018 +0200 +++ b/src/Doc/System/Server.thy Wed Jun 27 20:31:22 2018 +0200 @@ -708,9 +708,9 @@ in a robust manner, instead of relying on directory locations. \<^medskip> - The \system_mode\ field set to \<^verbatim>\true\ stores resulting session images and - log files in @{path "$ISABELLE_HOME/heaps"} instead of the default location - @{path "$ISABELLE_HOME_USER/heaps"}. See also option \<^verbatim>\-s\ in @{tool build}. + If \system_mode\ is \<^verbatim>\true\, session images are stored in @{path + "$ISABELLE_HEAPS_SYSTEM"} instead of @{path "$ISABELLE_HEAPS"}. See also + option \<^verbatim>\-s\ in @{tool build} (\secref{sec:tool-build}). \<^medskip> The \verbose\ field set to \<^verbatim>\true\ yields extra verbosity. The effect is diff -r d9cbc1e8644d -r ccacc84e0251 src/Doc/System/Sessions.thy --- a/src/Doc/System/Sessions.thy Wed Jun 27 11:16:43 2018 +0200 +++ b/src/Doc/System/Sessions.thy Wed Jun 27 20:31:22 2018 +0200 @@ -395,9 +395,9 @@ performance tuning on Linux servers with separate CPU/memory modules. \<^medskip> - Option \<^verbatim>\-s\ enables \<^emph>\system mode\, which means that resulting heap images - and log files are stored in @{path "$ISABELLE_HOME/heaps"} instead of the - default location @{path "$ISABELLE_HOME_USER/heaps"}. + Option \<^verbatim>\-s\ enables \<^emph>\system mode\, which means that session images are + stored in @{path "$ISABELLE_HEAPS_SYSTEM"} instead of @{path + "$ISABELLE_HEAPS"}. \<^medskip> Option \<^verbatim>\-v\ increases the general level of verbosity. Option \<^verbatim>\-l\ lists diff -r d9cbc1e8644d -r ccacc84e0251 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Wed Jun 27 11:16:43 2018 +0200 +++ b/src/Pure/Thy/sessions.scala Wed Jun 27 20:31:22 2018 +0200 @@ -1012,8 +1012,8 @@ /* directories */ - val system_output_dir: Path = Path.explode("~~/heaps/$ML_IDENTIFIER") - val user_output_dir: Path = Path.explode("$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER") + val system_output_dir: Path = Path.explode("$ISABELLE_HEAPS_SYSTEM/$ML_IDENTIFIER") + val user_output_dir: Path = Path.explode("$ISABELLE_HEAPS/$ML_IDENTIFIER") val output_dir: Path = if (system_mode) system_output_dir else user_output_dir @@ -1023,7 +1023,7 @@ else List(user_output_dir, system_output_dir) val browser_info: Path = - if (system_mode) Path.explode("~~/browser_info") + if (system_mode) Path.explode("$ISABELLE_BROWSER_INFO_SYSTEM") else Path.explode("$ISABELLE_BROWSER_INFO")