<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Fri, Jun 13, 2014 at 2:29 AM, Andy Ray <span dir="ltr"><<a href="mailto:andy.ray@ujamjar.com" target="_blank">andy.ray@ujamjar.com</a>></span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br></blockquote><div><br></div><div>Hi Andy!<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">



I was recently told about CakeML during a visit to Cambridge Uni and<br>
have been meaning to have a proper look at it.  My interest is around<br>
uses of ML (actually more specifically OCaml) on FPGAs.<br></blockquote><div><br></div><div>Excellent. Have you asked the OCaml community whether they already support any FPGA backends? If so, I expect that would probably be the best route for your interests. The focus for CakeML is full verification; if you're not at all interested in verification then you'll be going through extra hoops for nothing. That said, we also want CakeML to be a usable and useful implementation even when you don't care about verification. (It's not quite there yet...)<br>

</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

When I asked David Greaves about OCaml on FPGA he pointed out this<br>
<br>
<a href="http://technotes-djg.blogspot.co.uk/2013/08/tndjg0004-i-converted-my-processor.html" target="_blank">http://technotes-djg.blogspot.co.uk/2013/08/tndjg0004-i-converted-my-processor.html</a><br>
<br>
As a starting point I wonder if you have any advice on how I could use<br>
the code at<br>
<br>
<a href="https://github.com/xrchz/vml" target="_blank">https://github.com/xrchz/vml</a><br>
<br>
to compile an OCaml program which could run on Davids processor model?<br></blockquote><div><br></div><div>There are a few blockers at the moment to the above plan:<br><ol><li>CakeML is a subset of Standard ML, not OCaml. In particular we use the syntax of the former. There has been talk (and perhaps even a bit of work) towards supporting OCaml syntax as well (e.g. see the first item at <a href="https://cakeml.org/projects.html">https://cakeml.org/projects.html</a>) but it is not currently supported.</li>

<li>The version of CakeML Bytecode that David Greaves implemented is likely somewhat out of date - we would probably need to get back in sync with him if you want to use the latest version of the compiler. On a related note, the roadmap for CakeML involves shifting focus away from the bytecode in favour of a new backend with a more traditional series of back end languages. We hope the new backend might also be suitable for targeting FPGAs, or perhaps to support an alternative route to bytecode (which can then be implemented on FPGA), but the new backend is still work-in-progress.</li>

<li>There are probably OCaml features you want to use that aren't (yet) supported in CakeML.</li><li>The verified CakeML Bytecode implementation is not quite finished.</li></ol></div><div>So, there's plenty to work on :) If you're still interested, we could talk more about the details and what we would need to do to support your applications.<br>

<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

Longer term I am interested in the possibility of implementing<br>
something like LWT-light on top of this CPU as a potential controller<br>
for FPGA related gubbins (serial port, network, etc).<br></blockquote><div><br></div><div>Sounds cool. <br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">



In the interests of full disclosure I have no real understanding of<br>
the theorem proving world, though I suspect I probably should.<br></blockquote><div><br></div><div>If you're using CakeML it probably would make sense :)<br><br></div><div>Cheers,<br>Ramana<br></div></div></div></div>