None of them work. I did enable MaSh.
The new Isabelle pre-release does work. Larry On 12 Sep 2013, at 22:43, Jasmin Christian Blanchette <[email protected]> wrote: > Hi Larry, > > Am 12.09.2013 um 20:14 schrieb Lawrence Paulson <[email protected]>: > >> 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 [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
