[isabelle-dev] Circular reasoning via multithreading seems too easy

[Makarius]

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
> generated code).

So what is wrong here?

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, with lots of user tools that are mostly thread-safe.

The "implementation" manual (sections 0.7.9 and 0.8) has some brief
explanations for users of Isabelle/ML.


	Makarius