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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and