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
