[CakeML-dev] Naming of split ...ProofScript.sml files
Magnus Myreen
magnus.myreen at gmail.com
Tue May 2 06:17:14 UTC 2017
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
More information about the Developers
mailing list