1 theory ExternalSolver

     2 imports "../Base"

     3 begin

     4 

     5 

     6 section {* Executing an External Application \label{rec:external}*}

     7 

     8 text {*

     9   {\bf Problem:}

    10   You want to use an external application.

    11   \smallskip

    12 

    13   {\bf Solution:} The function @{ML system_out} might be the right thing for

    14   you.

    15   \smallskip

    16 

    17   This function executes an external command as if printed in a shell. It

    18   returns the output of the program and its return value.

    19 

    20   For example, consider running an ordinary shell commands:

    21 

    22   @{ML_response [display,gray] 

    23     "system_out \"echo Hello world!\"" "(\"Hello world!\\n\", 0)"}

    24 

    25   Note that it works also fine with timeouts (see Recipe~\ref{rec:timeout}

    26   on Page~\pageref{rec:timeout}), i.e. external applications are killed

    27   properly. For example, the following expression takes only approximately

    28   one second:

    29 

    30   @{ML_response [display,gray] 

    31     "TimeLimit.timeLimit (Time.fromSeconds 1) system_out \"sleep 30\"

    32      handle TimeLimit.TimeOut => (\"timeout\", ~1)" "(\"timeout\", ~1)"}

    33 *}

    34 

    35 text {*

    36   The function @{ML system_out} can also be used for more reasonable

    37   applications, e.g. coupling external solvers with Isabelle. In that case,

    38   one has to make sure that Isabelle can find the particular executable.

    39   One way to ensure this is by adding a Bash-like variable binding into

    40   one of Isabelle's settings file (prefer the user settings file usually to

    41   be found at @{text "$HOME/.isabelle/etc/settings"}).

    42   

    43   For example, assume you want to use the application @{text foo} which

    44   is here supposed to be located at @{text "/usr/local/bin/"}.

    45   The following line has to be added to one of Isabelle's settings file:

    46 

    47   @{text "FOO=/usr/local/bin/foo"}

    48 

    49   In Isabelle, this application may now be executed by

    50 

    51   @{ML_response_fake [display,gray] "system_out \"$FOO\"" "\<dots>"}

    52 *}

    53 

    54 

    55 end