Email Gateway (Aug 22 2022 at 09:42): Email Gateway (Aug 22 2022 at 09:42):From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi all,
Le 08/05/2015 00:44, Alfio Martini a écrit :
Hi Jasmin,
That’s really bad — that lemma is supposed to be ultra easy. In a previous
email, I suggested > you try disabling MaSh. Did that make any change?I certainly missed that remark. I have no idea what is MaSh. How can I
disable it?
There is something about it in Isabelle Plugin Options.Best!
Put none in the options (documentation panel > sledgehammer manual, §7.2).
On Thu, May 7, 2015 at 7:31 PM, Jasmin Blanchette <
jasmin.blanchette@inria.fr> wrote:Dear Alfio,
- 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).
That’s really bad — that lemma is supposed to be ultra easy. In a previous
email, I suggested you try disabling MaSh. Did that make any change?Otherwise, thanks to my colleague Mathias Fleury, we should be able to
include CVC4 executables with proof output in RC4 and/or the final
Isabelle2015 release. We will look into this in the next 24 hours.
Makarius, please don’t release anything until then. ;)We’ll also see if we manage to reproduce the issues. I unfortunately have
no Windows license anymore now that I’ve left the TU München, so I need to
find a solution quick or rely on your remote debugging. If you think this
could be useful, we could try a chatting session. Otherwise, I could try
pestering my Windows-based students. ;)
So I have given your two lemmas a try on a Windows machine: both lemmas
are solved with sledgehammer (IMHO
in a reasonable amount of time, but I wait for Jasmin's opinion). And
for some reason, e does not find a proof on
Windows for the setsum lemma while it does find one on my Macbook.
Windows machine:
I am not a Windows user, so I do not know whether the situation is
getting worse or not.
Cheers,
Mathias
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 09:42):From: Lars Hupel <hupel@in.tum.de>
Hello,
I've started up my Windows 8 VM (in VirtualBox, using 4 GB of RAM,
single core) and installed RC3. Here are my findings, should they be
helpful to anyone:
lemma "[a] = [b] ⟹ a = b"
With "try methods" enabled:
"remote_vampire": Error: SystemOnTPTP is not available.
"z3": Try this: by simp (0.0 ms).
"spass": Try this: by auto (0.0 ms).
"e": Try this: by simp (0.0 ms).
With "try methods" disabled:
"cvc4": Try this: by (metis list.inject) (0.0 ms).
"remote_vampire": Try this: by (metis list.inject) (0.0 ms).
"z3": Try this: by (metis list.inject) (15 ms).
"spass": Try this: by (metis list.inject) (0.0 ms).
"e": Try this: by (metis the_elem_set) (156 ms).
lemma "m < n+1 ⟹setsum f {m..n + 1} = setsum f {m..n} + f (n + 1 ::
int)"
"cvc4": Try this: by (smt ... a bunch of facts ...) (235 ms).
"remote_vampire": Timed out.
"z3": Try this: by (simp add: add.commute atLeastAtMostPlus1_int_conv)
(109 ms).
"spass": Timed out.
"e": Timed out.
Cheers
Lars
Email Gateway (Aug 22 2022 at 09:44):From: Alfio Martini <alfio.martini@acm.org>
HI Jasmin,
If you have the clear impression that Sledgehammer is weaker and can repeat
Email Gateway (Aug 22 2022 at 10:10):From: Makarius <makarius@sketis.net>
(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
Email Gateway (Aug 22 2022 at 10:11):From: Alfio Martini <alfio.martini@acm.org>
Hi Makarius,
Avast free antivirus, 2015.
Best!
Email Gateway (Aug 22 2022 at 10:11):From: Makarius <makarius@sketis.net>
I booted up my old laptop in Windows 8.1 64bit, with more or less the
same results: failure of the second example.
Hardware: i7-3632QM 4-core hyperthreading, 8 GB, using threads=4.
No antivirus that could cause problems starting executables.
Experimenting a bit with existing examples of nitpick, sledgehammer, and
smt as proof method, it all seems to work as it used to work in
Isabelle2014. I.e. there are no new problems of the updated Cygwin of
Isabelle2015-RC4, as far as I can see at the moment.
Maybe there is something wrong with MaSH. I've no proper idea how that
actually works.
Makarius
Email Gateway (Aug 22 2022 at 10:11):From: Alfio Martini <alfio.martini@acm.org>
Hi Makarius,
Experimenting a bit with existing examples of nitpick, sledgehammer, and
Last updated: Apr 24 2024 at 01:07 UTC