[CakeML] cakeML build fails

Tue Jan 14 21:09:44 UTC 2014

Thanks Magnus. I will do as you suggest.

I haven't absorbed your last point yet, so this is half-baked,
but I can imagine using the compiler to generate executables
that get linked in with I/O components coming from (say) a pre-existing
C library, so that the repl is not involved at all. Is that a possbile
scenario for cakeML?

Cheers,
Konrad.

On Tue, Jan 14, 2014 at 2:51 PM, Magnus Myreen
<magnus.myreen at cl.cam.ac.uk>wrote:

> 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
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20140114/14d926af/attachment.html>