Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] sledgehammer info

view this post on Zulip Email Gateway (Aug 18 2022 at 14:01):

From: Michael Shulman <shulman@math.uchicago.edu>
Hi,

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

Thanks!
Mike

view this post on Zulip Email Gateway (Aug 18 2022 at 14:01):

From: Sascha Boehme <boehmes@in.tum.de>
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

view this post on Zulip Email Gateway (Aug 18 2022 at 14:01):

From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hi Michael,

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

view this post on Zulip Email Gateway (Aug 18 2022 at 14:01):

From: Makarius <makarius@sketis.net>
Note that in the official Isabelle2009 release the file is actually
src/HOL/Tools/atp_wrapper.ML which is also here in the repository
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2009/src/HOL/Tools/atp_wrapper.ML

Makarius

view this post on Zulip Email Gateway (Aug 18 2022 at 19:05):

From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Jesus,

In "sledgehammer.pdf", there's an option that's documented there, "overlord", that will do that and much more for you. I use it every day, hence the name! See the docs for details (p. 17):

http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2011-1/doc/sledgehammer.pdf

Regards,

Jasmin
(a.k.a. the overlord)

Last updated: Apr 18 2024 at 16:19 UTC