How to change the timeout for sledgehammer?

[haoxiongliu]

Hello,

Thanks for sharing the code!

I find that the default timeout of sledgehammer seems to be around 30~35s rather than the 120s reported in the paper, since I get exceptions like

Exception while trying to run sledgehammer: Timeout after 35.848s
Action: normalhammer
IsabelleException: Outer syntax error (line 1): command expected,
but identifier Timeout (line 1) was found
At command "<malformed>" (line 1)

When looking into the PISA source code, I find the following code snippet in src/main/scala/pisa/agent/RepHammer.scala

val normal_with_Sledgehammer: MLFunction4[ToplevelState, Theory, List[String], List[String], (Boolean, (String, List[String]))] =
  compileFunction[ToplevelState, Theory, List[String], List[String], (Boolean, (String, List[String]))](
    s""" fn (state, thy, adds, dels) =>
       |    let
       |       val override = {add=[],del=[],only=false};
       |       fun go_run (state, thy) =
       |          let
       |             val p_state = Toplevel.proof_of state;
       |             val ctxt = Proof.context_of p_state;
       |             val params = ${Sledgehammer_Commands}.default_params thy
       |                [("provers", "e"),("timeout","30"),("verbose","true")];
       |             val results = ${Sledgehammer}.run_sledgehammer params ${Sledgehammer_Prover}.Normal NONE 1 override p_state;
       |             val (result, (outcome, step)) = results;
       |           in
       |             (result, (${Sledgehammer}.short_string_of_sledgehammer_outcome outcome, [YXML.content_of step]))
       |           end;
       |    in
       |      Timeout.apply (Time.fromSeconds 35) go_run (state, thy) end
       |""".stripMargin
  )

Does changing the "Time.fromSeconds 35" to "Time.fromSeconds 120" the right way to do it? I'm not familiar with Scala.

Thanks for your attention. Looking forward to your reply!

[albertqjiang]

That's indeed the right way. You need to rebuild the PISA library after the change though, for the changes to be reflected.

[haoxiongliu]

Thank you for the quick reply!