Email Gateway (Aug 22 2022 at 09:42): Email Gateway (Aug 22 2022 at 09:42):From: Alfio Martini <alfio.martini@acm.org>
Hi Jasmin,
I finallly discover your paper "Machine Learning for Sledgehammer". So now
I know
what it means. I have only to discover how to disable it (within jEdit?).
Best!
---------- Forwarded message ----------
From: Alfio Martini <alfio.martini@acm.org>
Date: Thu, May 7, 2015 at 7:44 PM
Subject: Re: [isabelle] Isabelle2015-RC3 available for testing
To: Jasmin Blanchette <jasmin.blanchette@inria.fr>, "
cl-isabelle-users@lists.cam.ac.uk" <cl-isabelle-users@lists.cam.ac.uk>
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!
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. ;)Cheers,
Jasmin
--
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
--
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
Email Gateway (Aug 22 2022 at 09:44):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
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.
OK, that failed unfortunately. We got a 400 MB binary, which is definitely too big for Isabelle. Plan B...
Jasmin
Email Gateway (Aug 22 2022 at 09:45):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi all,
It turns out that the solution was as simple as “strip”ping the file. Now we’re back at 14 MB.
I have prepared a new component and a corresponding change for “isabelle-release”. The binary comes from Mathias, but we haven’t tested the full loop yet.
Mathias, now that the component is ready, could you apply the following change to your Isabelle (e.g. using “qimport” and “qpush” or even just modifying the two files manually or with the “patch” program)? Then the acid test in Isabelle is something like
lemma “rev (rev xs) = xs”
sledgehammer [cvc4, debug]
Check that the minimizer starts with “Testing 1 fact”, not “Testing N facts” for some large N. If this works, please tell us so that Makarius can include the change to “isabelle-release”.
Makarius, if you are impatient, you can try out the change yourself and tell us how that went.
I’m sorry for the last-minute trouble with this. This won’t solve all the issues Alfio reported (I’ll come back to them later), but it will certainly give a boost to Sledgehammer on Windows.
Cheers,
Jasmin
new_cvc.export
Email Gateway (Aug 22 2022 at 10:05):From: Makarius <makarius@sketis.net>
Dear Isabelle users,
Isabelle2015-RC3 is now available for further testing:
http://isabelle.in.tum.de/website-Isabelle2015-RC3
Changes can be inspected formally here:
https://bitbucket.org/isabelle_project/isabelle-release/commits
This is an informal summary of notable points:
- misc tuning of Isabelle/jEdit
- updated and extended "jedit" manual (including new bibtex mode)
- improved 'lift_definition' command and update of "isar-ref" manual
- last-minute refinements of Eisbach
- further polishing of BNF datatype package
- further polishing of Sledgehammer
- Windows: workaround for cvc4 in Sledgehammer
- Ubuntu 15.04: avoid odd warnings about JAVA_TOOL_OPTIONS
With ever increasing size and complexity of the system and its many add-on
tools, it is important to take testing of release candidates seriously.
People who have tested earlier release candidates should upgrade now.
Local settings can be preserved by copying $ISABELLE_HOME_USER in a
suitable manner: renaming the last component of the directory name to
Isabelle2015-RC3 before starting the new version.
The main forum for discussion is here on isabelle-users, but it is also
possible to contact the person who is responsible for particular Isabelle
tools via private mail -- better than keeping potential problems private.
When reporting problems, the subject line should be changed to something
meaningful, such that the mailing list traffic becomes more manageable.
Makarius
Email Gateway (Aug 22 2022 at 10:10):From: Alfio Martini <alfio.martini@acm.org>
Dear Makarius and Jasmin,
I have just tried Sledgehammer with RC3 with the (now usual)
following lemmas (without using try methods):
lemma "[a] = [b] ⟹ a = b" oops
lemma aux: "m < n+1 ⟹setsum f {m..n + 1} = setsum f {m..n} + f (n + 1 ::
int)"
oops
Isabelle for Linux (installed in a virtual machine): Both lemmas
are solved very quickly. The second is solved with cvc4 and z3.
I launched s/h with the standard initial configuration.
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). With the second lemma, all provers time out. Using
timeout=60 and Threads=1, the second lemma is solved with Z3
(after a considerable amount of time, if compared with the linux
version). Strangely enough, the first time I launched s/h, I got
a message in a terminal window stating that cvc4 binary file
was compiled without proof support (or something like that).
My machine (laptop) configuration:
Operating System: Windows 8.1, 64-bit operating system
Ram Memory: 8GB
Processor: intel i5-3230M, 64 bit processor
Best!
Email Gateway (Aug 22 2022 at 10:11):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Alfio,
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. ;)
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 10:11):From: Alfio Martini <alfio.martini@acm.org>
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!
Email Gateway (Aug 22 2022 at 10:11):From: Alfio Martini <alfio.martini@acm.org>
Dear Jasmin,
If you think this could be useful, we could try a chatting session.
If this proves to be necessary, I'll be more than willing to help.
Best!
Last updated: Apr 19 2024 at 20:15 UTC