On 21.11.2013, at 10:56 pm, Makarius 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
professional privilege and/o
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 newer
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 -- the
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 remote
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 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 the
> Isabelle2
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
https://bitbucket.org/isabelle_projec
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 t
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 Thu, 21 Nov 2013, Tobias Nipkow wrote:
I don't know if the attached has been reported or not, but I had to quit
Isabelle/jedit because it got stuck. This happened more often in the
past, today I have had it again. Further symptoms: poly runing 200%, no
prover running, when I click on s/h th
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 the
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 w
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
https://bitbucket.org/isabelle_project/isabelle-rele
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,
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 isabelle-release/5adc68d
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 co
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
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,
> 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 Exn.I
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 we
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 isabelle/jEd
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 m
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:
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
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
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 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 Isabelle
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 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 lim
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. (This
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 l
>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, sch
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 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 'adho
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 a
I’m not sure that we need to rush into a new release immediately.
Yes, warn the mailing list, but leave time for other problems to be reported.
Are there options that would reveal instances of this problem?
Larry
On 20 Nov 2013, at 21:49, Makarius wrote:
> We have a problem with Isabelle2013-
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
We have a problem with Isabelle2013-1 that cannot be ignored. A changeset
is included for information.
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 d
37 matches
Mail list logo