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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev