Re: [isabelle] sledgehammer info



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

Please have a look at src/HOL/Tools/ATP_Manager/atp_wrapper.ML for the options
passed to the external ATPs, e.g. here:

  http://isabelle.in.tum.de/repos/isabelle/file/ea322e847633/src/HOL/Tools/ATP_Manager/atp_wrapper.ML

Look for functions named "<PROVER>_opts" or "<PROVER>_opts_full", where
<PROVER> may be instantiated with "vampire", "eprover", or "spass".

The input is usually kept in temporary files which are deleted after the
Sledgehammer call. You may, however, instruct sledgehammer to keep those files.
Copy the following line into your theory:

  ML {* AtpWrapper.destdir := "/foo/bar" *}

Any subsequent invocation of Sledgehammer during your Isabelle session will
store its problem files (and proof files) in directory "/foo/bar". Please make
sure this path exists.

Regards,
Sascha





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