[CakeML] cakeML build fails

Konrad Slind konrad.slind at gmail.com
Mon Jan 13 19:19:50 UTC 2014


Hi guys,

  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:

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

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

2a. The build needs lem. This should be mentioned.
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.

Thanks,
Konrad.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20140113/12778b0e/attachment.html>


More information about the Users mailing list