# HG changeset patch # User sultana # Date 1334675647 -3600 # Node ID b2f209258621e762314ddc41bffe4abc61d1cb6a # Parent 6bc4c66d8c1ba4f867ea3998991d6f83d3a58f25 more cleaning of tptp tests; diff -r 6bc4c66d8c1b -r b2f209258621 src/HOL/TPTP/TPTP_Interpret_Test.thy --- a/src/HOL/TPTP/TPTP_Interpret_Test.thy Tue Apr 17 16:14:07 2012 +0100 +++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy Tue Apr 17 16:14:07 2012 +0100 @@ -11,7 +11,7 @@ begin section "Interpreter tests" -(* + text "Interpret a problem." ML {* val (time, ((type_map, const_map, fmlas), thy)) = @@ -27,19 +27,18 @@ text "... and display nicely." ML {* - List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #4) fmlas -*} -ML {* + List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #4) fmlas; + (*Don't use TPTP_Syntax.string_of_tptp_formula, it's just for testing*) List.app (writeln o TPTP_Syntax.string_of_tptp_formula o #3) fmlas *} -*) subsection "Multiple tests" ML {* + (*default timeout is 1 min*) fun interpret timeout file thy = - TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 600 else timeout)) + TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 60 else timeout)) (TPTP_Interpret.interpret_file false (Path.dir tptp_probs_dir) @@ -50,18 +49,9 @@ fun interpret_timed timeout file thy = Timing.timing (interpret timeout file) thy - (*default timeout is 10 mins*) fun interpretation_test timeout ctxt = test_fn ctxt - (fn file => (*FIXME use "interpret" function above*) - TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 600 else timeout)) - (TPTP_Interpret.interpret_file - false - (Path.dir tptp_probs_dir) - file - [] - []) - @{theory}(*FIXME*)) + (fn file => interpret timeout file (Proof_Context.theory_of ctxt)) "interpreter" () @@ -128,19 +118,20 @@ *} ML {* - interpretation_tests 5 @{context} + interpretation_tests (get_timeout @{context}) @{context} (some_probs @ take_too_long @ timeouts @ more_probs) *} -declare [[warning_out = ""]] subsection "Test against whole TPTP" text "Run interpretation over all problems. This works only for logics for which interpretation is defined (in TPTP_Parser/tptp_interpret.ML)." ML {* - report @{context} "Interpreting all problems."; - (*val _ = S timed_test (interpretation_test 5) @{context}*) + if test_all @{context} then + (report @{context} "Interpreting all problems"; + S timed_test (interpretation_test (get_timeout @{context})) @{context}) + else () *} -end +end \ No newline at end of file diff -r 6bc4c66d8c1b -r b2f209258621 src/HOL/TPTP/TPTP_Parser_Example.thy --- a/src/HOL/TPTP/TPTP_Parser_Example.thy Tue Apr 17 16:14:07 2012 +0100 +++ b/src/HOL/TPTP/TPTP_Parser_Example.thy Tue Apr 17 16:14:07 2012 +0100 @@ -5,7 +5,7 @@ *) theory TPTP_Parser_Example -imports TPTP_Parser +imports TPTP_Parser TPTP_Interpret uses "~~/src/HOL/ex/sledgehammer_tactics.ML" begin diff -r 6bc4c66d8c1b -r b2f209258621 src/HOL/TPTP/TPTP_Parser_Test.thy --- a/src/HOL/TPTP/TPTP_Parser_Test.thy Tue Apr 17 16:14:07 2012 +0100 +++ b/src/HOL/TPTP/TPTP_Parser_Test.thy Tue Apr 17 16:14:07 2012 +0100 @@ -7,7 +7,7 @@ *) theory TPTP_Parser_Test -imports TPTP_Test (*TPTP_Parser_Example*) +imports TPTP_Test TPTP_Parser_Example begin section "Parser tests" @@ -73,10 +73,11 @@ *} text "Run the parser over all problems." -ML {*report @{context} "Testing parser"*} ML {* -(* val _ = S timed_test parser_test @{context}*) + if test_all @{context} then + (report @{context} "Testing parser"; + S timed_test parser_test @{context}) + else () *} - end \ No newline at end of file diff -r 6bc4c66d8c1b -r b2f209258621 src/HOL/TPTP/TPTP_Test.thy --- a/src/HOL/TPTP/TPTP_Test.thy Tue Apr 17 16:14:07 2012 +0100 +++ b/src/HOL/TPTP/TPTP_Test.thy Tue Apr 17 16:14:07 2012 +0100 @@ -1,9 +1,9 @@ (* Title: HOL/TPTP/TPTP_Test.thy -5A Author: Nik Sultana, Cambridge University Computer Laboratory + Author: Nik Sultana, Cambridge University Computer Laboratory -Some tests for the TPTP interface. Some of the tests rely on the Isabelle -environment variable TPTP_PROBLEMS_PATH, which should point to the -TPTP-vX.Y.Z/Problems directory. +Some test support for the TPTP interface. Some of the tests rely on +the Isabelle environment variable TPTP_PROBLEMS_PATH, which should +point to the TPTP-vX.Y.Z/Problems directory. *) theory TPTP_Test @@ -11,7 +11,12 @@ begin ML {* - val warning_out = Attrib.setup_config_string @{binding "warning_out"} (K "") + val tptp_test_out = Attrib.setup_config_string @{binding "tptp_test_out"} (K "") + val tptp_test_all = Attrib.setup_config_bool @{binding "tptp_test_all"} (K false) + val tptp_test_timeout = + Attrib.setup_config_int @{binding "tptp_test_timeout"} (K 5) + fun test_all ctxt = Config.get ctxt tptp_test_all + fun get_timeout ctxt = Config.get ctxt tptp_test_timeout fun S x y z = x z (y z) *} @@ -47,12 +52,12 @@ ML {* fun report ctxt str = let - val warning_out = Config.get ctxt warning_out + val tptp_test_out = Config.get ctxt tptp_test_out in - if warning_out = "" then warning str + if tptp_test_out = "" then warning str else let - val out_stream = TextIO.openAppend warning_out + val out_stream = TextIO.openAppend tptp_test_out in (TextIO.output (out_stream, str ^ "\n"); TextIO.flushOut out_stream; TextIO.closeOut out_stream) @@ -108,6 +113,4 @@ () *} -declare [[warning_out = ""]] - end \ No newline at end of file