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

[Peter Lammich]

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 tracking to avoid exactly those
situations, making the kernel robust against data races on the user-
level/in the tools. Is such a tracking possible, how hard would it be
to implement, and how much would it impact performance? I thought about
using level-1 proof terms to track theorem dependencies, and ensure
that they are non-circular, perhaps by simply numbering them in order
of occurrence. Would this be enough?

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

-- 
  Peter

-------------


theory Scratch
imports Main
begin

ML ‹
  val thm = Unsynchronized.ref @{thm TrueI};

  fun sleep 0 = ()
    | sleep n = sleep (n-1)

  val _ = thm := (Goal.prove_future @{context} [] [] @{prop "False"}
(fn {context,...} 
    => ALLGOALS (sleep 10000000; resolve_tac context [!thm])))
›

lemma F: False
  by (tactic ‹resolve_tac @{context} [!thm] 1›)

end