Stream: Beginner Questions

Topic: Sledgehammer Windows Issues

view this post on Zulip Jason Veenendaal (Sep 05 2024 at 20:41):

I'm taking a course on Isabelle and I'm having trouble with sledgehammer. Sledgehammer is having difficulty finding proofs when other people in my class are having no problems. I'm unfolding definitions and proving lemmas and still running into problems. I'm using windows 11 and have 8gb of RAM.

view this post on Zulip Craig Alan Feinstein (Sep 06 2024 at 01:12):

I’ve ran sledgehammer multiple times on the same statement with different results.

view this post on Zulip Mathias Fleury (Sep 06 2024 at 04:51):

  1. Sledgehammer is not deterministic at various levels: fact selection [the default depends on what you learned before and variable names can change what SMT solver do], run-time of the solver [the more programs run, the slower the solver get], replaying on the Isabelle side [Isabelle issue]

view this post on Zulip Mathias Fleury (Sep 06 2024 at 04:52):

  1. 8GB is not a lot when you run Isabelle and some solvers (if some memory is offloaded to disk… big problem)

view this post on Zulip Mathias Fleury (Sep 06 2024 at 04:54):

I would limit the number of run solvers to 2 or 3 (for 3: cvc, z3 or vampire, e; for 2: cvc and e)

view this post on Zulip Mathias Fleury (Sep 06 2024 at 04:54):

In the sledgehammer panel, next to the run sledgehammer button, there is a string list you can edit to change the used solvers

view this post on Zulip Jason Veenendaal (Sep 06 2024 at 13:45):

I've tried changing the number of solvers and I still am having trouble. I've also tried to limit the number of slices as well but I'm not sure if that should help or not.

Last updated: Dec 21 2024 at 16:20 UTC