Re: [isabelle-dev] Circular reasoning via multithreading seems too easy
On 03/12/16 14:57, Peter Lammich wrote: > > 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). Where did you see these lots of Unsynchronized.ref (or better Synchronized.var) in Isabelle Tools? In the last 10 years, we have got rid of most of this poking around in mutable memory cells, and today it is mainly confined to system infrastructure implementation, but not user tools. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Circular reasoning via multithreading seems too easy
On 03/12/16 14:57, Peter Lammich wrote: > > 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! The behaviour is the same in Isabelle2014 and Isabelle2013, which conforms to my intuition about this aspect of the system. It also means it is not a regression, so not relevant for the Isabelle2016-1 release. I can't say on the spot what is going on, and if there is a genuine error somewhere, but I can imagine a conflict of the existing dependency check of proof promises with PThm boxes of proof terms. In general, the thm type in Isabelle is definitely not what is being told in the common story about the "LCF approach", there is also not "the kernel" in Isabelle. We need to stop telling these tales. Did you encounter this situation in an actual application, or is it an artificially constructed counter-example? That makes an important difference, because it is theoretically obvious that Isabelle is not 100% correct (just like Coq, HOL-Light, ...). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Circular reasoning via multithreading seems too easy
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 1000; 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
