Re: [isabelle] Sledgehammer on Windows



HI Jasmin,

If you have the clear impression that Sledgehammer is weaker and can repeat
> this on many examples, ideally with the âfact_filter = mepoâ option (using
> the âsledgehammerâ command directly, or âsledgehammer_paramsâ), I would
> like to hear again from you.


Using RC3 and s/h with the initial configuration up to

sledgehammer_params [dont_try0, fact_filter = mepo]


lemma "[a] = [b] ==> a = b"
"remote_vampire": Try this: by (metis list.inject) (31 ms).
"z3": Try this: by (metis list.inject) (501 ms).
"spass": Try this: by (metis list.inject) (500 ms).
"e": Try this: by (metis the_elem_set) (1.2 s).

lemma aux: "m <= n+1 ==> setsum f {m..n + 1} =
    setsum f {m..n} + f (n + 1 :: int)"
"cvc4": Timed out.
"remote_vampire": Timed out.
"z3": Timed out.
"spass": Timed out.
"e": Timed out.

Surprisingly, cvc4 is not mentioned at all when s/h is working on the
first, easy lemma. I repeated that
a couple of times. Hope this helps.

Best!

On Thu, May 7, 2015 at 5:09 PM, Makarius <makarius at sketis.net> wrote:

> On Thu, 7 May 2015, Alfio Martini wrote:
>
>  I have just tried Sledgehammer with RC3 with the (now usual)
>> following lemmas (without using try methods):
>>
>> 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
>>
>> - Isabelle for Linux (installed in a virtual machine): Both lemmas
>> are solved very quickly. The second is solved with cvc4 and z3.
>> I launched s/h with the standard initial configuration.
>>
>> - 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). With the second lemma, all provers time out. Using
>>  timeout=60 and Threads=1, the second lemma is solved with Z3
>>  (after a considerable amount of time, if compared with the linux
>>  version). Strangely enough, the first time I launched s/h, I got
>>  a message in a terminal window stating that cvc4 binary file
>>  was compiled without proof support (or something like that).
>>
>>
>> My machine (laptop) configuration:
>>
>> Operating System: Windows 8.1, 64-bit operating system
>> Ram Memory: 8GB
>> Processor: intel i5-3230M, 64 bit processor
>>
>
> (Change of subject line to disentangle mail threads.)
>
> That is a 2-core CPU with hyperthreading from early 2013.
>
> Can you also say something about the Antivirus software on your system?
>
>
>         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.