<div dir="ltr">Thanks for clarifying, I was thinking of:<div><br></div><div>1) There is a compiler in the logic, e.g. compile :ast -> bytes (ignoring configurations)</div><div><br></div><div>2) Translate this compiler, to get some cakeml AST (in HOL) [..., val compile = ... ]</div><div><br></div><div>3) Add new FFI/IO decls to the AST (as we do now) to get the full compiler [..., val compile = ..., val main = ... ]</div><div><br></div><div>4) Define a new constant for the AST in 3),  |- cml_ast =  [..., val compile = ..., val main = ... ]</div><div><br></div><div>5) Translate cml_ast to get the deeply embedded version of the AST: ``val cml_ast  = [ ... ]``<br></div><div><br></div><div>6) Stick cml_ast onto the back of 2): [ ..., val compile = ..., val cml_ast = [ ...], val main = print (compile cml_ast)]</div><div><br></div><div>7) Run the in-logic compiler on 6 (doesn't need to be the same as 1)</div><div><br></div><div>I think Q2 would be 4) and Q1 would be 2).</div><div><br></div><div>How does it speed things up (maybe?): 7) would run a "fast" version of the compiler in the logic, but it produces a program that runs a "slow" version of the bootstrap outside the logic.</div><div><br></div><div>RE: translation bottleneck, it won't get past it, because we still need to translate the whole compiler anyhow. The main purpose would be to speedup bootstrap compilation, but I am not sure if the "fast" in-logic compiler exists though.</div><div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Feb 11, 2017 at 6:56 AM, Ramana Kumar <span dir="ltr"><<a href="mailto:Ramana.Kumar@cl.cam.ac.uk" target="_blank">Ramana.Kumar@cl.cam.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">This looks like an interesting idea. I haven't understood it fully.<br>
Let me try to clarify.<br>
Here are 2 questions I have about your 2-fold example, which I'll copy below:<br>
<br>
val prog2fold = process_topdecs`<br>
val (compile,conf) = ^Q1;<br>
val cml_ast = ^Q2;<br>
val main = print(compile conf cml_ast);`<br>
<br>
My questions are about what Q1 and Q2 should be.<br>
<br>
I assume the above program, prog2fold, is going to be used as input<br>
for proof-grounded evaluation of the compiler, i.e., we will produce a<br>
theorem like this by EVAL: |- compile ^prog2fold = <... some bytes<br>
...><br>
<br>
I guess Q2 is produced by translator (i.e., what is currently in<br>
compiler/bootstrap/<wbr>translation). I understand that part, if so.<br>
<br>
Is Q1 also produced by the translator? i.e., we roughly have Q1 = Q2?<br>
Or what is it?<br>
<br>
I think this would be interesting if it provided a principled way to<br>
substantially increase the speed for bootstrapping. It also seems like<br>
it would interact interestingly with the eval primitive. It seems to<br>
have no effect on the translation-time bottleneck for bootstrap speed,<br>
though.<br>
<div><div class="gmail-h5"><br>
On 11 February 2017 at 16:34, Yong Kiam <<a href="mailto:tanyongkiam@gmail.com">tanyongkiam@gmail.com</a>> wrote:<br>
> Hi dev,<br>
><br>
> This is more of a random question than anything. I was wondering if it is<br>
> possible to get a theorem about k-fold bootstrap of the compiler, i.e. using<br>
> the compiler to iterate compilation on itself once in the logic and k-1<br>
> times (outside the logic).<br>
><br>
> Concretely, 1-fold bootstrap would be what we have right now, so the code<br>
> being compiled in the logic looks like:<br>
><br>
> ...<br>
> val main str = print (compile conf str);<br>
><br>
> A 2-fold bootstrap could look like:<br>
><br>
> ...<br>
> val cml_ast = ... //from an iterated translation of the compiler AST in HOL<br>
> into a translated AST<br>
> val main = print(compile conf (cml_ast));<br>
><br>
> i.e. the output is a program, that when run, compiles the compiler AST.<br>
><br>
> My sense is that such a k-fold bootstrap theorem could probably be done with<br>
> what we have now (replace cml_ast with the appropriate n-1 th translation).<br>
> The corresponding top-level correctness theorem would have some weird nested<br>
> assumptions about each time the bootstrap is ran.<br>
><br>
> One possible use of 2-fold bootstrap: one could evaluate in HOL using a fast<br>
> (but less optimizing) version of the compiler, then turn on all the<br>
> optimizations inside cml_ast. It probably doesn't matter for our bootstrap<br>
> speed though.<br>
><br>
><br>
</div></div>> ______________________________<wbr>_________________<br>
> Developers mailing list<br>
> <a href="mailto:Developers@cakeml.org">Developers@cakeml.org</a><br>
> <a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/developers</a><br>
><br>
</blockquote></div><br></div></div></div>