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



This is bounced back to isabelle-users. I am actually not the expert on sledgehammer, only the (sole?) maintainer of multiplatform support.


	Makarius

---------- Forwarded message ----------
Date: Mon, 27 Apr 2015 17:28:24 -0300
From: Alfio Martini <alfio.martini at acm.org>
To: Makarius <makarius at sketis.net>
Subject: Re: [isabelle] Difficulties with "setsum" (Alfio Martini)

HI Makarius,

Next you can try the adhoc snapshot
http://www4.in.tum.de/~wenzelm/unofficial/Isabelle_25-Apr-2015 -- it
contains the change of CVC4 by Jasmin, and a checkbox to control the "try0"
or "dont_try0" option in the Sledgehammer panel.


I have tried this snapshot version and it fails to solve that lemma about
indexed sums. All provers time out with  sledgehammer_params [dont_try0,
timeout=60] .


I set up Avast not consider any Isabelle directory, but I am sure that it
is not the problem. Meanwhile,
I installed a virtual machine with Linux Mint and installed Isabelle 2014.
Sledgehammer works
reasonably well with Threads = 1, without try methods and with timeout=60,
especially with
Z3, which seems to be the best of them by far. I will wait for
RC3 and test again with Windows & Linux. In the worst case scenario, I will
use Isabelle normally
on Windows and if I need sledgehammer, then I will use it in my virtual
Linux installation. My God,
the look and feel of Isabelle/jEdit in Linux it is not that pretty (to put
it mildly), especially if one is already used
to the Windows version.

I am not sending these messages to the list anymore. It is just me that is
having this problem,
I think.

Best!

On Sat, Apr 25, 2015 at 5:48 PM, Makarius <makarius at sketis.net> wrote:

On Sat, 25 Apr 2015, Alfio Martini wrote:

 At least I got some progress, yet the overall situation is still far from
ideal.

I got the best results with Threads=1 (instead of the default 0). "ML
Multithreading..." returns 4. Following your suggestions, here is the
summary of my tests with 2014, RC1 and RC2.

It seems that 2014 is the best option so far. So what is next?


Next you can try the adhoc snapshot
http://www4.in.tum.de/~wenzelm/unofficial/Isabelle_25-Apr-2015 -- it
contains the change of CVC4 by Jasmin, and a checkbox to control the "try0"
or "dont_try0" option in the Sledgehammer panel.


Your SledgeFail.thy contains two examples:

lemma "[a] = [b] â a = b"

lemma "m < n + 1 â setsum f {m..n + 1} = setsum f {m..n} + f (n + 1 ::
int)"


The first works smoothly for me with or without "try methods", both on
Linux and Windows.


The second takes a bit longer to produce the following results (without
"try methods").  The following is on Linux:

"cvc4": Try this: by (smt add.commute atLeastAtMostPlus1_int_conv
atLeastAtMost_iff finite_atLeastAtMost_int setsum.insert) (122 ms).
"e": Try this: by (metis add.commute atLeastAtMostPlus1_int_conv
atLeastLessThanPlusOne_atLeastAtMost_int atLeastLessThan_iff
finite_atLeastAtMost_int less_irrefl setsum.insert zle_add1_eq_le
zless_add1_eq) (761 ms).
"z3": Try this: by (smt add.commute atLeastAtMostPlus1_int_conv
atLeastAtMost_iff finite_atLeastAtMost_int setsum.insert) (158 ms).
"spass": Timed out.
"remote_vampire": Timed out.


This is on Windows 7, with sledgehammer_timeout = 60 (see plugin options):

"cvc4": Try this: by (smt add.commute atLeastAtMostPlus1_int_conv
atLeastAtMost_iff finite_atLeastAtMost_int setsum.insert) (203 ms).
"remote_vampire": Timed out.
"spass": Timed out.
"z3": Try this: by (smt add.commute atLeastAtMostPlus1_int_conv
atLeastAtMost_iff finite_atLeastAtMost_int setsum.insert) (1.2 s).
"e": Timed out.


That is less than nothing, although not as smooth as on a proper Unix
system.

Do you have an extra virus checker that somehow delays external program
execution?


        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.