[CakeML] Build problems

[Ramana Kumar]

To replay the s-expression encode and decode function definitions in
Isabelle after recording in OpenTheory, I don't think you would replay any
datatype definitions. You already have the CakeML datatypes (from the Lem
import), and you can define the sexp datatype manually pretty easily. You
would target those existing Isabelle datatypes when importing, as the
Magnus and Michael have suggested.

On 6 April 2017 at 13:20, <Michael.Norrish at data61.csiro.au> wrote:

> Absolutely.  You can “cut away” the HOL core library’s construction of
> types and theorems, and record instead the fact that the later CakeML work
> depends on a type called ‘a list, with various theorems proved about it.
> You can then satisfy the requirement to provide such a type and the
> accompanying theorems with stuff taken from the core Isabelle development.
>
>
>
> Michael
>
>
>
> *From: *Magnus Myreen <magnus.myreen at gmail.com>
> *Date: *Thursday, 6 April 2017 at 21:14
> *To: *Lars Hupel <hupel at in.tum.de>, Ramana Kumar <
> Ramana.Kumar at cl.cam.ac.uk>
> *Cc: *"users at cakeml.org" <users at cakeml.org>
> *Subject: *Re: [CakeML] Build problems
>
>
>
> As far as I know, OpenTheory allows starting to record from a specific
> point and allows the importer to map constants/types from one prover to
> similar ones in the other system. -- Magnus
>
> On Thu, 6 Apr 2017 at 12:14, Lars Hupel <hupel at in.tum.de> wrote:
>
> > 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?
>
> The timeline is "eventually" :-)
>
> But I'm not sure how well that would work in general. The major problem
> I foresee is this: You would replay definitions, including datatypes, in
> Isabelle, right? That means that those datatype definitions would mimic
> HOL's construction, and not Isabelle's construction. This likely means
> that I can't do anything useful with them.
>
> > Another approach would be to manually port the encoder/decoder
> definitions,
> > which might be more expedient but less satisfying and reusable.
>
> Not just more expedient but probably also faster. I'll take a stab.
>
> > 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).
>
> Fair enough.
>
> Thanks for all the help so far!
>
> 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/20170406/00fe867b/attachment.html>