[CakeML-dev] speed of evaluation in logic

[Ramana Kumar]

Hi all,

On the cleanup branch I've been making the compilation-in-logic method used
by the bootstrap into a library to be used for compiling in the logic
generally. (This is issue #249.) The bootstrap method involves lots of
custom conversions and parallelised evaluation where possible. Preliminary
use of it to compile the characteristic examples suggests, however, that it
might be a lot slower than what was used before (essentially EVAL using the
compiler compset).

While we might expect some slowdown due to additional printing and
intermediate definitions, I would have overall expected a speedup. I'm just
noticing this based on my recollection of building the examples the EVAL
way (15 mins I thought) and so may be totally wrong about the slowdown.
More careful experiments would need to be done. And if EVAL really is
faster, I'd want to understand why! Or how to exploit it further!

Systematic experiments on various strategies for evaluation in the logic
could be interesting. We have a big program (the compiler) to do them with.
I tried various strategies for one compilation phase once (it's still in
the comments of x64BootstrapScript.sml) and could never beat EVAL and never
understood why not, because I was doing the most direct efficient custom
conversion I thought possible.

On a separate note, I will be out of contact (and not working on CakeML -
I'll be at an intensive training camp) from Wednesday for a week. I hope
nothing urgent comes up, and if you want to plan for any contingencies
beforehand, email me. (I will probably still have email during the week,
but not much access.)

Cheers,
Ramana
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20170501/d10bf186/attachment.html>