Re: [isabelle] sledgehammer info



Hi Michael,

Am 05.09.2009 um 21:37 schrieb Michael Shulman:

Is there a way to get the sledgehammer to tell me exactly what input
and options it is passing to the external ATPs?

The options seem fixed in HOL/Tools/ATP_Manager/atp_wrapper.ML, e.g. for E:

--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int timeout

To get the exact problem that's generated, try adding the following lines at the beginning of your theory file (before invoking Sledgehammer):

ML {*
val _ = AtpWrapper.destdir := "/tmp"
val _ = AtpWrapper.problem_name := "sledgehammer"
*}

Whenever you run Sledgehammer, the generated files will be called "/ tmp/sledgehammer<x>_<y>", for different values of x and y, and they won't be deleted automatically after use.

Regards,

Jasmin






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.