<div dir="ltr">Sounds good.<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 2 May 2017 at 16:17, Magnus Myreen <span dir="ltr"><<a href="mailto:magnus.myreen@gmail.com" target="_blank">magnus.myreen@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi dev,<br>
<br>
The proofs for data_to_word are currently in two large files:<br>
<br>
  0) data_to_wordPropsScript.sml is 8300 lines<br>
  1) data_to_wordProofScript.sml is 15600 lines<br>
<br>
I propose that (1) is split into separate files as follows.<br>
<br>
  a) a file that defines state_rel and GC, verifies the GC<br>
  b) a file that proves the bignum lemmas<br>
  c) a file that proves the Assign case of data_to_word<br>
  d) a file that verifies compile_def<br>
<br>
I would prefer to keep (0) intact. Its purpose is to define memory_rel<br>
and prove reusable lemmas about it. Policy: (0) should be as<br>
independent as possible from the definition of wordLang and its<br>
semantics.<br>
<br>
I suspect that there isn't much resistance to splitting large files as<br>
outlined above. So my question is mostly about how the separate files<br>
should be named. Here's a suggestion:<br>
<br>
 0) data_to_word_<wbr>memoryProofScript.sml<br>
 a) data_to_word_gcProofScript.sml<br>
 b) data_to_word_<wbr>bignumProofScript.sml<br>
 c) data_to_word_<wbr>assignProofScript.sml<br>
 d) data_to_wordProofScript.sml<br>
<br>
Any comments / concerns?<br>
<br>
If no one objects, I'll make these changes on the clos_stub branch<br>
where I'm currently working in (c) for ConsExtend.<br>
<br>
Cheers,<br>
Magnus<br>
<br>
______________________________<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>
</blockquote></div><br></div>