[CakeML] Build problems

[Michael.Norrish at data61.csiro.au]

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<mailto: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<mailto: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/7aefd427/attachment.html>