[CakeML] Build problems
hupel at in.tum.de
Mon Apr 3 11:05:17 UTC 2017
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
Linking grammarScript.uo to produce theory-builder executable
.HOLMK/grammarScript.sml:3: error: Structure (lcsymtacs) has not been
Found near open boolSimps lcsymtacs
.HOLMK/grammarScript.sml:5: error: Structure (finite_mapTheory) has not
Found near open listTheory pred_setTheory finite_mapTheory
../HOL-kananaskis-11/bin/Holmake: Failed script build for grammarScript
- exited with code 1
../HOL-kananaskis-11/bin/Holmake: Finished recursive invocation in
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?
More information about the Users