[CakeML] Build problems
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
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).
Thanks for all the help so far!
More information about the Users