Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] the sledgehammer 'debug' option

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>

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: Nov 21 2024 at 12:39 UTC