doc-src/System/Thy/document/Interfaces.tex
 author wenzelm Sat Apr 28 17:50:42 2012 +0200 (2012-04-28) changeset 47825 4f25960417ae parent 47824 65082431af2a child 47826 7c97bfe3a501 permissions -rw-r--r--
some coverage of Isabelle/Scala tools;
     1 %

     2 \begin{isabellebody}%

     3 \def\isabellecontext{Interfaces}%

     4 %

     5 \isadelimtheory

     6 %

     7 \endisadelimtheory

     8 %

     9 \isatagtheory

    10 \isacommand{theory}\isamarkupfalse%

    11 \ Interfaces\isanewline

    12 \isakeyword{imports}\ Base\isanewline

    13 \isakeyword{begin}%

    14 \endisatagtheory

    15 {\isafoldtheory}%

    16 %

    17 \isadelimtheory

    18 %

    19 \endisadelimtheory

    20 %

    21 \isamarkupchapter{User interfaces%

    22 }

    23 \isamarkuptrue%

    24 %

    25 \isamarkupsection{Plain TTY interaction \label{sec:tool-tty}%

    26 }

    27 \isamarkuptrue%

    28 %

    29 \begin{isamarkuptext}%

    30 The \indexdef{}{tool}{tty}\hypertarget{tool.tty}{\hyperlink{tool.tty}{\mbox{\isa{\isatt{tty}}}}} tool runs the Isabelle process interactively

    31   within a plain terminal session:

    32 \begin{ttbox}

    33 Usage: tty [OPTIONS]

    34

    35   Options are:

    36     -l NAME      logic image name (default ISABELLE_LOGIC)

    37     -m MODE      add print mode for output

    38     -p NAME      line editor program name (default ISABELLE_LINE_EDITOR)

    39

    40   Run Isabelle process with plain tty interaction, and optional line editor.

    41 \end{ttbox}

    42

    43   The \verb|-l| option specifies the logic image.  The

    44   \verb|-m| option specifies additional print modes.  The

    45   \verb|-p| option specifies an alternative line editor (such

    46   as the \indexdef{}{executable}{rlwrap}\hypertarget{executable.rlwrap}{\hyperlink{executable.rlwrap}{\mbox{\isa{\isatt{rlwrap}}}}} wrapper for GNU readline); the

    47   fall-back is to use raw standard input.

    48

    49   Regular interaction is via the standard Isabelle/Isar toplevel loop.

    50   The Isar command \hyperlink{command.exit}{\mbox{\isa{\isacommand{exit}}}} drops out into the raw ML system,

    51   which is occasionally useful for low-level debugging.  Invoking \verb|Isar.loop|~\verb|();| in ML will return to the Isar toplevel.%

    52 \end{isamarkuptext}%

    53 \isamarkuptrue%

    54 %

    55 \isamarkupsection{Proof General / Emacs%

    56 }

    57 \isamarkuptrue%

    58 %

    59 \begin{isamarkuptext}%

    60 The \indexdef{}{tool}{emacs}\hypertarget{tool.emacs}{\hyperlink{tool.emacs}{\mbox{\isa{\isatt{emacs}}}}} tool invokes a version of Emacs and Proof

    61   General within the regular Isabelle settings environment

    62   (\secref{sec:settings}).  This is more robust than starting Emacs

    63   separately, loading the Proof General lisp files, and then

    64   attempting to start Isabelle with dynamic \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}} lookup

    65   etc.

    66

    67   The actual interface script is part of the Proof General

    68   distribution~\cite{proofgeneral}; its usage depends on the

    69   particular version.  There are some options available, such as

    70   \verb|-l| for passing the logic image to be used by default,

    71   or \verb|-m| to tune the standard print mode.  The following

    72   Isabelle settings are particularly important for Proof General:

    73

    74   \begin{description}

    75

    76   \item[\indexdef{}{setting}{PROOFGENERAL\_HOME}\hypertarget{setting.PROOFGENERAL-HOME}{\hyperlink{setting.PROOFGENERAL-HOME}{\mbox{\isa{\isatt{PROOFGENERAL{\isaliteral{5F}{\isacharunderscore}}HOME}}}}}] points to the main

    77   installation directory of the Proof General distribution.  The

    78   default settings try to locate this in a number of standard places,

    79   notably \verb|\$ISABELLE_HOME/contrib/ProofGeneral|.

    80

    81   \item[\indexdef{}{setting}{PROOFGENERAL\_OPTIONS}\hypertarget{setting.PROOFGENERAL-OPTIONS}{\hyperlink{setting.PROOFGENERAL-OPTIONS}{\mbox{\isa{\isatt{PROOFGENERAL{\isaliteral{5F}{\isacharunderscore}}OPTIONS}}}}}] is implicitly prefixed to

    82   the command line of any invocation of the Proof General \verb|interface| script.

    83

    84   \item[\indexdef{}{setting}{XSYMBOL\_INSTALLFONTS}\hypertarget{setting.XSYMBOL-INSTALLFONTS}{\hyperlink{setting.XSYMBOL-INSTALLFONTS}{\mbox{\isa{\isatt{XSYMBOL{\isaliteral{5F}{\isacharunderscore}}INSTALLFONTS}}}}}] may contain a small shell

    85   script to install the X11 fonts required for the old X-Symbols mode

    86   of Proof General.  This is only relevant if the X11 display server

    87   runs on a different machine than the Emacs application, with a

    88   different file-system view on the Proof General installation.  Under

    89   most circumstances Proof General 3.x is able to refer to the font

    90   files that are part of its distribution, and Proof General 4.x finds

    91   its fonts by different means.

    92

    93   \end{description}%

    94 \end{isamarkuptext}%

    95 \isamarkuptrue%

    96 %

    97 \isamarkupsection{Isabelle/jEdit Prover IDE \label{sec:tool-jedit}%

    98 }

    99 \isamarkuptrue%

   100 %

   101 \begin{isamarkuptext}%

   102 The \indexdef{}{tool}{jedit}\hypertarget{tool.jedit}{\hyperlink{tool.jedit}{\mbox{\isa{\isatt{jedit}}}}} tool invokes a version of jEdit that has

   103   been augmented with some components to provide a fully-featured

   104   Prover IDE (based on Isabelle/Scala):

   105 \begin{ttbox}

   106 Usage: isabelle jedit [OPTIONS] [FILES ...]

   107

   108   Options are:

   109     -J OPTION    add JVM runtime option (default JEDIT_JAVA_OPTIONS)

   110     -b           build only

   111     -d           enable debugger

   112     -f           fresh build

   113     -j OPTION    add jEdit runtime option (default JEDIT_OPTIONS)

   114     -l NAME      logic image name (default ISABELLE_LOGIC)

   115     -m MODE      add print mode for output

   116

   117 Start jEdit with Isabelle plugin setup and opens theory FILES

   118 (default Scratch.thy).

   119 \end{ttbox}

   120

   121 The \verb|-J| and \verb|-j| options allow to pass

   122 additional low-level options to the JVM or jEdit, respectively.  The

   123 defaults are provided by the Isabelle settings environment.

   124

   125 The \verb|-d| option allows to connect to the runtime debugger

   126 of the JVM.  Note that the Scala Console of Isabelle/jEdit is more

   127 convenient in most practical situations.

   128

   129 The \verb|-b| and \verb|-f| options control the

   130 self-build mechanism of Isabelle/jEdit.  This is only relevant for

   131 building from sources, which also requires an auxiliary \verb|jedit_build| component.  Official Isabelle releases already include a

   132 version of Isabelle/jEdit that is built properly.

   133

   134 The \verb|-l| option specifies the logic image.  The

   135 \verb|-m| option specifies additional print modes.%

   136 \end{isamarkuptext}%

   137 \isamarkuptrue%

   138 %

   139 \isadelimtheory

   140 %

   141 \endisadelimtheory

   142 %

   143 \isatagtheory

   144 \isacommand{end}\isamarkupfalse%

   145 %

   146 \endisatagtheory

   147 {\isafoldtheory}%

   148 %

   149 \isadelimtheory

   150 %

   151 \endisadelimtheory

   152 \end{isabellebody}%

   153 %%% Local Variables:

   154 %%% mode: latex

   155 %%% TeX-master: "root"

   156 %%% End: