*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Difficulties with "setsum" (Alfio Martini)*From*: Makarius <makarius at sketis.net>*Date*: Mon, 27 Apr 2015 23:14:25 +0200 (CEST)*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

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 fromideal. 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

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

- Previous by Date: Re: [isabelle] "Stuck" (i.e. looping) prover issues
- Next by Date: Re: [isabelle] Difficulties with "setsum" (Alfio Martini)
- 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