[CakeML] cakeML build fails

[Magnus Myreen]

Hi Konrad,

>   I've downloaded cakeML from git and have been building it. I was warned
> that I needed 16 GB to do everything, so I expected failure. But I wanted
> to see how far it got before crashing. Here's the error message:

As far as I know, the full bootstrap has only been successfully run on
a 64 GB machine, but maybe Ramana had some data suggesting 16 GB would
is enough.

> 294 declarations still to go
> 0: (val opn_to_prim2)0 (val div_exc_cn)1 (val cdiv_exc)2 (val eq_exc_cn)3
> (val ceq_exc)4 (fun pat_to_cpat*)5 (fun exp_to_cexp*)6 (datatype
> call_context)7 (fun lunion)8 (val lshift)9 (fun free_vars*)10 (val
> bind_fv)11 (fun label_closures*)12 (val get_label)13 (val pushret)14 (fun
> compile_envref)15 (val compile_varref)16 (val el_check)17 (val
> bool_to_tag)18 (val unit_tag)19 runtime: 21m34s,    gctime: 21m07s,
> systime: 2m40s.
> 1: (val block_tag)0 (fun num_fold)1 (val push_lab)2 (val emit_ceref)3 (val
> emit_ceenv)4 (val closure_tag)5 (val cons_closure)6 (val update_refptr)7
> (val compile_closures)8 (val prim1_to_bc)9 (val prim2_to_bc)10 (fun
> compile*)Warning - Unable to increase stack - interrupting thread
> runtime: 17m06s,    gctime: 16m47s,     systime: 3m42s.
> Exception- Interrupt raised
> Holmake: Failed script build for compileReplDecsScript - exited with code 1
> make: *** [all] Error 1
>
>
> Questions:
>
> 1. Is this the expected place of failure? (This is on an 8 GB box running
> PolyML 5.5).

That looks like the expected choke point.

> 2. I just invoked "make" in the top level. What is the invocation if I
> wanted to avoid
>     the memory-expensive bootstrap?

You'll need to replace

vml/bootstrap/compileReplDecsScript.sml

with

vml/bootstrap/compileReplDecsCheatScript.sml

and also delete "Cheat" in the second line in the file, i.e. the
new_theory command.

> 2a. The build needs lem. This should be mentioned.

Yes, lem is required for silly Holmake reasons.

> 2b. In lem, the hol-lib directory has a spurious file called
> stringScript.sml that
>       derails the build. I've talked to Scott about this already.
>
> 3. I would like to explore the verification aspects of the system. In
> particular, suppose
>     I want to define (executable) functions in HOL and prove properties,
> then somehow
>     map the functions to cakeML and get some sort of
> "correctness-of-compilation"
>     theorem out that I can use to make a formal connection between the
> properties, the
>     function, and the executable code.
>
>     For example, I define factorial and prove that it is always positive:
>
>       val fact_def = Define `fact n = if n <= 0 then 1 else n * fact (n-1)`;
>       (* The fact function could be over integers, if need be. *)
>
>       val fact_pos = prove(``!n. 0 < fact n``, ....);
>
>       ... and now what steps do I take? I have read the relevant papers by
> Magnus and
>       others, but now I am seeking more concrete hints.

To turn your fact function into CakeML, you'll need to run it through
the translator, i.e. write a file like

  vml/translator/ml_translator_demoScript.sml

for your fact function, which can use num. The translator turns HOL
``:num`` into CakeML ints and maintains an invariant that the CakeML
ints are not negative.

To reason about the machine code or bytecode that executes this CakeML
is a bit more tricky. The top-level theorem makes a statement about
the whole system in terms of an input stream of characters and an
output stream of characters. I guess we'd need a verified pretty
printer to turn CakeML AST into a string that is guaranteed to parse
back as that CakeML AST. Alternatively, one can try to evaluate (in
the logic) a the application of the parser to a string representing
that AST and check that the parser maps that string into the desired
AST. Then you'll need to somehow talk about your fact function in the
context of all the other code that gets input during execution of the
read-eval-print loop. The final theorem would be about the output
string and terminate/diverge behaviour of the entire system with the
fact function fed in on the input stream.

I'm rather vague about the last parts because we haven't yet worked
through all the details. But we aim to do so in conjunction with the
verified HOL light case study.

Cheers,
Magnus

> Thanks,
> Konrad.
>
>
> _______________________________________________
> Users mailing list
> Users at cakeml.org
> https://lists.cakeml.org/listinfo/users
>