[CakeML] Build problems

[Lars Hupel]

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.)

> 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. Is there a
reason why the sexp encoders/decorders are not specified in Lem?

Cheers
Lars