61
|
1 |
theory ExternalSolver
|
|
2 |
imports "../Base"
|
|
3 |
begin
|
|
4 |
|
94
|
5 |
|
119
|
6 |
section {* Executing an External Application \label{rec:external}*}
|
61
|
7 |
|
|
8 |
text {*
|
|
9 |
{\bf Problem:}
|
94
|
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.
|
61
|
15 |
\smallskip
|
|
16 |
|
94
|
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 |
|
61
|
55 |
end |