On 21.11.2013, at 10:56 pm, Makarius makar...@sketis.net wrote:
Did anybody test WWW_Find?
Have just confirmed that WWW_Find works fine with Isabelle2013-2-RC2
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal
Sorry, missed all this, because I was away (and the rest of NICTA had a quite
busy week).
On 21.11.2013, at 10:56 pm, Makarius makar...@sketis.net wrote:
On Wed, 20 Nov 2013, Makarius wrote:
Did anybody test WWW_Find?
WWW_Find is a NICTA-only tool. Did any of the NICTA guys test it in
On Mon, 25 Nov 2013, Gerwin Klein wrote:
the main use case for WWW_Find is with images that are potentially too
big to build yourself or that you don’t have on your machine for some
other reason (e.g. too big for a laptop or small desktop).
If the find_theorems panel could connect to a
Another approach is to have the whole prover process running
remotely, similar to the ancient rsh mode of Proof General 2.x that
is
forgotten now. Isabelle/Scala uses actors for internal
communication,
and this needs to be upgraded soon to one of the newer actor
frameworks, such as Akka --
On Mon, 25 Nov 2013, Lars Hupel wrote:
Another approach is to have the whole prover process running
remotely, similar to the ancient rsh mode of Proof General 2.x that is
forgotten now. Isabelle/Scala uses actors for internal communication,
and this needs to be upgraded soon to one of the
It says Timeout. Presumably this supports your guess.
Tobias
Am 21/11/2013 15:34, schrieb Makarius:
On Thu, 21 Nov 2013, Tobias Nipkow wrote:
Some such effects may indeed play a role, although I originally did not
observe
it when reloading a theory but while editing an existing theory.
Looks good. Sorry for the delay, and for dropping this check in the
first place (honestly I do not remember why I dropped it, but I do
remember that it was no accident ... I guess I was convinced that it
would not do any harm ;)).
chris
On 11/21/2013 10:02 PM, Makarius wrote:
On Thu, 21 Nov
On Fri, 22 Nov 2013, Christian Sternagel wrote:
honestly I do not remember why I dropped it, but I do remember that it
was no accident ... I guess I was convinced that it would not do any
harm
Just formally, the existing sources are always right. This means when
doing a change to override
On Fri, 22 Nov 2013, Christian Sternagel wrote:
Looks good.
I'm waiting for Christian to confirm this.
Chris, is this OK?
I am ready to send f6ffe53387ef to the emergency release branch
https://bitbucket.org/isabelle_project/isabelle-release
See now
From my angle Isabelle/f6ffe53387ef resolves [1] in a robust way. But
I'm waiting for Christian to confirm this.
Dmitriy
Am 21.11.2013 00:13, schrieb René Neumann:
If there will already be a new release, would it perhaps be possible to
merge the fix (given there is a robust one) for this
Am 20/11/2013 22:49, schrieb Makarius:
Are there any other potential problems of Isabelle2013-1 that were not
reported
yet?
There is a problem with autoquickcheck in Isabelle/jedit. It sometimes fails to
find or dislay a counterexample. I have a theory with a wrong lemma in it. When
I load
From your description, this looks like a timeout-problem to me ... while
your machine is loaded by proving the theory, quickcheck times out.
After the edit, there is less load, and quickcheck is faster.
--
Peter
On Do, 2013-11-21 at 10:40 +0100, Tobias Nipkow wrote:
Am 20/11/2013 22:49,
Some such effects may indeed play a role, although I originally did not observe
it when reloading a theory but while editing an existing theory.
Thanks
Tobias
Am 21/11/2013 10:48, schrieb Peter Lammich:
From your description, this looks like a timeout-problem to me ... while
your machine is
On Wed, 20 Nov 2013, Lawrence Paulson wrote:
Are there options that would reveal instances of this problem?
It happens whenever you have something still running, but continue
editing. The running tasks are errorneously interrupted and thus look
finished, although the state is failed.
On Thu, 21 Nov 2013, Peter Lammich wrote:
From your description, this looks like a timeout-problem to me ... while
your machine is loaded by proving the theory, quickcheck times out.
After the edit, there is less load, and quickcheck is faster.
Yes, this is also my first guess.
Real-time
On Thu, 21 Nov 2013, Dmitriy Traytel wrote:
From my angle Isabelle/f6ffe53387ef resolves [1] in a robust way.
This changeset amends lost updates from a few months ago, which is always
a very embarrassing situation -- a syntactic regression of the source.
Your changeset looks formally OK to
On Wed, 20 Nov 2013, Makarius wrote:
Did anybody test WWW_Find?
This is not a running gag nor a bad joke.
WWW_Find is a NICTA-only tool. Did any of the NICTA guys test it in the
Isabelle2013-1 RC phase?
There was also zero feedback about the context selector in the Find panel
of
On Wed, 20 Nov 2013, Makarius wrote:
Are there any side-conditions on the timing of a follow-up
Isabelle2013-2, e.g. concerning AFP which needs to be updated once more?
I am basically ready to ship a new release within a few days +/-. To
make it not too odd, we could wait until the start of
On Do, 2013-11-21 at 12:21 +0100, Makarius wrote:
On Wed, 20 Nov 2013, Lawrence Paulson wrote:
Are there options that would reveal instances of this problem?
It happens whenever you have something still running, but continue
editing. The running tasks are errorneously interrupted and
On Thu, 21 Nov 2013, Peter Lammich wrote:
On my machine, there is also a second way to run into this Problem: Just
load a theory with a diverging command, and wait long enough
(nondeterministically, between tens of seconds and several minutes). The
command appears to finish, and the theorem's
In an earlier message on this thread, you have posted a patch.
However,
I cannot apply this patch to the development repository, nor does the
revision db3d3d99c69d, which your patch refers to, exist.
I suppose db3d3d99c69d is the id of the patch itself, and it has
already been applied on top
On Thu, 21 Nov 2013, Peter Lammich wrote:
Are there currently real proof methods that may run out of stack space
or otherwise throw Exn.Interrupt?
The problem of Exn.Interrupt emerging explicitly or implicitly in
Isabelle/ML is an old one. I have kept an eye on that routinely in the
past
On Thu, 21 Nov 2013, Lawrence Paulson wrote:
This wasn’t noticed because there was nothing to notice: the problem is
the absence of something, rather than the presence, so it’s subtle and
insidious.
That's right, but the insidiousness of real problems has always been part
of the game that
On Thu, 21 Nov 2013, Tobias Nipkow wrote:
Some such effects may indeed play a role, although I originally did not observe
it when reloading a theory but while editing an existing theory.
Apart from timing problems there might be some internal breakdown of auto
tools that is not seen, because
Finally, here is another way how isabelle-release/5adc68deb322 (i.e.
after your first patch)
appears to have proven a non-theorem.
Load the following and just wait a moment until the tactic interrupts
due to stack-overflow. The theorem's status gets failed, but this is not
displayed in
On Thu, 21 Nov 2013, Dmitriy Traytel wrote:
From my angle Isabelle/f6ffe53387ef resolves [1] in a robust way. But I'm
waiting for Christian to confirm this.
Chris, is this OK?
I am ready to send f6ffe53387ef to the emergency release branch
On Thu, 21 Nov 2013, Lars Hupel wrote:
In an earlier message on this thread, you have posted a patch. However,
I cannot apply this patch to the development repository, nor does the
revision db3d3d99c69d, which your patch refers to, exist.
I suppose db3d3d99c69d is the id of the patch itself,
If a breakdown happens as easily as editing the text, it is a problem.
If it is merely a conceptual demonstration of breakability, if is not.
Of course my example was synthetic.
The question is: Are there currently real proof methods that may run out
of stack space or otherwise throw
On Thu, 21 Nov 2013, Peter Lammich wrote:
I think that is a clear indication that the status failed can happen
(stack-overflow, out-of-memory, what-so-ever), and should be displayed
in isabelle/jEdit!
After diagnosing the problem, I did put a note on my TODO list to make the
status reports
I doubt very much that many people are still using PG.
This wasn’t noticed because there was nothing to notice: the problem is the
absence of something, rather than the presence, so it’s subtle and insidious.
People may have encountered this problem without realising it.
Larry
On 21 Nov 2013,
Addition: The stack-overflow problem already occurs in Isabelle2013,
however, the theorem's status is unfinished here, but isabelle/jEdit
also gives no indication of this.
--
Peter
On Do, 2013-11-21 at 14:56 +0100, Peter Lammich wrote:
Finally, here is another way how
Sorry for the delay (I'm currently moving from Japan back to Austria, and
moving in takes longer than expected... Thus only irregular internet access.)
I'll have a look today in the afternoon if that is okay, otherwise I'm sure
that Dmitriy knows what he is doing :-)
cheers
chris
Makarius
On Wed, 20 Nov 2013, Makarius wrote:
Are there any side-conditions on the timing of a follow-up
Isabelle2013-2, e.g. concerning AFP which needs to be updated once more?
I am basically ready to ship a new release within a few days +/-. To
make it not too odd, we could wait until the start of
If there will already be a new release, would it perhaps be possible to
merge the fix (given there is a robust one) for this 'adhoc_overloading
raises TYPE' issue [1] ?
This error is quite puzzling. And it occurs even if one does not know
what the packages 'adhoc_overloading' and 'coercions' are
34 matches
Mail list logo
