[CakeML] Users Digest, Vol 4, Issue 1

[Kimmitt, Jonathan]

Dear Andy,
  The concept behind CakeML is a language just sufficient to run
hop-light, to allow bootstrapping
a proven theorem prover infrastructure. If you examine the source code you
will see that the byte code
implementation has departed significantly from the version used in David¹s
processor. However there
is an incomplete implementation of OCaml targeting this processor. I do
not know if this model needs
to be modified for full support of OCaml exceptions since it does not keep
track of pending stack adjustments
when an exception is taken.

A simpler approach for you if you just want to run OCaml on an FPGA and
are not interested in compiler
backend implementation would be to use the SPARC port and one of
the numerous versions of that processor such as the Leon-3 which comes
with a complete build environment for
various FPGA boards. It also supports numerous convenience features such
as step-by-step debugging using
GDB remotely over ethernet, and the ability to determine the size of the
core/caches/memory/included peripherals.

To get the network working under Ocaml will be more of a challenge
especially if you want to run bare-metal,
however there is an opam project (see http://www.openmirage.org) in
progress
to address this challenge in the Xen/Unix environment which could
potentially be extended. The biggest challenge in an embedded environment
might be memory consumption if there is plenty of copying
of functional data structures as will tend to happen in the various layers
of a network stack. Due to
the nature of FPGA development boards memory size and bandwidth will be
considerably less than what workstation
users are used to nowadays.

Regards,
Jonathan Kimmitt


>Hi,
>
>I was recently told about CakeML during a visit to Cambridge Uni and
>have been meaning to have a proper look at it.  My interest is around
>uses of ML (actually more specifically OCaml) on FPGAs.
>
>When I asked David Greaves about OCaml on FPGA he pointed out this
>
>http://technotes-djg.blogspot.co.uk/2013/08/tndjg0004-i-converted-my-proce
>ssor.html
>
>As a starting point I wonder if you have any advice on how I could use
>the code at
>
>https://github.com/xrchz/vml
>
>to compile an OCaml program which could run on Davids processor model?
>
>Longer term I am interested in the possibility of implementing
>something like LWT-light on top of this CPU as a potential controller
>for FPGA related gubbins (serial port, network, etc).
>
>In the interests of full disclosure I have no real understanding of
>the theorem proving world, though I suspect I probably should.
>
>Cheers,
>Andy
>
>
>
>------------------------------
>
>Subject: Digest Footer
>
>_______________________________________________
>Users mailing list
>Users at cakeml.org
>https://lists.cakeml.org/listinfo/users
>
>
>------------------------------
>
>End of Users Digest, Vol 4, Issue 1
>***********************************

--

World-leading research.  The government rated 8 areas of our research activity as world-leading in the Research Assessment Exercise (RAE) 2008, they were:   Allied Health Professions & Studies; Art & Design; English Language & Literature; Geography & Environmental Studies; History; Music; Psychology and Social Work & Social Policy & Administration.

This e-mail and any attachments are intended for the above named 
recipient(s)only and may be privileged. If they have come to you in 
error you must take no action based on them, nor must you copy or show 
them to anyone please reply to this e-mail to highlight the error and 
then immediately delete the e-mail from your system. Any opinions 
expressed are solely those of the author and do not necessarily 
represent the views or opinions of Anglia Ruskin University.
Although measures have been taken to ensure that this e-mail and attachments are 
free from any virus we advise that, in keeping with good computing 
practice, the recipient should ensure they are actually virus free. 
Please note that this message has been sent over public networks which 
may not be a 100% secure communications