[CakeML] Build problems

[Lars Hupel]

Dear Scott,

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

I'm on Arch Linux, using Poly/ML 5.6. Here are the relevant logs from
"smart-configure":

OS:                 linux
poly:               /usr/bin/poly
polyc:              /usr/bin/polyc
polymllibdir:       /usr/lib
holdir:             /home/lars/work/reify/HOL
DOT_PATH:           /usr/bin/dot

... and the failing bits from "bin/build":

Building directory src/holyhammer/hh [03 Apr, 14:01:12]
hh_parse.ml       / toolbox..         | Holmake: Fail exception: Unknown
result status

Build failed in directory /home/lars/work/reify/HOL/src/holyhammer/hh
(exited with code 1)

If I re-run "bin/build" I get an error that seems to be related to OCaml:

Building directory src/holyhammer/hh [03 Apr, 14:03:21]
hh_parse.{cmi,cmx}
FAILED!
 File "hh_parse.ml", line 1:
 Error: Could not find the .cmi file for interface hh_parse.mli.
Build failed in directory /home/lars/work/reify/HOL/src/holyhammer/hh
(exited with code 1)

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

I see. That would have been the "optimal" solution for me, but if it
doesn't work, I'm happy to consider alternatives.

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

I'm working on a verified code generator for Isabelle targeting CakeML
syntax trees. So far, I execute the generated code by running it through
the semantics (using Isabelle's predicate compiler).

But my eventual goal is to offer a "button" in Isabelle that produces an
executable binary generated by the CakeML compiler. So in essence, I
need some way to run the CakeML compiler from within Isabelle.

The ideal solution would be to have everything in a single process (by
loading the CakeML compiler into the Poly/ML runtime that also runs
Isabelle). The other option would be to print the syntax trees that I've
generated and run them through whatever other mechanism you have (a
compiler binary, presumably?).

Cheers
Lars