--- a/Admin/components/components.sha1 Sun Nov 06 22:51:40 2016 +0100
+++ b/Admin/components/components.sha1 Mon Nov 07 14:55:39 2016 +0100
@@ -115,6 +115,7 @@
377e36efb8608e6c828c7718d890e97fde2006a4 linux_app-20131007.tar.gz
0aab4f73ff7f5e36f33276547e10897e1e56fb1d macos_app-20130716.tar.gz
ad5d0e640ce3609a885cecab645389a2204e03bb macos_app-20150916.tar.gz
+26df569cee9c2fd91b9ac06714afd43f3b37a1dd nunchaku-0.3.tar.gz
1c8cb6a8f4cbeaedce2d6d1ba8fc7e2ab3663aeb polyml-5.4.1.tar.gz
a3f9c159a0ee9a63b7a5d0c835ed9c2c908f8b56 polyml-5.5.0-1.tar.gz
7d604a99355efbfc1459d80db3279ffa7ade3e39 polyml-5.5.0-2.tar.gz
--- a/Admin/components/main Sun Nov 06 22:51:40 2016 +0100
+++ b/Admin/components/main Mon Nov 07 14:55:39 2016 +0100
@@ -9,6 +9,7 @@
jfreechart-1.0.14-1
jortho-1.0-2
kodkodi-1.5.2
+nunchaku-0.3
polyml-5.6-1
scala-2.11.8
ssh-java-20161009
--- a/src/HOL/Nunchaku/Nunchaku.thy Sun Nov 06 22:51:40 2016 +0100
+++ b/src/HOL/Nunchaku/Nunchaku.thy Mon Nov 07 14:55:39 2016 +0100
@@ -9,9 +9,9 @@
https://github.com/nunchaku-inria
-The "$NUNCHAKU" environment variable must be set to the absolute file name of
-the "nunchaku" executable. The Isabelle components for CVC4 and Kodkodi are
-necessary to use these backends.
+The "$NUNCHAKU_HOME" environment variable must be set to the absolute path to
+the directory containing the "nunchaku" executable. The Isabelle components
+for CVC4 and Kodkodi are necessary to use these backends.
*)
theory Nunchaku
--- a/src/HOL/Nunchaku/Tools/nunchaku.ML Sun Nov 06 22:51:40 2016 +0100
+++ b/src/HOL/Nunchaku/Tools/nunchaku.ML Mon Nov 07 14:55:39 2016 +0100
@@ -256,7 +256,7 @@
| Unknown (SOME (output, _)) => sat_or_maybe_sat false output
| Timeout => (print_n "Time out"; (unknownN, NONE))
| Nunchaku_Var_Not_Set =>
- (print_n ("Variable $" ^ nunchaku_env_var ^ " not set"); (unknownN, NONE))
+ (print_n ("Variable $" ^ nunchaku_home_env_var ^ " not set"); (unknownN, NONE))
| Nunchaku_Cannot_Execute =>
(print_n "External tool \"nunchaku\" cannot execute"; (unknownN, NONE))
| Nunchaku_Not_Found =>
--- a/src/HOL/Nunchaku/Tools/nunchaku_tool.ML Sun Nov 06 22:51:40 2016 +0100
+++ b/src/HOL/Nunchaku/Tools/nunchaku_tool.ML Mon Nov 07 14:55:39 2016 +0100
@@ -33,7 +33,7 @@
| CVC4_Not_Found
| Unknown_Error of int * string
- val nunchaku_env_var: string
+ val nunchaku_home_env_var: string
val solve_nun_problem: tool_params -> nun_problem -> nun_outcome
end;
@@ -71,7 +71,7 @@
((out, err), rc)
end;
-val nunchaku_env_var = "NUNCHAKU";
+val nunchaku_home_env_var = "NUNCHAKU_HOME";
val cached_outcome =
Synchronized.var "Nunchaku_Tool.cached_outcome" (NONE : (nun_problem * nun_outcome) option);
@@ -79,13 +79,13 @@
fun uncached_solve_nun_problem ({overlord, specialize, timeout, ...} : tool_params)
(problem as {sound, complete, ...}) =
with_tmp_or_overlord_file overlord "nunchaku" "nun" (fn prob_path =>
- if getenv nunchaku_env_var = "" then
+ if getenv nunchaku_home_env_var = "" then
Nunchaku_Var_Not_Set
else
let
val bash_cmd =
- "PATH=\"$CVC4_HOME:$KODKODI/bin:$PATH\" \"$" ^ nunchaku_env_var ^ "\" \
- \--skolems-in-model --no-color " ^
+ "PATH=\"$CVC4_HOME:$KODKODI/bin:$PATH\" \"$" ^
+ nunchaku_home_env_var ^ "\"/nunchaku --skolems-in-model --no-color " ^
(if specialize then "" else "--no-specialize ") ^
"--timeout " ^ string_of_int (Time.toSeconds timeout) ^ " " ^
File.bash_path prob_path;
@@ -99,10 +99,12 @@
(if sound then Sat else Unknown o SOME) (output, {tys = [], tms = []})
else if String.isPrefix "UNSAT" output then
if complete then Unsat else Unknown NONE
+ else if String.isSubstring "TIMEOUT" output
+ (* FIXME: temporary *)
+ orelse String.isSubstring "kodkod failed (errcode 152)" error then
+ Timeout
else if String.isPrefix "UNKNOWN" output then
Unknown NONE
- else if String.isPrefix "TIMEOUT" output then
- Timeout
else if code = 126 then
Nunchaku_Cannot_Execute
else if code = 127 then