[CakeML] Build problems

[Scott Owens]

> On 2017/04/03, at 12:05, Lars Hupel <hupel at in.tum.de> wrote:
> 
> Dear list,
> 
> I'm trying to build a recent version of CakeML (0c48672).
> 
> I started out using Kananaskis 11. With that, I get the following errors:
> 
> cakeml (master)$ ../HOL-kananaskis-11/bin/Holmake
> ../HOL-kananaskis-11/bin/Holmake: Recursively calling Holmake in
> /home/lars/work/reify/HOL-kananaskis-11/examples/formal-languages/context-free
> Linking grammarScript.uo to produce theory-builder executable
> .HOLMK/grammarScript.sml:3: error: Structure (lcsymtacs) has not been
> declared
> Found near open boolSimps lcsymtacs
> .HOLMK/grammarScript.sml:5: error: Structure (finite_mapTheory) has not
> been declared
> Found near open listTheory pred_setTheory finite_mapTheory
> Static Errors
> ../HOL-kananaskis-11/bin/Holmake: Failed script build for grammarScript
> - exited with code 1
> ../HOL-kananaskis-11/bin/Holmake: Finished recursive invocation in
> /home/lars/work/reify/HOL-kananaskis-11/examples/formal-languages/context-free

We’re pretty active at moving things from CakeML into HOL, when they are general. Thus, you generally need to use an up-to-date version of HOL. Although K11 was released recently, I think it doesn’t have a lot of newer additions/changes to HOL because it was in release preparation for a long time. I’m not surprised that it doesn’t work.


> 
> A recent version of HOL (4b08982) fails to build from source in the
> first place (I didn't even get as far as trying to build CakeML).

That commit is tagged in Github as passing the regression tests. Can you give some indication how it failed, and what PolyML version you are using?

> 
> My goal is to feed fully-constructed CakeML syntax trees into the
> compiler backend. I found <https://cakeml.org/cakeml-v1-beta.zip> but
> this has various problems:
> 
> - it's outdated, as far as I can tell (?)
> - I have to feed it source code

Both are correct.

> Is it possible to get some stand-alone ML sources of the compiler?

No. The compiler is defined as a collection of HOL functions, which are translated to CakeML using the HOL->CakeML proof producing translator. You could in principle use the unverified emitML features of HOL to pretty print the HOL functions to SML, but we haven’t set that up and I imagine that it would require a non-trivial amount of boring drudge work.

Depending on exactly what you want to use the compiler for, we can probably help you to get something set up. In general, we want to provide a language and compiler that is flexible enough to incorporate into different kinds of verification projects, but have so far concentrated on the particular applications that we have been working on ourselves.

Scott