clarified settings -- avoid hard-wired directories;
authorwenzelm
Wed Jun 27 20:31:22 2018 +0200 (17 months ago)
changeset 68523ccacc84e0251
parent 68522 d9cbc1e8644d
child 68524 f5ca4c2157a5
child 68536 e14848001c4c
clarified settings -- avoid hard-wired directories;
tuned documentation;
NEWS
etc/settings
src/Doc/System/Environment.thy
src/Doc/System/Server.thy
src/Doc/System/Sessions.thy
src/Pure/Thy/sessions.scala
     1.1 --- a/NEWS	Wed Jun 27 11:16:43 2018 +0200
     1.2 +++ b/NEWS	Wed Jun 27 20:31:22 2018 +0200
     1.3 @@ -474,10 +474,16 @@
     1.4  * The command-line tool "isabelle mkroot -I" initializes a Mercurial
     1.5  repository for the generated session files.
     1.6  
     1.7 +* Settings ISABELLE_HEAPS + ISABELLE_BROWSER_INFO (or
     1.8 +ISABELLE_HEAPS_SYSTEM + ISABELLE_BROWSER_INFO_SYSTEM in "system build
     1.9 +mode") determine the directory locations of the main build artefacts --
    1.10 +instead of hard-wired directories in ISABELLE_HOME_USER (or
    1.11 +ISABELLE_HOME).
    1.12 +
    1.13  * Settings ISABELLE_PATH and ISABELLE_OUTPUT have been discontinued:
    1.14  heap images and session databases are always stored in
    1.15 -$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER (command-line default) or
    1.16 -$ISABELLE_HOME/heaps/$ML_IDENTIFIER (main Isabelle application or
    1.17 +$ISABELLE_HEAPS/$ML_IDENTIFIER (command-line default) or
    1.18 +$ISABELLE_HEAPS_SYSTEM/$ML_IDENTIFIER (main Isabelle application or
    1.19  "isabelle jedit -s" or "isabelle build -s").
    1.20  
    1.21  * ISABELLE_LATEX and ISABELLE_PDFLATEX now include platform-specific
     2.1 --- a/etc/settings	Wed Jun 27 11:16:43 2018 +0200
     2.2 +++ b/etc/settings	Wed Jun 27 20:31:22 2018 +0200
     2.3 @@ -77,8 +77,13 @@
     2.4  # Location for temporary files (should be on a local file system).
     2.5  ISABELLE_TMP_PREFIX="${TMPDIR:-/tmp}/isabelle-$USER"
     2.6  
     2.7 +# Heap locations.
     2.8 +ISABELLE_HEAPS="$ISABELLE_HOME_USER/heaps"
     2.9 +ISABELLE_HEAPS_SYSTEM="$ISABELLE_HOME/heaps"
    2.10 +
    2.11  # HTML browser info.
    2.12  ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
    2.13 +ISABELLE_BROWSER_INFO_SYSTEM="$ISABELLE_HOME/browser_info"
    2.14  
    2.15  # Site settings check -- just to make it a little bit harder to copy this file verbatim!
    2.16  [ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \
     3.1 --- a/src/Doc/System/Environment.thy	Wed Jun 27 11:16:43 2018 +0200
     3.2 +++ b/src/Doc/System/Environment.thy	Wed Jun 27 20:31:22 2018 +0200
     3.3 @@ -175,9 +175,17 @@
     3.4    always the (native) 64 bit variant: \<^verbatim>\<open>x86_64-linux\<close>, \<^verbatim>\<open>x86_64-darwin\<close>,
     3.5    \<^verbatim>\<open>x86_64-windows\<close>.
     3.6  
     3.7 -  \<^descr>[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where theory
     3.8 -  browser information is stored as HTML and PDF (see also \secref{sec:info}).
     3.9 -  The default value is @{path "$ISABELLE_HOME_USER/browser_info"}.
    3.10 +  \<^descr>[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where HTML and PDF
    3.11 +  browser information is stored (see also \secref{sec:info}); its default is
    3.12 +  @{path "$ISABELLE_HOME_USER/browser_info"}. For ``system build mode'' (see
    3.13 +  \secref{sec:tool-build}), @{setting_def ISABELLE_BROWSER_INFO_SYSTEM} is
    3.14 +  used instead; its default is @{path "$ISABELLE_HOME/browser_info"}.
    3.15 +
    3.16 +  \<^descr>[@{setting_def ISABELLE_HEAPS}] is the directory where session heap images,
    3.17 +  log files, and build databases are stored; its default is @{path
    3.18 +  "$ISABELLE_HOME_USER/heaps"}. For ``system build mode'' (see
    3.19 +  \secref{sec:tool-build}), @{setting_def ISABELLE_HEAPS_SYSTEM} is used
    3.20 +  instead; its default is @{path "$ISABELLE_HOME/heaps"}.
    3.21  
    3.22    \<^descr>[@{setting_def ISABELLE_LOGIC}] specifies the default logic to load if none
    3.23    is given explicitely by the user. The default value is \<^verbatim>\<open>HOL\<close>.
     4.1 --- a/src/Doc/System/Server.thy	Wed Jun 27 11:16:43 2018 +0200
     4.2 +++ b/src/Doc/System/Server.thy	Wed Jun 27 20:31:22 2018 +0200
     4.3 @@ -708,9 +708,9 @@
     4.4    in a robust manner, instead of relying on directory locations.
     4.5  
     4.6    \<^medskip>
     4.7 -  The \<open>system_mode\<close> field set to \<^verbatim>\<open>true\<close> stores resulting session images and
     4.8 -  log files in @{path "$ISABELLE_HOME/heaps"} instead of the default location
     4.9 -  @{path "$ISABELLE_HOME_USER/heaps"}. See also option \<^verbatim>\<open>-s\<close> in @{tool build}.
    4.10 +  If \<open>system_mode\<close> is \<^verbatim>\<open>true\<close>, session images are stored in @{path
    4.11 +  "$ISABELLE_HEAPS_SYSTEM"} instead of @{path "$ISABELLE_HEAPS"}. See also
    4.12 +  option \<^verbatim>\<open>-s\<close> in @{tool build} (\secref{sec:tool-build}).
    4.13  
    4.14    \<^medskip>
    4.15    The \<open>verbose\<close> field set to \<^verbatim>\<open>true\<close> yields extra verbosity. The effect is
     5.1 --- a/src/Doc/System/Sessions.thy	Wed Jun 27 11:16:43 2018 +0200
     5.2 +++ b/src/Doc/System/Sessions.thy	Wed Jun 27 20:31:22 2018 +0200
     5.3 @@ -395,9 +395,9 @@
     5.4    performance tuning on Linux servers with separate CPU/memory modules.
     5.5  
     5.6    \<^medskip>
     5.7 -  Option \<^verbatim>\<open>-s\<close> enables \<^emph>\<open>system mode\<close>, which means that resulting heap images
     5.8 -  and log files are stored in @{path "$ISABELLE_HOME/heaps"} instead of the
     5.9 -  default location @{path "$ISABELLE_HOME_USER/heaps"}.
    5.10 +  Option \<^verbatim>\<open>-s\<close> enables \<^emph>\<open>system mode\<close>, which means that session images are
    5.11 +  stored in @{path "$ISABELLE_HEAPS_SYSTEM"} instead of @{path
    5.12 +  "$ISABELLE_HEAPS"}.
    5.13  
    5.14    \<^medskip>
    5.15    Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity. Option \<^verbatim>\<open>-l\<close> lists
     6.1 --- a/src/Pure/Thy/sessions.scala	Wed Jun 27 11:16:43 2018 +0200
     6.2 +++ b/src/Pure/Thy/sessions.scala	Wed Jun 27 20:31:22 2018 +0200
     6.3 @@ -1012,8 +1012,8 @@
     6.4  
     6.5      /* directories */
     6.6  
     6.7 -    val system_output_dir: Path = Path.explode("~~/heaps/$ML_IDENTIFIER")
     6.8 -    val user_output_dir: Path = Path.explode("$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER")
     6.9 +    val system_output_dir: Path = Path.explode("$ISABELLE_HEAPS_SYSTEM/$ML_IDENTIFIER")
    6.10 +    val user_output_dir: Path = Path.explode("$ISABELLE_HEAPS/$ML_IDENTIFIER")
    6.11  
    6.12      val output_dir: Path =
    6.13        if (system_mode) system_output_dir else user_output_dir
    6.14 @@ -1023,7 +1023,7 @@
    6.15        else List(user_output_dir, system_output_dir)
    6.16  
    6.17      val browser_info: Path =
    6.18 -      if (system_mode) Path.explode("~~/browser_info")
    6.19 +      if (system_mode) Path.explode("$ISABELLE_BROWSER_INFO_SYSTEM")
    6.20        else Path.explode("$ISABELLE_BROWSER_INFO")
    6.21  
    6.22