[isabelle-dev] Isabelle/ML/Scala parallel computation and PIDE execution
Over the past few weeks, I have reworked a few aspects of parallel computation in Isabelle/ML and Isabelle/Scala, e.g. to provide Par_List.map on both sides with more or less the same semantics (concerning max. threads and cancelation of tasks). As Lars Hupel has pointed out, Scala .par is not the best way to do parallel computation, so more Isabelle library support for that makes sense. This unification of ML/Scala libraries has lead to small re-adjustments like Synchronized.value with actual synchronization in e557a9ddee5f. This seamingly tiny change (NEWS: subtle change of semantics with minimal potential for INCOMPATIBILITY) has lead to various bad consequences, such as huge waste of cycles on more than 4 cores and spurious deadlocks. (There were some private mail threads about both, concluding eventually with ba2a326fc271 and e99f706aeab9.) After some more refinements, there is even less access to costly Synchronized.value than before and more plain value-oriented programming. Moreover, I have pushed some reforms from the bottom to the top of PIDE. In particular, the global execution is no longer sequential over its ongoing history (e.g. current 702e0971d617). The practical consequence of the latter should be improved scheduling of long-running print functions, notably Sledgehammer. This means the Sledgehammer panel should work more asynchronously from the document processing, even after several edits of the text. So far this is just an intermediate outline of some reforms that came about spontaneously. We are right in the middle between two releases, so more is likely to happen. As usual, problems, observations etc. can be posted at any time, but it is important to refer to a *current* and *explicit* repository version. Makarius http://stop-ttip.org 1,235,896 Participants ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Metis vs. polymorphism
Metis proof reconstruction is already known to have occasional problems due to polymorphism. E.g. a long-pending question is how to avoid the various workarounds for Thm.bicompose that can be seen in Brownian motion here: changeset: 52225:568b2cd65d50 user:wenzelm date:Wed May 29 18:55:37 2013 +0200 files: src/HOL/Tools/Metis/metis_reconstruct.ML description: resolve_inc_tyvars: back to old behavior before 0fa3b456a267 where types of equal Vars are *not* unified -- recover last example in src/HOL/Metis_Examples/Clausification.thy; A related or unrelated Metis breakdown happened after a slight reform to give it a proper proof context (115965966e15), such that internal tools may refer to configuration options from the context as expected. A bad consequence of that were a handful of broken Metis proofs (one in main Isabelle, the rest in AFP). E.g. see changeset: 59166:4e43651235b2 user:wenzelm date:Sun Dec 21 15:59:19 2014 +0100 files: src/HOL/Cardinals/Cardinal_Order_Relation.thy description: recovered metis proof after 115965966e15 (Odd clash of type variables!?); In all these situations there were (redundant) polymorphic uses in the proof state, that could somehow cause a clash with schematic type variables inside Metis. Presumably, Metis does not observe the Isabelle proof context with its notion of locally used names -- but this is really just a guess from a big distance from the actual code. I did not change anything there, but repaired these very few proofs manually, by omitting the unused polymorphic facts. There is probably no immediate need for further action, although someone who understands Metis proof reconstruction might want to clean up its internal treatment of locally generated types, to eliminate this potential of surprise. Makarius http://stop-ttip.org 1,235,909 Participants ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle/ML/Scala parallel computation and PIDE execution
On Tue, 30 Dec 2014, Makarius wrote: So far this is just an intermediate outline of some reforms that came about spontaneously. We are right in the middle between two releases, so more is likely to happen. Another reason why more parallelism is likely to happen is my new (very modest) workstation with 12 cores / 24 hardware threads. That is actually just the low-end: the current high-end in the workstation market is at 36 cores / 72 hardware threads -- double that for high-end servers. Makarius http://stop-ttip.org 1,235,950 Participants ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
