--- a/CookBook/Recipes/ExternalSolver.thy Wed Mar 18 23:52:51 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,55 +0,0 @@
-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
\ No newline at end of file