<div dir="ltr"><div><div><div><div><div>Hi guys,<br><br></div>  I've downloaded cakeML from git and have been building it. I was warned<br>that I needed 16 GB to do everything, so I expected failure. But I wanted<br>to see how far it got before crashing. Here's the error message:<br>
<br>294 declarations still to go<br>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.<br>
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<br>
runtime: 17m06s,    gctime: 16m47s,     systime: 3m42s.<br>Exception- Interrupt raised<br>Holmake: Failed script build for compileReplDecsScript - exited with code 1<br>make: *** [all] Error 1<br><br><br></div>Questions:<br>
<br></div>1. Is this the expected place of failure? (This is on an 8 GB box running PolyML 5.5).<br><br></div>2. I just invoked "make" in the top level. What is the invocation if I wanted to avoid<br>    the memory-expensive bootstrap?<br>
<br></div><div>2a. The build needs lem. This should be mentioned.<br></div><div>2b. In lem, the hol-lib directory has a spurious file called stringScript.sml that <br></div><div>      derails the build. I've talked to Scott about this already.<br>
<br></div><div>3. I would like to explore the verification aspects of the system. In particular, suppose<br></div><div>    I want to define (executable) functions in HOL and prove properties, then somehow<br></div><div>    map the functions to cakeML and get some sort of "correctness-of-compilation" <br>
</div><div>    theorem out that I can use to make a formal connection between the properties, the<br></div><div>    function, and the executable code.<br> <br></div><div>    For example, I define factorial and prove that it is always positive:<br>
<br></div><div>      val fact_def = Define `fact n = if n <= 0 then 1 else n * fact (n-1)`;<br></div><div>      (* The fact function could be over integers, if need be. *)<br><br></div><div>      val fact_pos = prove(``!n. 0 < fact n``, ....);<br>
<br></div><div>      ... and now what steps do I take? I have read the relevant papers by Magnus and<br></div><div>      others, but now I am seeking more concrete hints.<br><br></div><div>Thanks,<br>Konrad.<br><br></div>
</div>