"remote_e" and "remote_vampire" support TSTP proof output + fix "overlord" mode ATP output postprocessing
authorblanchet
Thu Apr 22 13:50:58 2010 +0200 (2010-04-22)
changeset 36286fa6d03d42aab
parent 36285 d868b34d604c
child 36287 96f45c5ffb36
"remote_e" and "remote_vampire" support TSTP proof output + fix "overlord" mode ATP output postprocessing
src/HOL/Tools/ATP_Manager/atp_wrapper.ML
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Thu Apr 22 10:54:56 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Thu Apr 22 13:50:58 2010 +0200
     1.3 @@ -119,8 +119,12 @@
     1.4           space_implode " " ["exec", File.shell_path cmd, args,
     1.5           File.shell_path probfile, "2>&1"]) ^
     1.6        (if overlord then
     1.7 -         " | sed 's/,/, /g' | sed 's/\\([=|]\\)/ \\1 /g' | sed 's/! =/ !=/g' \
     1.8 -         \| sed 's/  / /g'"
     1.9 +         " | sed 's/,/, /g' \
    1.10 +         \| sed 's/\\([^!=]\\)\\([=|]\\)\\([^=]\\)/\\1 \\2 \\3/g' \
    1.11 +         \| sed 's/! =/ !=/g' \
    1.12 +         \| sed 's/  / /g' | sed 's/| |/||/g' \
    1.13 +         \| sed 's/ = = =/===/g' \
    1.14 +         \| sed 's/= = /== /g'"
    1.15         else
    1.16           "")
    1.17      fun split_time s =
    1.18 @@ -335,7 +339,8 @@
    1.19      "Error: The remote ATP proof is ill-formed.")]
    1.20  
    1.21  fun remote_prover_config prover_prefix args
    1.22 -        ({known_failures, max_new_clauses, prefers_theory_relevant, ...}
    1.23 +        ({known_failures, max_new_clauses, prefers_theory_relevant,
    1.24 +          supports_isar_proofs, ...}
    1.25           : prover_config) : prover_config =
    1.26    {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP",
    1.27     arguments = (fn timeout =>
    1.28 @@ -344,7 +349,7 @@
    1.29     known_failures = remote_known_failures @ known_failures,
    1.30     max_new_clauses = max_new_clauses,
    1.31     prefers_theory_relevant = prefers_theory_relevant,
    1.32 -   supports_isar_proofs = false}
    1.33 +   supports_isar_proofs = supports_isar_proofs}
    1.34  
    1.35  val remote_vampire =
    1.36    tptp_prover "remote_vampire"