disable SPASS's splitting if Isar proofs are desired, because these are not handled by the proof reconstruction code (and it's not clear how to handle them considering the lack of documentation)
authorblanchet
Sun May 26 14:02:03 2013 +0200 (2013-05-26)
changeset 52151de43876e77bf
parent 52150 41c885784e04
child 52152 b561cdce6c4c
child 52154 b707a26d8fe0
disable SPASS's splitting if Isar proofs are desired, because these are not handled by the proof reconstruction code (and it's not clear how to handle them considering the lack of documentation)
src/HOL/Tools/ATP/atp_systems.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Sun May 26 12:56:37 2013 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Sun May 26 14:02:03 2013 +0200
     1.3 @@ -521,11 +521,11 @@
     1.4  (* FIXME: Make "SPASS_NEW_HOME" legacy. *)
     1.5  val spass_config : atp_config =
     1.6    {exec = (["SPASS_NEW_HOME", "SPASS_HOME"], ["SPASS"]),
     1.7 -   arguments =
     1.8 -     fn _ => fn _ => fn extra_options => fn timeout => fn file_name => fn _ =>
     1.9 -         "-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^
    1.10 -         file_name
    1.11 -         |> extra_options <> "" ? prefix (extra_options ^ " "),
    1.12 +   arguments = fn _ => fn full_proofs => fn extra_options => fn timeout =>
    1.13 +       fn file_name => fn _ =>
    1.14 +       "-Isabelle=1 " ^ (if full_proofs then "-Splits=0 " else "") ^
    1.15 +       "-TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name
    1.16 +       |> extra_options <> "" ? prefix (extra_options ^ " "),
    1.17     proof_delims = [("Here is a proof", "Formulae used in the proof")],
    1.18     known_failures =
    1.19       [(OldSPASS, "Unrecognized option Isabelle"),
    1.20 @@ -711,12 +711,12 @@
    1.21  fun remote_config system_name system_versions proof_delims known_failures
    1.22                    prem_role best_slice : atp_config =
    1.23    {exec = (["ISABELLE_ATP"], ["scripts/remote_atp"]),
    1.24 -   arguments =
    1.25 -     fn _ => fn _ => fn command => fn timeout => fn file_name => fn _ =>
    1.26 -         (if command <> "" then "-c " ^ quote command ^ " " else "") ^
    1.27 -         "-s " ^ the_remote_system system_name system_versions ^ " " ^
    1.28 -         "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^
    1.29 -         " " ^ file_name,
    1.30 +   arguments = fn _ => fn _ => fn command => fn timeout => fn file_name =>
    1.31 +       fn _ =>
    1.32 +       (if command <> "" then "-c " ^ quote command ^ " " else "") ^
    1.33 +       "-s " ^ the_remote_system system_name system_versions ^ " " ^
    1.34 +       "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^
    1.35 +       " " ^ file_name,
    1.36     proof_delims = union (op =) tstp_proof_delims proof_delims,
    1.37     known_failures = known_failures @ known_perl_failures @ known_says_failures,
    1.38     prem_role = prem_role,