[CakeML] Build problems

[Lars Hupel]

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

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).

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

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

Cheers
Lars