[CakeML-dev] Naming of split ...ProofScript.sml files

Ramana Kumar Ramana.Kumar at cl.cam.ac.uk
Tue May 2 06:20:43 UTC 2017


Sounds good.

On 2 May 2017 at 16:17, Magnus Myreen <magnus.myreen at gmail.com> wrote:

> Hi dev,
>
> The proofs for data_to_word are currently in two large files:
>
>   0) data_to_wordPropsScript.sml is 8300 lines
>   1) data_to_wordProofScript.sml is 15600 lines
>
> I propose that (1) is split into separate files as follows.
>
>   a) a file that defines state_rel and GC, verifies the GC
>   b) a file that proves the bignum lemmas
>   c) a file that proves the Assign case of data_to_word
>   d) a file that verifies compile_def
>
> I would prefer to keep (0) intact. Its purpose is to define memory_rel
> and prove reusable lemmas about it. Policy: (0) should be as
> independent as possible from the definition of wordLang and its
> semantics.
>
> I suspect that there isn't much resistance to splitting large files as
> outlined above. So my question is mostly about how the separate files
> should be named. Here's a suggestion:
>
>  0) data_to_word_memoryProofScript.sml
>  a) data_to_word_gcProofScript.sml
>  b) data_to_word_bignumProofScript.sml
>  c) data_to_word_assignProofScript.sml
>  d) data_to_wordProofScript.sml
>
> Any comments / concerns?
>
> If no one objects, I'll make these changes on the clos_stub branch
> where I'm currently working in (c) for ConsExtend.
>
> Cheers,
> Magnus
>
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20170502/712004f6/attachment.html>


More information about the Developers mailing list