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!

## Advertising

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