Re: [isabelle] Difficulties with "setsum" (Alfio Martini)



Hi Makarius,

There is Isabelle2015-RC1 already, to try if the situation has improved. If
> not, we also need a bit of information about your hardware and operating
> system version.
> I am not aware of any such problems in Isabelle2014 or Isabelle2015-RC1,
> so unless there are tangible problem reports, the problems don't exist.


My machine (laptop) configuration:

Operating System: Windows 8.1, 64-bit operating system
Ram Memory: 8GB
Processor: intel i5-3230M, 64 bit processor

Lemmas I tried with sledgehammer

lemma "[a] = [b] â a = b" oops
lemma aux: "m < n+1 âsetsum f {m..n + 1} = setsum f {m..n} + f (n + 1 ::
int)"
oops

When I run the theory file (attached) with Isabelle2015-RC1 I get the
following messages in the output window:

Sledgehammering...
> "remote_vampire": Error: SystemOnTPTP is not available.
>
> "spass": Timed out.
> "cvc4": Timed out.
> "z3": Timed out


And with Isabelle2014, similar messages appear:

"remote_vampire": Error: SystemOnTPTP is not available.
>
> "z3": Timed out.
> "e": Timed out.
> "spass": Timed out.


One information might be useful: Usually (but not always) I have to exit
Chrome before starting
Isabelle 2014 or Isabelle 2015-RC1. Otherwise I get the error message:
"error starting  Java VM".

Thank you in advance for any help with this. I never complained before
about this because I always felt guilty when using sledgehammer. I had the
impression
that I did not wanted to work hard enough. That I was cheating.
But that feeling of guilt does not exists anymore. Hopefully it is not
because
I gave up working hard.

Best!





On Thu, Apr 23, 2015 at 6:28 AM, Makarius <makarius at sketis.net> wrote:

> On Wed, 22 Apr 2015, Alfio Martini wrote:
>
>  I use the Windows installation of  Isabelle 2014 and my sledgehammer
>> installation does not find any proof for this lemma. Actually, it never
>> finds any proof whatsoever. I have just realized that it does not solve
>> even that lemma in section 3 (First Steps) of the Sledgehammer tutorial. I
>> have always used Sledgehammer as it is packaged. I just set z3
>> non-commercial
>> use to "yes". The prover "remote-vampire" is never available (literally),
>> while e, spass and z3 always time out.
>>
>> I will have to take a look into this. This is really making may Isabelle
>> experience miserable  at the moment.
>>
>
> There is Isabelle2015-RC1 already, to try if the situation has improved.
> If not, we also need a bit of information about your hardware and operating
> system version.
>
> I am not aware of any such problems in Isabelle2014 or Isabelle2015-RC1,
> so unless there are tangible problem reports, the problems don't exist.
>
>
>         Makarius
>
>


-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
www.inf.pucrs.br/alfio
Av. Ipiranga, 6681 - PrÃdio 32 - Faculdade de InformÃtica
90619-900 -Porto Alegre - RS - Brasil



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