Poking on the problem a bit more, I realized that, in the Isabelle/jedit IDE, promises seem to be never checked. The following theory works fine in the IDE, but, fortunately, fails in build mode.
I would have expected, at least at some point, to be notified of the problem (mismatch of promised and proved thm) by the IDE. However, I can even import Scratch.thy from some other theory, without ever seeing any error in the IDE. -- Peter theory Scratch imports Main begin ML ‹ val thm_f = Future.fork (fn () => @{thm TrueI}) val thm = Thm.future thm_f @{cprop False} › lemma F: False by (tactic ‹resolve_tac @{context} [thm] 1›) (*ML ‹ Thm.join_proofs [thm]; ›*) end On So, 2016-12-04 at 23:13 +0100, Makarius wrote: > On 04/12/16 22:52, Peter Lammich wrote: > > > > On So, 2016-12-04 at 22:30 +0100, Makarius wrote: > > > > > > On 04/12/16 11:14, Lars Hupel wrote: > > > > > > > > > > > > > > > > > > > > > > > Where did you see these lots of Unsynchronized.ref (or better > > > > > Synchronized.var) in Isabelle Tools? > > > > There are 48 occurrences of "Unsynchronized.ref" in > > > > "~~/src/Tools", > > > > 181 > > > > in "~~/src/HOL", and some more in the AFP (many of which appear > > > > to > > > > be in > > > > generated code). > > > So what is wrong here? > > I find it a bit scary that my first(!) naive attempt to trick > > Isabelle > > in presence of multithreading worked out immediately. I do not > > think > > that it is a desirable state that Isabelle's soundness depends on > > correct use of multithreading by the user/tools, and, at the same > > time, > > tools are using more and more multithreading. > There might be something wrong at the very bottom (which I still need > to > figure out later), but your kind of Isabelle/ML code would expose so > many other problems in practice that is unlikely to lead to a working > tool. > > This also explains why existing tools have never tripped this odd > case, > because they use Isabelle/ML in a canonical (value-oriented) manner. > > > > > > Btw: I do not believe that the error that I found depends on a > > (low- > > level) datarace, it should (not yet tried) also work out if using > > proper synchronization to make the tactic wait for the theorem. > It is about circularity. When implementing the parallel proof > engine in > 2007/2008, I was aware that: > > (1) in practice, circularity hardly ever happens, > > (2) in theory, it might be a vector for attack. > > So I added some complexity in the implementation to address that, but > that is still an unfinished area -- there are other conflicts with > proof > terms in need of renovation. > > > Generically, Isabelle as a system is relatively hard to grasp. It is > surprising that it works so well, such that empirically most users > think > that it is unbreakable. > > This is mainly a social problem, and needs to be solved there. > > > Makarius > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev