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

Makarius makarius at sketis.net
Sat Dec 3 20:58:08 CET 2016

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.


More information about the isabelle-dev mailing list