Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] the sledgehammer 'debug' option

view this post on Zulip Email Gateway (Aug 22 2022 at 18:59):

From: noam neer <noamneer@gmail.com>
hi everybody.
the following questions are about sledgehammer in Isabelle/jEdit 2018 on
windows 10.

  1. I tried to prove some lemma with sledgehammer. when I tries
    lemma "..."
    by sledgehammer [timeout=600]
    the provers indeed ran for 10 about minutes. but when I tried
    lemma "..."
    by sledgehammer [debug, timeout=600]
    everything ended in a few seconds. it didn't even run for the default 60
    seconds.
    why?

  2. when I used the debug option I got in the output window something like
    "mesh": Including 1000 relevant facts: ... a 1000 names ...
    "mepo": Including 1000 relevant facts: ...
    "mash": Including 1000 relevant facts: ...
    but then I got
    "e" slice #1 with 133 facts for 90.0 s...
    and similarly for the other default provers. if I understand this
    correctly, it means that from the
    1000 facts only a fraction (133) was actually used. so, how do I know which
    ones were actually used?

  3. is there a way to get not just a list of facts, but the precise input
    fed to the provers?

thanx

<https://www.avast.com/sig-email?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=webmail&utm_term=icon>
Virus-free.
www.avast.com
<https://www.avast.com/sig-email?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=webmail&utm_term=link>
<#DAB4FAD8-2DD7-40BB-A1B8-4E2AA1F9FDF2>

view this post on Zulip Email Gateway (Aug 22 2022 at 19:00):

From: noam neer <noamneer@gmail.com>
here are three versions of the problem (together with the corresponding
output.)
version a : with [timeout=60], works.
version b : with [timeout=60, debug], doesn't work.
version c : with [timeout=60, debug, fact_filter=mepo], doesn't work.

BTW, another strange thing is that in these calls SPASS does not run.
on the other hand if I apply sledgehammer through the sledgehammer panel
instead of a text command, SPASS does run.

<https://www.avast.com/sig-email?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=webmail&utm_term=icon>
Virus-free.
www.avast.com
<https://www.avast.com/sig-email?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=webmail&utm_term=link>
<#DAB4FAD8-2DD7-40BB-A1B8-4E2AA1F9FDF2>
query_19_01_30a_out.txt
query_19_01_30c.thy
query_19_01_30b.thy
query_19_01_30a.thy
query_19_01_30b_out.txt
query_19_01_30c_out.txt

Last updated: Apr 26 2024 at 04:17 UTC