[CakeML-dev] speed of evaluation in logic

[Magnus Myreen]

If I remember correctly, the standard kernel has special combined
primitives and other tricky for fast EVAL. Maybe your conversions
weren't using the right things in the kernel. -- Magnus

On 1 May 2017 at 15:16, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
> 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
>
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers
>