Re: [isabelle] Isabelle2014-RC0 segfault / sledgehammer raises exception DUP



On Wed, 23 Jul 2014, Jasmin Christian Blanchette wrote:

Sticking to pure functional data structure would add a logarithmic component and a whole lot of memory allocations in a tight loop. If the opposite of "archaic" means "slow", I'm siding with "archaic".

The opposite of archaic means fast on the usual side-conditions of our ML environment (persistent data structures in a parallel environment). The overall performance of Isabelle has increased a lot in that respect in the past 7 years. In contrast, OCaml guys usually optimize for a different execution model, and well-known provers on that platform are perceived as very slow today.

Sometimes there are archaic algorithms that insist in poking around in some array in a certain way, but that is often not necessary. I can't say anything specific about the machine-learning business -- it might require some actual work to reform it. There might be also quick-and-dirty workarounds to allocate many small arrays with a normal tree table for access -- Poly/ML does not like large blobs on the heap.


In my everyday encounter with arrarys in legacy APIs on the JVM, they usually inflict a performance hit that could have been avoided by proper immutable structures from the Scala library. This old "arrays are fast myth" is really just a myth and needs to be overcome.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.