src/HOL/Library/Sum_of_Squares/sos_wrapper.ML
changeset 72278 199dc903131b
parent 71340 6d9dd5309b85
equal deleted inserted replaced
72277:48254fa33d88 72278:199dc903131b
    39         val _ = File.write in_path input
    39         val _ = File.write in_path input
    40 
    40 
    41         val (output, rc) =
    41         val (output, rc) =
    42           Isabelle_System.bash_output
    42           Isabelle_System.bash_output
    43             ("\"$ISABELLE_CSDP\" " ^
    43             ("\"$ISABELLE_CSDP\" " ^
    44               Bash.string (File.platform_path in_path) ^ " " ^
    44               File.bash_platform_path in_path ^ " " ^
    45               Bash.string (File.platform_path out_path));
    45               File.bash_platform_path out_path);
    46         val _ = Sum_of_Squares.debug_message ctxt (fn () => "Solver output:\n" ^ output)
    46         val _ = Sum_of_Squares.debug_message ctxt (fn () => "Solver output:\n" ^ output)
    47 
    47 
    48         val result = if File.exists out_path then File.read out_path else ""
    48         val result = if File.exists out_path then File.read out_path else ""
    49 
    49 
    50         val (res, res_msg) = get_result rc
    50         val (res, res_msg) = get_result rc