Quelle  Environment.thy   Sprache: Isabelle

(*:maxLineLen=78:*)

theory Environment
imports Base
begin

chapter ‹The Isabelle system environment›

text ‹
  This manual describes Isabelle together with related tools as seen from a
  system oriented view. See also the 🚫‹Isabelle/Isar Reference Manual›
  🍋‹"isabelle-isar-ref"› for the actual Isabelle input language and
  related concepts, and 🚫‹The Isabelle/Isar Implementation Manual›
  🍋‹"isabelle-implementation"› for the main concepts of the underlying
  implementation in Isabelle/ML.
›


section ‹Isabelle settings \label{sec:settings}›

text ‹
  Isabelle executables may depend on the 🚫‹Isabelle settings› within the
  process environment. This is a statically scoped collection of environment
  variables, such as @{setting ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting
  POLYML_HOME}. These variables are 🚫‹not› intended to be set directly from the
  shell, but are provided by Isabelle 🚫‹components› within their 🚫‹settings
  files›, as explained below.
›


subsection ‹Bootstrapping the environment \label{sec:boot}›

text ‹
  Isabelle executables need to be run within a proper settings environment.
  This is bootstrapped as described below, on the first invocation of one of
  the outer wrapper scripts (such as @{executable_ref isabelle}). This happens
  only once for each process tree, i.e.\ the environment is passed to
  subprocesses according to regular Unix conventions.

    🚫 The special variable @{setting_def ISABELLE_HOME} is determined
    automatically from the location of the binary that has been run.

    You should not try to set @{setting ISABELLE_HOME} manually. Also note
    that the Isabelle executables either have to be run from their original
    location in the distribution directory, or via the executable objects
    created by the @{tool install} tool. Symbolic links are admissible, but a
    plain copy of the 🍋‹$ISABELLE_HOME/bin› files will not work!

    🚫 The file 🍋‹$ISABELLE_HOME/etc/settings› is run as a @{executable_ref
    bash} shell script with the auto-export option for variables enabled.

    This file holds a rather long list of shell variable assignments, thus
    providing the site-wide default settings. The Isabelle distribution
    already contains a global settings file with sensible defaults for most
    variables.

    🚫 The file 🍋‹$ISABELLE_HOME_USER/etc/settings› (if it
    exists) is run in the same way as the site default settings. Note that the
    variable @{setting ISABELLE_HOME_USER} has already been set before ---
    usually to something like 🍋‹$USER_HOME/.isabelle/Isabelle2025-1›.

    Thus individual users may override the site-wide defaults. Typically, a
    user settings file contains only a few lines, with some assignments that
    are actually changed. Never copy the central
    🍋‹$ISABELLE_HOME/etc/settings› file!

  Since settings files are regular GNU @{executable_def bash} scripts, one may
  use complex shell commands, such as 🍋‹if› or 🍋‹case› statements to set
  variables depending on the system architecture or other environment
  variables. Such advanced features should be added only with great care,
  though. In particular, external environment references should be kept at a
  minimum.

  🚫
  A few variables are somewhat special, e.g.\ @{setting_def ISABELLE_TOOL} is
  set automatically to the absolute path name of the @{executable isabelle}
  executables.

  🚫
  Note that the settings environment may be inspected with the @{tool getenv}
  tool. This might help to figure out the effect of complex settings scripts.
›


subsection ‹Common variables›

text ‹
  This is a reference of common Isabelle settings variables. Note that the
  list is somewhat open-ended. Third-party utilities or interfaces may add
  their own selection. Variables that are special in some sense are marked
  with ‹🚫*›.

  🚫[@{setting_def USER_HOME}‹🚫*›] Is the cross-platform user home directory.
  On Unix systems this is usually the same as @{setting HOME}, but on Windows
  it is the regular home directory of the user, not the one of within the
  Cygwin root file-system.🚫‹Cygwin itself offers another choice whether its
  HOME should point to the 🍋‹/home› directory tree or the Windows user
  home.›

  🚫[@{setting_def ISABELLE_HOME}‹🚫*›] is the location of the top-level
  Isabelle distribution directory. This is automatically determined from the
  Isabelle executable that has been invoked. Do not attempt to set @{setting
  ISABELLE_HOME} yourself from the shell!

  🚫[@{setting_def ISABELLE_HOME_USER}] is the user-specific counterpart of
  @{setting ISABELLE_HOME}. The default value is relative to
  🍋‹$USER_HOME/.isabelle›, under rare circumstances this may be changed
  in the global setting file. Typically, the @{setting ISABELLE_HOME_USER}
  directory mimics @{setting ISABELLE_HOME} to some extend. In particular,
  site-wide defaults may be overridden by a private
  🍋‹$ISABELLE_HOME_USER/etc/settings›.

  🚫[@{setting_def ISABELLE_PLATFORM_FAMILY}‹🚫*›] is automatically set to the
  general platform family (🍋‹linux›, 🍋‹macos›, 🍋‹windows›). Note that
  platform-dependent tools usually need to refer to the more specific
  identification according to @{setting ISABELLE_PLATFORM64}, @{setting
  ISABELLE_WINDOWS_PLATFORM64}, @{setting ISABELLE_APPLE_PLATFORM64}.

  🚫[@{setting_def ISABELLE_PLATFORM64}‹🚫*›] indicates the standard Posix
  platform (🍋‹x86_64›, 🍋‹arm64›), together with a symbolic name for the
  operating system (🍋‹linux›, 🍋‹darwin›, 🍋‹cygwin›).

  🚫[@{setting_def ISABELLE_WINDOWS_PLATFORM64}‹🚫*›, @{setting_def
  ISABELLE_WINDOWS_PLATFORM32}‹🚫*›] indicate the native Windows platform: both
  64\,bit and 32\,bit executables are supported here.

  In GNU bash scripts, a preference for native Windows platform variants may
  be specified like this (first 64 bit, second 32 bit):

  @{verbatim [display] ‹"${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM32:-
  $ISABELLE_PLATFORM64}}"\}

  🚫[@{setting_def ISABELLE_APPLE_PLATFORM64}‹🚫*›] indicates the native Apple
  Silicon platform (🍋‹arm64-darwin› if available), instead of Intel emulation
  via Rosetta (🍋‹ISABELLE_PLATFORM64=x86_64-darwin›).

  🚫[@{setting ISABELLE_TOOL}‹🚫*›] is automatically set to the full path name
  of the @{executable isabelle} executable.

  🚫[@{setting_def ISABELLE_IDENTIFIER}‹🚫*›] refers to the name of this
  Isabelle distribution, e.g.\ ``🍋‹Isabelle2025-1›''.

  🚫[@{setting ML_OPTIONS}, @{setting ML_OPTIONS32}, @{setting ML_OPTIONS64}]
  provide command-line options to the underlying ML system of Isabelle.
  @{setting ML_OPTIONS} is empty by default, but if a proper value is provided
  (e.g.\ via user settings) that takes precedence. Otherwise, @{setting
  ML_OPTIONS32} or @{setting ML_OPTIONS64} will be used, depending on the
  system option @{system_option_ref ML_system_64}.

  🚫[@{setting_def ISABELLE_JDK_HOME}] points to a full JDK (Java Development
  Kit) installation with 🍋‹javac› and 🍋‹jar› executables. Note that
  conventional 🍋‹JAVA_HOME› points to the JRE (Java Runtime Environment), not
  the JDK.

  🚫[@{setting_def ISABELLE_JAVA_PLATFORM}] identifies the hardware and
  operating system platform for the Java installation of Isabelle. That is
  always the (native) 64 bit variant: 🍋‹x86_64-linux›, 🍋‹x86_64-darwin›,
  🍋‹x86_64-windows›.

  🚫[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where HTML and PDF
  browser information is stored (see also \secref{sec:info}); its default is
  🍋‹$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 🍋‹$ISABELLE_HOME/browser_info›.

  🚫[@{setting_def ISABELLE_HEAPS}] is the directory where session heap images,
  log files, and session build databases are stored; its default is
  🍋‹$ISABELLE_HOME_USER/heaps›. If @{system_option system_heaps} is
  🍋‹true›, @{setting_def ISABELLE_HEAPS_SYSTEM} is used instead; its default
  is 🍋‹$ISABELLE_HOME/heaps›. See also \secref{sec:tool-build}.

  🚫[@{setting_def ISABELLE_LOGIC}] specifies the default logic to load if none
  is given explicitly by the user. The default value is 🍋‹HOL›.

  🚫[@{setting_def ISABELLE_LINE_EDITOR}] specifies the line editor for the
  @{tool_ref console} interface.

  🚫[@{setting_def ISABELLE_PDFLATEX}, @{setting_def ISABELLE_LUALATEX},
  @{setting_def ISABELLE_BIBTEX}, @{setting_def ISABELLE_MAKEINDEX}] refer to
  {\LaTeX}-related tools for Isabelle document preparation (see also
  \secref{sec:tool-document}).

  🚫[@{setting_def ISABELLE_TOOLS}] is a colon separated list of directories
  that are scanned by @{executable isabelle} for external utility programs
  (see also \secref{sec:isabelle-tool}).

  🚫[@{setting_def ISABELLE_DOCS}] is a colon separated list of directories
  with documentation files.

  🚫[@{setting_def PDF_VIEWER}] specifies the program to be used for displaying
  🍋‹pdf› files.

  🚫[@{setting_def ISABELLE_TMP_PREFIX}‹🚫*›] is the prefix from which any
  running Isabelle ML process derives an individual directory for temporary
  files.

  🚫[@{setting_def ISABELLE_TOOL_JAVA_OPTIONS}] is passed to the 🍋‹java›
  executable when running Isabelle tools (e.g.\ @{tool build}). This is
  occasionally helpful to provide more heap space, via additional options like
  🍋‹-Xms1g -Xmx4g›.
›


subsection ‹Additional components \label{sec:components}›

text ‹
  Any directory may be registered as an explicit 🚫‹Isabelle component›. The
  general layout conventions are that of the main Isabelle distribution
  itself, and the following two files (both optional) have a special meaning:

    🚫 🍋‹etc/settings› holds additional settings that are initialized when
    bootstrapping the overall Isabelle environment, cf.\ \secref{sec:boot}. As
    usual, the content is interpreted as a GNU bash script. It may refer to
    the component's enclosing directory via the \<^verbatim>\COMPONENT\ shell variable.

    For example, the following setting allows to refer to files within the
    component later on, without having to hardwire absolute paths:
    @{verbatim [display] ‹MY_COMPONENT_HOME="$COMPONENT"›}

    Components can also add to existing Isabelle settings such as
    @{setting_def ISABELLE_TOOLS}, in order to provide component-specific
    tools that can be invoked by end-users. For example:
    @{verbatim [display] ‹ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"›}

    🚫 🍋‹etc/components› holds a list of further sub-components of the same
    structure. The directory specifications given here can be either absolute
    (with leading 🍋‹/›) or relative to the component's main directory.

  The root of component initialization is @{setting ISABELLE_HOME} itself.
  After initializing all of its sub-components recursively, @{setting
  ISABELLE_HOME_USER} is included in the same manner (if that directory
  exists). This allows to install private components via
  🍋‹$ISABELLE_HOME_USER/etc/components›, although it is often more
  convenient to do that programmatically via the
  🚫‹init_component› shell function in the 🍋‹etc/settings›
  script of 🍋‹$ISABELLE_HOME_USER› (or any other component directory). For
  example:
  @{verbatim [display] ‹init_component "$HOME/screwdriver-2.0"›}

  This is tolerant wrt.\ missing component directories, but might produce a
  warning.

  🚫
  More complex situations may be addressed by initializing components listed
  in a given catalog file, relatively to some base directory:
  @{verbatim [display] ‹init_components "$HOME/my_component_store" "some_catalog_file"›}

  The component directories listed in the catalog file are treated as relative
  to the given base directory.

  See also \secref{sec:tool-components} for some tool-support for resolving
  components that are formally initialized but not installed yet.
›


section ‹The Isabelle tool wrapper \label{sec:isabelle-tool}›

text ‹
  The main 🚫‹Isabelle tool wrapper› provides a generic startup environment for
  Isabelle-related utilities, user interfaces, add-on applications etc. Such
  tools automatically benefit from the settings mechanism
  (\secref{sec:settings}). Moreover, this is the standard way to invoke
  Isabelle/Scala functionality as a separate operating-system process.
  Isabelle command-line tools are run uniformly via a common wrapper ---
  @{executable_ref isabelle}:
  @{verbatim [display]
‹Usage: isabelle TOOL [ARGS ...]

  Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help.

Available tools:
  ...›}

  Tools may be implemented in Isabelle/Scala or as stand-alone executables
  (usually as GNU bash scripts). In the invocation of ``@{executable
  isabelle}~‹tool›'', the named ‹tool› is resolved as follows (and in the
  given order).

    🚫 An external tool found on the directories listed in the @{setting
    ISABELLE_TOOLS} settings variable (colon-separated list in standard POSIX
    notation). It is invoked as stand-alone program with the command-line
    arguments provided as 🍋‹argv› array.

    🚫 An internal tool that is declared via class
    🍋‹isabelle.Isabelle_Scala_Tools› and registered via
    🍋‹services› in 🍋‹etc/build.props›. See \secref{sec:scala-build} for
    more details.

  There are also various administrative tools that are available from a bare
  repository clone of Isabelle, but not in regular distributions.
›


subsubsection ‹Examples›

text ‹
  Show the list of available documentation of the Isabelle distribution:
  @{verbatim [display] ‹isabelle doc›}

  View a certain document as follows:
  @{verbatim [display] ‹isabelle doc system›}

  Query the Isabelle settings environment:
  @{verbatim [display] ‹isabelle getenv ISABELLE_HOME_USER›}
›


section ‹The raw ML process \label{sec:tool-ml-process}›

text ‹
  The raw ML process has limited use in actual applications: it lacks
  the full session context that is required for export artifacts,
  Isabelle/ML/Scala integration and Prover IDE messages or markup. It is
  better to use @{tool build} (\secref{sec:tool-build}) for regular sessions,
  or its front-end @{tool process_theories}
  (\secref{sec:tool-process-theories}) for adhoc sessions.
›


subsection ‹The raw ML process as command-line tool›

text ‹
  The @{tool_def ML_process} tool runs the raw ML process from the
  command-line:

  @{verbatim [display]
‹Usage: isabelle ML_process [OPTIONS]

  Options are:
    -C DIR       change working directory
    -d DIR       include session directory
    -e ML_EXPR   evaluate ML expression on startup
    -f ML_FILE   evaluate ML file on startup
    -l NAME      logic session name (default ISABELLE_LOGIC="HOL")
    -m MODE      add print mode for output
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    -r           redirect stderr to stdout

  Run the raw ML process without Isabelle/Scala context.›}

  Note that is often better to run the raw ML process directly from
  Isabelle/ML (via 🚫‹Isabelle_System.ML_process›) or Isabelle/Scala (via
  🍋‹isabelle.ML_Process›): both avoid another bulky Java
  process.

  🚫
  Options 🍋‹-e› and 🍋‹-f› allow to evaluate ML code, before the ML process is
  started. The source is either given literally or taken from a file. Multiple
  🍋‹-e› and 🍋‹-f› options are evaluated in the given order. Errors lead to
  a premature exit of the ML process with return code 1.

  🚫
  Option 🍋‹-l› specifies the logic session name. Option 🍋‹-d› specifies
  additional directories for session roots, see also \secref{sec:tool-build}.

  🚫
  The 🍋‹-m› option adds identifiers of print modes to be made active for this
  session. For example, 🍋‹-m ASCII› prefers ASCII replacement syntax over
  mathematical Isabelle symbols.

  🚫
  Option 🍋‹-o› allows to override Isabelle system options for this process,
  see also \secref{sec:system-options}.

  🚫
  Option 🍋‹-C› specifies an explicit working directory. Option 🍋‹-r› redirects
  🍋‹stderr› to 🍋‹stdout›.
›


subsubsection ‹Examples›

text ‹
  The subsequent example retrieves the 🍋‹Main› theory value from the theory
  loader within ML:
  @{verbatim [display] ‹isabelle ML_process -e 'Thy_Info.get_theory "Main"'›}

  Observe the delicate quoting rules for the GNU bash shell vs.\ ML. The
  Isabelle/ML and Scala libraries provide functions for that, but here we need
  to do it manually.

  🚫
  This is how to invoke a function body with proper return code and printing
  of errors, and without printing of a redundant 🍋‹val it = (): unit› result:
  @{verbatim [display] ‹isabelle ML_process -e 'Command_Line.tool (fn () => writeln "OK")'›}
  @{verbatim [display] ‹isabelle ML_process -e 'Command_Line.tool (fn () => error "Bad")'›}
›


subsection ‹Interactive mode›

text ‹
  The @{tool_def console} tool runs the raw ML process with interactive
  console and line editor:
  @{verbatim [display]
‹Usage: isabelle console [OPTIONS]

  Options are:
    -d DIR       include session directory
    -i NAME      include session in name-space of theories
    -l NAME      logic session name (default ISABELLE_LOGIC)
    -m MODE      add print mode for output
    -n           no build of session image on startup
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    -r           bootstrap from raw Poly/ML

  Build a logic session image and run the raw Isabelle ML process
  in interactive mode, with line editor ISABELLE_LINE_EDITOR.›}

  🚫
  Option 🍋‹-l› specifies the logic session name. By default, its heap image is
  checked and built on demand, but the option 🍋‹-n› skips that.

  Option 🍋‹-i› includes additional sessions into the name-space of theories:
  multiple occurrences are possible.

  Option 🍋‹-r› indicates a bootstrap from the raw Poly/ML system, which is
  relevant for Isabelle/Pure development.

  🚫
  Options 🍋‹-d›, 🍋‹-m›, 🍋‹-o› have the same meaning as for @{tool ML_process}
  (\secref{sec:tool-ml-process}).

  🚫
  The Isabelle/ML process is run through the line editor that is specified via
  the settings variable @{setting ISABELLE_LINE_EDITOR} (e.g.java.lang.NullPointerException
  @{executable_def rlwrap} for GNU readline); the fall-back is to use plain
  standard input/output.

  The user is connected to the raw ML toplevel loop: this is neither
  Isabelle/Isar nor Isabelle/ML within the usual formal context. The most
  relevant ML commands at this stage are ``🚫‹use "ROOT0.ML"›'' and
  ``🚫‹use "ROOT.ML"›'' to load the ML sources of Isabelle/Pure interactively.
›


section ‹The raw Isabelle Java process \label{sec:isabelle-java}›

text ‹
  The @{executable_ref isabelle_java} executable allows to run a Java process
  within the name space of Java and Scala components that are bundled with
  Isabelle, but 🚫‹without› the Isabelle settings environment
  (\secref{sec:settings}).

  After such a JVM cold-start, the Isabelle environment can be accessed via
  🍋‹Isabelle_System.getenv› as usual, but the underlying process environment
  remains clean. This is e.g.\ relevant when invoking other processes that
  should remain separate from the current Isabelle installation.

  🚫
  Note that under normal circumstances, Isabelle command-line tools are run
  🚫‹within› the settings environment, as provided by the @{executable
  isabelle} wrapper (\secref{sec:isabelle-tool} and \secref{sec:tool-java}).
›


subsubsection ‹Example›

text ‹
  The subsequent example creates a raw Java process on the command-line and
  invokes the main Isabelle application entry point:
  @{verbatim [display] ‹isabelle_java -Djava.awt.headless=false isabelle.jedit.JEdit_Main›}
›


section ‹System registry via TOML \label{sec:system-registry}›

text ‹
  Tools implemented in Isabelle/Scala may refer to a global registry of
  hierarchically structured values, which is based on a collection of TOML
  files. TOML is conceptually similar to JSON, but aims at human-readable
  syntax.

  The recursive structure of a TOML 🚫‹value› is defined as follows:
    🚫 atom: string, integer, float, bool, date (ISO-8601)
    🚫 array: sequence of 🚫‹values› ‹t›, written 🍋‹[›‹t🚫1›🍋‹,›‹…›🍋‹,›‹t🚫n›🍋‹]›
    🚫 table: mapping from 🚫‹names› ‹a› to 🚫‹values› ‹t›, written
      🍋‹{›‹a🚫1›🍋‹=›‹t🚫1›🍋‹,›‹…›🍋‹,›‹a🚫n›🍋‹=›‹t🚫n›🍋‹}›

  There are various alternative syntax forms for convenience, e.g. to
  construct a table of tables, using 🚫‹header syntax› that resembles
  traditional 🍋‹.INI›-file notation. For example:
  @{verbatim [display, indent = 2]
  ‹[point.A]
x = 1
y = 1
description = "one point"

[point.B]
x = 2
y = -2
description = "another point"

[point.C]
x = 3
y = 7
description = "yet another point"
›}

  Or alternatively like this:
  @{verbatim [display, indent = 2]
  ‹point.A.x = 1
point.A.y = 1
point.A.description = "one point"

point.B.x = 2
point.B.y = -2
point.B.description = "another point"

point.C.x = 3
point.C.y = 7
point.C.description = "yet another point"
›}

  The TOML website🚫‹🚫‹https://toml.io/en/v1.0.0›› provides many examples,
  together with the full language specification. Note that the Isabelle/Scala
  implementation of TOML uses the default ISO date/time format of
  Java.🚫‹🚫‹https://docs.oracle.com/en/java/javase/21/docs/api/java.base/java/time/format/DateTimeFormatter.html››

  🚫
  The overall system registry is collected from 🍋‹registry.toml› files in
  directories specified via the settings variable @{setting
  "ISABELLE_REGISTRY"}: this refers to 🍋‹$ISABELLE_HOME› and
  🍋‹$ISABELLE_HOME_USER› by default, but further directories may be
  specified via the GNU bash function 🚫‹isabelle_registry›
  within 🍋‹etc/settings› of Isabelle components.

  The result is available as Isabelle/Scala object
  🍋‹isabelle.Registry.global›. That is empty by default, unless users
  populate 🍋‹$ISABELLE_HOME_USER/etc/registry.toml› or provide other
  component 🍋‹etc/registry.toml› files.
›


section ‹YXML versus XML \label{sec:yxml-vs-xml}›

text ‹
  Isabelle tools often use YXML, which is a simple and efficient syntax for
  untyped XML trees. The YXML format is defined as follows.

    🚫 The encoding is always UTF-8.

    🚫 Body text is represented verbatim (no escaping, no special treatment of
    white space, no named entities, no CDATA chunks, no comments).

    🚫 Markup elements are represented via ASCII control characters ‹🚫X = 5›
    and ‹🚫Y = 6› as follows:

    \begin{tabular}{ll}
      XML & YXML \\\hline
      🍋‹<›‹name attribute›🍋‹=›‹value …›🍋‹>› &
      ‹🚫X🚫Yname🚫Yattribute›🍋‹=›‹value…🚫X› \\
      🍋‹</›‹name›🍋‹>› & ‹🚫X🚫Y🚫X› \\
    \end{tabular}

    There is no special case for empty body text, i.e.\ 🍋‹<foo/>› is treated
    like 🍋‹<foo></foo>›. Also note that ‹🚫X› and ‹🚫Y› may never occur in
    well-formed XML documents.

  Parsing YXML is pretty straight-forward: split the text into chunks
  separated by ‹🚫X›, then split each chunk into sub-chunks separated by ‹🚫Y›.
  Markup chunks start with an empty sub-chunk, and a second empty sub-chunk
  indicates close of an element. Any other non-empty chunk consists of plain
  text. For example, see 🍋‹~~/src/Pure/PIDE/yxml.ML› or
  🍋‹~~/src/Pure/PIDE/yxml.scala›.

  YXML documents may be detected quickly by checking that the first two
  characters are ‹🚫X🚫Y›.
›

end