Re: [isabelle] Sledgehammer on Windows



Hi all,

Le 08/05/2015 00:44, Alfio Martini a Ãcrit :
> Hi Jasmin,
>
>> Thatâs really bad â that lemma is supposed to be ultra easy. In a previous
> email, I suggested > you try disabling MaSh. Did that make any change?
>
> I certainly missed that remark. I have no idea what is MaSh. How can  I
> disable it?
> There is something about it in Isabelle Plugin Options.
>
> Best!
Put none in the options (documentation panel > sledgehammer manual, Â7.2).

> On Thu, May 7, 2015 at 7:31 PM, Jasmin Blanchette <
> jasmin.blanchette at inria.fr> wrote:
>
>> Dear Alfio,
>>
>>> - Isabelle for Windows: Using the standard configuration,  s/h
>>>   solves the first lemma only with e (and it takes quite some time
>>>   to do it).
>> Thatâs really bad â that lemma is supposed to be ultra easy. In a previous
>> email, I suggested you try disabling MaSh. Did that make any change?
>>
>> Otherwise, thanks to my colleague Mathias Fleury, we should be able to
>> include CVC4 executables with proof output in RC4 and/or the final
>> Isabelle2015 release. We will look into this in the next 24 hours.
>> Makarius, please donât release anything until then. ;)
>>
>> Weâll also see if we manage to reproduce the issues. I unfortunately have
>> no Windows license anymore now that Iâve left the TU MÃnchen, so I need to
>> find a solution quick or rely on your remote debugging. If you think this
>> could be useful, we could try a chatting session. Otherwise, I could try
>> pestering my Windows-based students. ;)
So I have given your two lemmas a try on a Windows machine: both lemmas
are solved with sledgehammer (IMHO
in a reasonable amount of time, but I wait for Jasmin's opinion).  And
for some reason, e does not find a proof on
Windows for the setsum lemma while it does find one on my Macbook.

Windows machine:
* intel core i3 2120 3.30GHz
* 8 GB RAM
* Windows 8
(tested with Isabelle-RC3)


I am not a Windows user, so I do not know whether the situation is
getting worse or not.


Cheers,

Mathias


>> Cheers,
>>
>> Jasmin
>>
>>





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.