Commit 5b56aa0b authored by wenzelm's avatar wenzelm

merged

......@@ -46,14 +46,15 @@ fun compile_ml_file mode source =
val bash_cake = File.bash_path (compiler ())
val bash_source = File.bash_path source
val {out, err, rc, ...} =
Isabelle_System.bash_process (bash_cake ^ " --sexp=" ^ sexp ^ " < " ^ bash_source)
val res = Isabelle_System.bash_process (bash_cake ^ " --sexp=" ^ sexp ^ " < " ^ bash_source)
val err = Process_Result.err res
val out = Process_Result.out res
val _ = if err <> "" then warning err else ()
in
if rc <> 0 orelse err <> "" then
if not (Process_Result.ok res) orelse err <> "" then
error "CakeML: ML compilation failed"
else
(File.write output (trim_line out); output)
(File.write output out; output)
end
fun compile_ml mode source =
......@@ -71,12 +72,13 @@ fun compile_c_file source =
val bash_cc = File.bash_path (Path.explode (getenv_strict "ISABELLE_CC"))
val bash_source = File.bash_path source
val bash_output = File.bash_path output
val {out, err, rc, ...} =
Isabelle_System.bash_process (bash_cc ^ " -c -o " ^ bash_output ^ " " ^ bash_source)
val res = Isabelle_System.bash_process (bash_cc ^ " -c -o " ^ bash_output ^ " " ^ bash_source)
val err = Process_Result.err res
val out = Process_Result.out res
val _ = if err <> "" then warning err else ()
val _ = writeln out
in
if rc <> 0 orelse err <> "" then
if not (Process_Result.ok res) orelse err <> "" then
error "CakeML: C compilation failed"
else
output
......@@ -93,12 +95,13 @@ fun link sources =
val bash_cc = File.bash_path (Path.explode (getenv_strict "ISABELLE_CC"))
val bash_sources = Bash.strings (map File.standard_path sources)
val bash_output = File.bash_path output
val {out, err, rc, ...} =
Isabelle_System.bash_process (bash_cc ^ " -o " ^ bash_output ^ " " ^ bash_sources)
val res = Isabelle_System.bash_process (bash_cc ^ " -o " ^ bash_output ^ " " ^ bash_sources)
val err = Process_Result.err res
val out = Process_Result.out res
val _ = if err <> "" then warning err else ()
val _ = writeln out
in
if rc <> 0 orelse err <> "" then
if not (Process_Result.ok res) orelse err <> "" then
error "CakeML: linking failed"
else
output
......@@ -109,13 +112,15 @@ fun eval mode source =
val cake = compile_ml mode source
val ffi = compile_ffi ()
val bin = link [cake, ffi]
val {out, err, rc, ...} = Isabelle_System.bash_process (File.bash_path bin)
val res = Isabelle_System.bash_process (File.bash_path bin)
val err = Process_Result.err res
val out = Process_Result.out res
val _ = if err <> "" then warning err else ()
in
if rc <> 0 orelse err <> "" then
if not (Process_Result.ok res) orelse err <> "" then
error "CakeML: evaluation failed"
else
trim_line out
out
end
fun eval_source mode =
......
......@@ -643,10 +643,11 @@ structure Export_code_env = struct
end
fun compile l cmd =
let val (l, rc) = fold (fn cmd => (fn (l, 0) =>
let val {out, err, rc, ...} = Isabelle_System.bash_process cmd in
((out, err) :: l, rc) end
| x => x)) l ([], 0)
let val (l, rc) = fold (fn cmd =>
(fn (l, 0) =>
let val res = Isabelle_System.bash_process cmd in
((Process_Result.out res, Process_Result.err res) :: l, Process_Result.rc res) end
| x => x)) l ([], 0)
val l = rev l in
if rc = 0 then
(l, Isabelle_System.bash_output cmd)
......
......@@ -358,11 +358,11 @@ fun solve_program prog =
val esolver_path = getenv "QSOPT_EXACT_PATH"
val esolver = if esolver_path = "" then "esolver" else esolver_path
val command = wrap esolver ^ " -O " ^ wrap resultname ^ " " ^ wrap lpname
val {err, rc, ...} = Isabelle_System.bash_process command
val res = Isabelle_System.bash_process command
in
if rc <> 0 then
if not (Process_Result.ok res) then
raise Fail ("QSopt_exact returned with an error (return code " ^
Int.toString rc ^ "):\n" ^ err)
Int.toString (Process_Result.rc res) ^ "):\n" ^ Process_Result.err res)
else
let
val result = read_result_file resultname
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment