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



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


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