[CakeML] Build problems

[Ramana Kumar]

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.

For using s-expressions, running the encoder in Isabelle (after OpenTheory
translation) as Magnus suggested seems like a good idea to me. As Scott
mentioned, you don't need to know the s-expression format exactly (though
it's quite simple): what matters is that there are verified encode and
decode functions. In particular, there are the theorems topsexp_sexptop and
sexptop_topsexp in fromSexpTheory.

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.


On 3 April 2017 at 13:46, Lars Hupel <hupel at in.tum.de> wrote:

> > I don’t think I can debug this problem :) For what it’s worth, I’m
> > using HOL commit be4ab1074df7a6a68bb532146f9bd15b51364344 which is
> > pretty recent. You could try that for now.
>
> That commit fails with the exact same error. I'll take this to
> [hol-info] :-)
>
> > It depends a bit on what kind of assurance story you want to tell. I
> > can see a few approaches:
> >
> > 1) Translating the CakeML compiler to SML via the unverified HOL4 SML
> > extraction. The TCB includes the unverified translation and PolyML.
> >
> > 2) Translating the CakeML compiler to CakeML via the verified
> > translator, and then installing some compatibility libraries to run
> > the generated code on PolyML. The TCB is just the compatibility
> > libraries and PolyML. The compatibility libraries will have simple
> > code, but there are some differences that can’t be handled with a
> > library (such as evaluation order and the semantics of polymorphic
> > equality). However, those shouldn’t be observable in code produced by
> > the translator (this observation is something else being trusted).
> >
> > 3) Translate the CakeML compiler to CakeML and bootstrap it. Now you
> > have to produce CakeML concrete syntax to be parsed back in. You are
> > trusting your CakeML pretty printer, but not PolyML. If you wrote the
> > pretty printer in HOL4, and extracted that using the same techniques
> > from 1) and 2), then you could verify the pretty printing algorithm
> > and increase assurance, but that would not be a fun proof to do.
> >
> > 4) Translate and bootstrap the compiler, but use the alternate
> > s-expression syntax (as Magnus mentioned). The same as 3, but the
> > pretty printer is simpler and already verified.
> >
> > The difficulty of getting there from where we are now is (easiest to
> > hardest) 3, 4, 2, 1.
> >
> > If you do want a separate bootstrapped executable, then we should
> > build that for you as a release, because running the bootstrap takes
> > 2 days and needs a computer with lots of RAM.
>
> For now I'd be happy with (4). Of course, eventually this
> should be shipped with Isabelle so a source-based distribution model
> (i.e. (2)) would be preferable.
>
> Cheers
> Lars
>
>
>
> _______________________________________________
> Users mailing list
> Users at cakeml.org
> https://lists.cakeml.org/listinfo/users
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20170403/ed697545/attachment.html>