Re: [isabelle-dev] Total failure of sledgehammer
Hi Larry, Am 13.09.2013 um 21:17 schrieb Lawrence Paulson l...@cam.ac.uk: That fixed it. One of the Australians has run into the same issue with MaSh. The issue should be addressed starting with Isabelle/8d9f4e89d8c8. If you're willing to give MaSh a second try, you could try to set MASH=yes again. To be sure that no stale data or zombies lie around, I would recommend running the following commands: pkill -f ython.*server.py rm -fr ~/.isabelle/mash/ Thank you for the report sorry for the invconvenience! Regards, Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Total failure of sledgehammer
Am 13.09.2013 um 09:34 schrieb Lawrence Paulson l...@cam.ac.uk: None of them work. Can you reproduce it in Proof General? As an additional test, you could try playing with options like debug and see if the output says anything interesting. Just to make sure it's not MaSh-related somehow, I would also recommend you comment out MASH=yes in your settings file and see if this has any impact. Another useful data point would be to know if you can run the HOL-Metis_Examples session. The file Proxies.thy contains some Sledgehammer regression tests that rely on SPASS. Otherwise I'm running out of ideas. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Total failure of sledgehammer
That fixed it. Larry On 13 Sep 2013, at 10:15, Jasmin Blanchette jasmin.blanche...@gmail.com wrote: Just to make sure it's not MaSh-related somehow, I would also recommend you comment out MASH=yes in your settings file and see if this has any impact. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Total failure of sledgehammer
Hi Larry, Am 12.09.2013 um 20:14 schrieb Lawrence Paulson l...@cam.ac.uk: Provers don't launch at all (according to process monitor) and no output, either in the new S/H panel or via the sledgehammer command. I'm using 9d8764624487 but I don't think the precise version matters, as I grabbed a new copy this morning and nothing's changed. Anybody else seen this? I'm using the slightly more recent 3fb81ab13ea3 (but as you pointed out, hardly anything has changed in between) and everything is OK here. Let's try to debug this systematically. 1. First, can you confirm that this total failure of Sledgehammer also occurs in the following example (which should be solved quasi instantly by several ATPs)? theory Scratch imports Main begin lemma hd [x] = x sledgehammer (hd.simps) 2. If step 1 works, please try sledgehammer [mepo] instead. 3. If step 2 works, please try sledgehammer without any options. 4. If step 3 works, try to construct a minimal self-contained example that doesn't work and send it to me. One of my suspicions is that you might have enabled MaSh and today's change to it might have broken things somehow. Another We'll definitely need to be more conservative in our changes getting closer to the release. Thanks for your help. Cheers, Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Total failure of sledgehammer
Provers don't launch at all (according to process monitor) and no output, either in the new S/H panel or via the sledgehammer command. I'm using 9d8764624487 but I don't think the precise version matters, as I grabbed a new copy this morning and nothing's changed. Anybody else seen this? Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
