[CakeML] Build problems

[Lars Hupel]

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

That commit fails with the exact same error. I'll take this to
[hol-info] :-)

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

For now I'd be happy with (4). Of course, eventually this
should be shipped with Isabelle so a source-based distribution model
(i.e. (2)) would be preferable.

Cheers
Lars