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

[Makarius]

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 Unsynchronized.ref in the Isabelle 
> Tools).

Where did you see these lots of Unsynchronized.ref (or better
Synchronized.var) in Isabelle Tools?

In the last 10 years, we have got rid of most of this poking around in
mutable memory cells, and today it is mainly confined to system
infrastructure implementation, but not user tools.


	Makarius