[CakeML] Build problems

[Magnus Myreen]

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/370897aa/attachment-0001.html>