[CakeML] Build problems

Lars Hupel hupel at in.tum.de
Thu Apr 6 10:13:50 UTC 2017

> 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!


More information about the Users mailing list