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 invest
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 "hello"
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 be
> 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, w
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 and
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 "Unsynchronized.r
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 "Unsynchronized.ref" in "~~/src/Tools",
> > 181
> > in
>> 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
> gen
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 An: Peter Lammich ,isa
> 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 Unsy
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 Isab
14 matches
Mail list logo