On 03/12/16 14:57, Peter Lammich wrote:
>
> the attached theory is accepted by all Isabelle's from 2015 to the
> latest 2016-1-RC4, without any complaints, even in batch mode
> (isabelle build).
> It just uses a prove_future, and proves the theorem with itself!
Here is the main result of
On 05/12/16 17:13, Ondřej Kunčar wrote:
>
> If you remove the call of the function Thm.name_derivation, the cycle gets
> caught. The function
> is internally used in Goal.prove_future. It seems that the promises of the
> theorem in question
> are dropped in the function but we don’t understand
Peter and I minimized the last example:
ML‹
fun get_some var =
case Synchronized.value var of
NONE => (@{print} "defer"; get_some var)
| SOME v => (@{print} "got it"; v)
fun set var x =
Synchronized.change var (K x)
val thm: thm option Synchronized.var = Synchronized.var
On 05/12/16 11:00, Peter Lammich wrote:
> Poking on the problem a bit more, I realized that, in the
> Isabelle/jedit IDE, promises seem to be never checked. The following
> theory works fine in the IDE, but, fortunately, fails in build mode.
>
> I would have expected, at least at some point, to
> Tending global state (normally via Synchronized.var and not the raw
> Unsynchronized.ref) has been part of the normal routine of Isabelle
> maintenance in the last 10 years. At the beginning almost nothing
> worked, but around 2008/2009 it became routine. Today we have a fairly
> robust system,
Poking on the problem a bit more, I realized that, in the
Isabelle/jedit IDE, promises seem to be never checked. The following
theory works fine in the IDE, but, fortunately, fails in build mode.
I would have expected, at least at some point, to be notified of the
problem (mismatch of promised
On 04/12/16 22:52, Peter Lammich wrote:
> On So, 2016-12-04 at 22:30 +0100, Makarius wrote:
>> On 04/12/16 11:14, Lars Hupel wrote:
>>>
Where did you see these lots of Unsynchronized.ref (or better
Synchronized.var) in Isabelle Tools?
>>> There are 48 occurrences of
>> There are 48 occurrences of "Unsynchronized.ref" in "~~/src/Tools", 181
>> in "~~/src/HOL", and some more in the AFP (many of which appear to be in
>> generated code).
>
> So what is wrong here?
Nothing, as far as I am concerned. I was merely trying to answer your
question.
On 04/12/16 11:14, Lars Hupel wrote:
>> Where did you see these lots of Unsynchronized.ref (or better
>> Synchronized.var) in Isabelle Tools?
>
> There are 48 occurrences of "Unsynchronized.ref" in "~~/src/Tools", 181
> in "~~/src/HOL", and some more in the AFP (many of which appear to be in
>
This was an artificial counterexample, which I tried out of curiosity, but having applications like caching of already proved theorems in mind.Peter Originalnachricht Betreff: Re: [isabelle-dev] Circular reasoning via multithreading seems too easyVon: Makarius
> Where did you see these lots of Unsynchronized.ref (or better
> Synchronized.var) in Isabelle Tools?
There are 48 occurrences of "Unsynchronized.ref" in "~~/src/Tools", 181
in "~~/src/HOL", and some more in the AFP (many of which appear to be in
generated code).
On 03/12/16 14:57, Peter Lammich wrote:
>
> 2. Is there any simple coding policy that guarantees absence of such
> problems? Would be: "Do not store cterm/thm + everything containing it
> in references" enough, or perhaps: "Do not use Unsynchronized.ref at
> all"? (There are lots of usages of
On 03/12/16 14:57, Peter Lammich wrote:
>
> the attached theory is accepted by all Isabelle's from 2015 to the
> latest 2016-1-RC4, without any complaints, even in batch mode
> (isabelle build).
> It just uses a prove_future, and proves the theorem with itself!
The behaviour is the same in
Hi all,
the attached theory is accepted by all Isabelle's from 2015 to the
latest 2016-1-RC4, without any complaints, even in batch mode
(isabelle build).
It just uses a prove_future, and proves the theorem with itself!
So, I have two questions here:
1. I always thought that there is some
14 matches
Mail list logo
