Peter and I minimized the last example:
ML‹
fun get_some var =
case Synchronized.value var of
NONE => (@{print} "defer"; get_some var)
| SOME v => (@{print} "got it"; v)
fun set var x =
Synchronized.change var (K x)
val thm: thm option Synchronized.var = Synchronized.var "hello" NONE;
val future_thm = Thm.future
(Future.fork (fn _ => get_some thm |> Thm.name_derivation ""))
@{cprop "False"}
val _ = set thm (SOME future_thm);
val _ = Thm.join_proofs [future_thm]
›
lemma F: False
by (tactic ‹resolve_tac @{context} [get_some thm] 1›)
If you remove the call of the function Thm.name_derivation, the cycle gets
caught. The function
is internally used in Goal.prove_future. It seems that the promises of the
theorem in question
are dropped in the function but we don’t understand whether this was intended
or not.
Hopefully, this helps you to pin down the problem.
Bests,
Ondrej
> On 5 Dec 2016, at 11:12, Lars Hupel <hu...@in.tum.de> wrote:
>
>> 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
smime.p7s
Description: S/MIME cryptographic signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
