equal
deleted
inserted
replaced
55 |> lines_of_atp_problem format (K []) |
55 |> lines_of_atp_problem format (K []) |
56 |> File.write_list prob_file |
56 |> File.write_list prob_file |
57 val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec) |
57 val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec) |
58 val command = |
58 val command = |
59 space_implode " " (File.bash_path (Path.explode path) :: |
59 space_implode " " (File.bash_path (Path.explode path) :: |
60 arguments ctxt false "" atp_timeout prob_file) |
60 arguments false false "" atp_timeout prob_file) |
61 val outcome = |
61 val outcome = |
62 Timeout.apply atp_timeout Isabelle_System.bash_output command |
62 Timeout.apply atp_timeout Isabelle_System.bash_output command |
63 |> fst |
63 |> fst |
64 |> extract_tstplike_proof_and_outcome false proof_delims known_failures |
64 |> extract_tstplike_proof_and_outcome false proof_delims known_failures |
65 |> snd |
65 |> snd |