theory ExternalSolver+
−
imports "../Appendix"+
−
begin+
−
+
−
+
−
section \<open>Executing an External Application (TBD) \label{rec:external}\<close>+
−
+
−
text \<open>+
−
  {\bf Problem:}+
−
  You want to use an external application.+
−
  \smallskip+
−
+
−
  {\bf Solution:} The function @{ML bash_output in Isabelle_System} 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_matchresult [display,gray] +
−
    \<open>Isabelle_System.bash_output "echo Hello world!"\<close> \<open>("Hello world!\n", 0)\<close>}+
−
+
−
  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_matchresult_fake [display,gray] +
−
    \<open>Timeout.apply (Time.fromSeconds 1) Isabelle_System.bash_output "sleep 30"+
−
     handle TIMEOUT => ("timeout", ~1)\<close> \<open>("timeout", ~1)\<close>}+
−
+
−
  The function @{ML bash_output in Isabelle_System} 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 \<open>$HOME/.isabelle/etc/settings\<close>).+
−
  +
−
  For example, assume you want to use the application \<open>foo\<close> which+
−
  is here supposed to be located at \<open>/usr/local/bin/\<close>.+
−
  The following line has to be added to one of Isabelle's settings file:+
−
+
−
  \<open>FOO=/usr/local/bin/foo\<close>+
−
+
−
  In Isabelle, this application may now be executed by+
−
+
−
  @{ML_matchresult_fake [display,gray] \<open>Isabelle_System.bash_output "$FOO"\<close> \<open>\<dots>\<close>}+
−
\<close>+
−
+
−
+
−
end+
−