*** Prover IDE -- Isabelle/Scala/jEdit ***

* Dockable window "Sledgehammer" manages asynchronous / parallel
sledgehammer runs over existing document sources, independently of
normal editing and checking process.


This refers to Isabelle/bca3769b6b45. It should be usable already, although rounds 2 and 3 of refinements still need to be done before the coming release, to ensure that the multithreading and interrupting really works.

All this has required a few years longer than anticipated. In 2005 Larry had proposed to make everything in Isabelle work concurrently, now we are more or less there. It is now subsumed by the PIDE document model, and the implementation is not so big after all, probably smaller than the earlier isolated attempts taken together (e.g. the first multi-threaded ATP manager from summer 2008.)


        Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to