theory ExternalSolver+ −
imports "../Base"+ −
begin+ −
+ −
+ −
section {* Executing an External Application \label{rec:external}*}+ −
+ −
text {*+ −
{\bf Problem:}+ −
You want to use an external application.+ −
\smallskip+ −
+ −
{\bf Solution:} The function @{ML system_out} might be the right thing for+ −
you.+ −
\smallskip+ −
+ −
This function executes an external command as if printed in a shell. It+ −
returns the output of the program and its return value.+ −
+ −
For example, consider running an ordinary shell commands:+ −
+ −
@{ML_response [display,gray] + −
"system_out \"echo Hello world!\"" "(\"Hello world!\\n\", 0)"}+ −
+ −
Note that it works also fine with timeouts (see Recipe~\ref{rec:timeout}+ −
on Page~\pageref{rec:timeout}), i.e. external applications are killed+ −
properly. For example, the following expression takes only approximately+ −
one second:+ −
+ −
@{ML_response [display,gray] + −
"TimeLimit.timeLimit (Time.fromSeconds 1) system_out \"sleep 30\"+ −
handle TimeLimit.TimeOut => (\"timeout\", ~1)" "(\"timeout\", ~1)"}+ −
*}+ −
+ −
text {*+ −
The function @{ML system_out} can also be used for more reasonable+ −
applications, e.g. coupling external solvers with Isabelle. In that case,+ −
one has to make sure that Isabelle can find the particular executable.+ −
One way to ensure this is by adding a Bash-like variable binding into+ −
one of Isabelle's settings file (prefer the user settings file usually to+ −
be found at @{text "$HOME/.isabelle/etc/settings"}).+ −
+ −
For example, assume you want to use the application @{text foo} which+ −
is here supposed to be located at @{text "/usr/local/bin/"}.+ −
The following line has to be added to one of Isabelle's settings file:+ −
+ −
@{text "FOO=/usr/local/bin/foo"}+ −
+ −
In Isabelle, this application may now be executed by+ −
+ −
@{ML_response_fake [display,gray] "system_out \"$FOO\"" "\<dots>"}+ −
*}+ −
+ −
+ −
end+ −