[CakeML] Build problems

[Ramana Kumar]

On 5 April 2017 at 11:14, Lars Hupel <hupel at in.tum.de> wrote:

> Hi Ramana,
>
> > I think (4) is better in the long run too. The TCB is smaller than (2).
> > Isabelle already ships with binaries, so I think it would make sense to
> > include a verified CakeML binary for this functionality.
>
> so, would it be possible to get a binary from somewhere? (Either with a
> CakeML parser or sexp syntax.)
>

A preliminary binary with the CakeML parser can be downloaded here:
https://cakeml.org/cake-32b749c3.S.tar.gz

To build it, one needs the file basis/basis_ffi.c from the repository, then
run:
gcc -o cake basis_ffi.c cake-32b749c3.S

If you feed the resulting executable source code on standard input, it will
produce another .S file on standard output which can be built using the
same recipe (i.e. linked with basis_ffi.c using gcc).


> > The fromSexpTheory doesn't seem to depend on much except astTheory (which
> > you already would have a copy of from your Lem -> Isabelle translation of
> > the CakeML semantics), and simpleSexpTheory (of which it only depends on
> > the sexp datatype - you could define that yourself in Isabelle manually
> > very simply). There is some work on importing OpenTheory packages into
> > Isabelle here:
> > https://github.com/xrchz/isabelle-opentheory
> >
> > To record the fromSexpTheory into OpenTheory format, I think you just
> need
> > to build it in the otknl.
>
> I'm not sure I know what that means or how I would do that.


It's quite an involved process unfortunately. At a high level, the idea is
as follows. One can record the definitions and proofs in a theory, at the
level of primitive inferences, in HOL4 and replay them in Isabelle/HOL.
This is one method of transporting a formal development from one system to
the other.

If you build a copy of HOL4 using the -otknl flag to bin/build, it uses the
proof-recording version of the HOL4 kernel and I think it will generated
OpenTheory articles for many of the standard library theories
automatically. (One wrinkle with using this for CakeML I just realised is
that the proof-recording kernel has slightly different generated-names
behaviour than the standard kernel and CakeML is only known to build on the
latter.)

What's your timeline for this project, and would you be interested in
working on producing an OpenTheory export of parts of CakeML with my
guidance?

Another approach would be to manually port the encoder/decoder definitions,
which might be more expedient but less satisfying and reusable.


> Is there a
> reason why the sexp encoders/decorders are not specified in Lem?
>
>
They're not part of the semantics. There's overhead to using Lem, and there
aren't formal guarantees that it produces the same semantics in multiple
systems (although I believe a fair amount of work has gone into ensuring
that is usually the case).


> Cheers
> Lars
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20170405/54b83bdb/attachment.html>