[CakeML] Build problems

Scott Owens S.A.Owens at kent.ac.uk
Mon Apr 3 12:32:17 UTC 2017


> On 2017/04/03, at 13:08, Lars Hupel <hupel at in.tum.de> wrote:
> 
> 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)

I don’t think I can debug this problem :) For what it’s worth, I’m using HOL commit be4ab1074df7a6a68bb532146f9bd15b51364344 which is pretty recent. You could try that for now.

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

Very cool.

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

It depends a bit on what kind of assurance story you want to tell. I can see a few approaches:

1) Translating the CakeML compiler to SML via the unverified HOL4 SML extraction. The TCB includes the unverified translation and PolyML.
2) Translating the CakeML compiler to CakeML via the verified translator, and then installing some compatibility libraries to run the generated code on PolyML. The TCB is just the compatibility libraries and PolyML. The compatibility libraries will have simple code, but there are some differences that can’t be handled with a library (such as evaluation order and the semantics of polymorphic equality). However, those shouldn’t be observable in code produced by the translator (this observation is something else being trusted).
3) Translate the CakeML compiler to CakeML and bootstrap it. Now you have to produce CakeML concrete syntax to be parsed back in. You are trusting your CakeML pretty printer, but not PolyML. If you wrote the pretty printer in HOL4, and extracted that using the same techniques from 1) and 2), then you could verify the pretty printing algorithm and increase assurance, but that would not be a fun proof to do.
4) Translate and bootstrap the compiler, but use the alternate s-expression syntax (as Magnus mentioned). The same as 3, but the pretty printer is simpler and already verified.

The difficulty of getting there from where we are now is (easiest to hardest) 3, 4, 2, 1.

If you do want a separate bootstrapped executable, then we should build that for you as a release, because running the bootstrap takes 2 days and needs a computer with lots of RAM.

Scott


More information about the Users mailing list