[CakeML] Build problems

[Magnus Myreen]

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

Would the bootstrapped compiler work for you? The bootstrapped
compiler runs from the Unix command line just like any compiler (e.g.
gcc). You might want to use it through the s-expression parser rather
than the usual parser which parses SML syntax, because it easier to
pretty print to s-expressions in a way that will be parsed to exactly
the same AST.

Cheers,
Magnus



On 3 April 2017 at 14: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)
>
>> 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
>
> _______________________________________________
> Users mailing list
> Users at cakeml.org
> https://lists.cakeml.org/listinfo/users