*To*: Makarius <makarius at sketis.net>, Jasmin Blanchette <jasmin.blanchette at inria.fr>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Difficulties with "setsum" (Alfio Martini)*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Sat, 25 Apr 2015 19:45:39 -0300*In-reply-to*: <alpine.LNX.2.00.1504252228280.58599@lxbroy10.informatik.tu-muenchen.de>*References*: <mailman.39335.1429716197.13101.cl-isabelle-users@lists.cam.ac.uk> <a0620070fd15deab6d15d@192.168.1.6> <CAAPnxw0K3qVTM9A-7y5-oVgkhQZMzk_pB7rTo8vzNYb6mzv3Vg@mail.gmail.com> <alpine.LNX.2.00.1504231124570.17925@lxbroy10.informatik.tu-muenchen.de> <CAAPnxw21YLFt8xH8FJZ94Gtr6eaUnkYYL2NLM-H3sgqrHaROcw@mail.gmail.com> <alpine.LNX.2.00.1504250103380.6376@lxbroy10.informatik.tu-muenchen.de> <CAAPnxw0UyvT+AhA5Ko4m=zJ=QyEys04tbnm+AFRw7LMbA8b58Q@mail.gmail.com> <alpine.LNX.2.00.1504251057450.9247@lxbroy10.informatik.tu-muenchen.de> <CAAPnxw1TVwy7POwLa-_xhLq5OC+j6HrBhJ+Ddh4ai6jVgzHKRw@mail.gmail.com> <alpine.LNX.2.00.1504252228280.58599@lxbroy10.informatik.tu-muenchen.de>*Sender*: alfio.martini at gmail.com

Hi Makarius, First of all, many thanks for helping me working around this problem, and during the weekend! >Do you have an extra virus checker that somehow delays external program execution? Good point. I have found some obscure McAffe internet security software in my machine. I do not know how it got there. I only use Avast. Anyway, I deleted and used time out = 60. Now I solve the harder lemma both in Isabelle 2014 and Isabelle 2015-RC2. I will remove cvc4 from the provers list until that bug is corrected. Things get much faster without it. In any case, sledgehammer seems to solve problems a lot faster in Isabelle 2014 than in RC2. Who would expect that? Here are my results. Thanks a lot! Isabelle 2014 sledgehammer_params [dont_try0] (* can't be used, otherwise sledgehammer runs forever and can't be canceled. I had to kill Isabelle *) Num. Threads = 1 lemma "[a] = [b] ==> a = b" "e": Try this: by (metis the_elem_set) (13 ms). "spass": Timed out. "remote_vampire": Try this: by (metis list.inject) (15 ms). "z3": Try this: by (metis list.inject) (19 ms). lemma aux: "m < n+1 ==> setsum f {m..n + 1} = setsum f {m..n} + f (n + 1 :: int)" "e": Try this: by (metis add.commute atLeastAtMostPlus1_int_conv atLeastAtMost_iff finite_atLeastAtMost_int linorder_not_less set_upto setsum.insert zle_add1_eq_le zless_add1_eq) (1.15 s). "spass": Timed out. "remote_vampire": Timed out. "z3": Timed out. -------------------------------------------------------------------- Isabelle RC2 sledgehammer_params [dont_try0] (* mandatory *) timeout = 60 Num_Threads = 1 lemma aux: "m < n+1 ==> setsum f {m..n + 1} = setsum f {m..n} + f (n + 1 :: int)" "cvc4": A prover error occurred: Solver "cvc4" failed -- enable tracing using the "smt_trace" option for details "remote_vampire": Timed out. "z3": Try this: by (smt add.commute atLeastAtMostPlus1_int_conv atLeastAtMost_upto atLeastLessThanPlusOne_atLeastAtMost_int atLeastLessThan_iff finite_atLeastAtMost_int setsum.insert) (> 1.0 s, timed out). "spass": Timed out. "e": Timed out. 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

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

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

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

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

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

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

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

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

- Previous by Date: Re: [isabelle] Difficulties with "setsum" (Alfio Martini)
- Next by Date: Re: [isabelle] What is sumC?
- Previous by Thread: Re: [isabelle] Difficulties with "setsum" (Alfio Martini)
- Next by Thread: Re: [isabelle] Difficulties with "setsum" (Alfio Martini)
- Cl-isabelle-users April 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list