> Tending global state (normally via Synchronized.var and not the raw
> Unsynchronized.ref) has been part of the normal routine of Isabelle
> maintenance in the last 10 years. At the beginning almost nothing
> worked, but around 2008/2009 it became routine. Today we have a fairly
> robust system, with lots of user tools that are mostly thread-safe.
For whatever it's worth, here's the same example with "Synchronized.var"
and without a data race:
ML‹
fun get_some var =
case Synchronized.value var of
NONE => (@{print} "defer"; get_some var)
| SOME v => v
fun set var x =
Synchronized.change var (K x)
val thm: thm option Synchronized.var = Synchronized.var "hello" NONE;
val _ =
set thm (SOME
(Goal.prove_future @{context} [] [] @{prop "False"}
(fn {context, ...} =>
ALLGOALS (resolve_tac context [get_some thm]))))
›
lemma F: False
by (tactic ‹resolve_tac @{context} [get_some thm] 1›)
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
