[CakeML-dev] Attempt to define version 2 vs version 3

[Magnus Myreen]

Hi Ramana and dev,

I like the idea of a simple deadline. Are updates to version2 allowed
after that? I'm guessing that the version2 branch will be a bit alive
until the next HOL release at which point it will become fixed.

> Examples of things I'd like to see in version 2, but which might never
> happen: compiler bootstrap for all targets (#325, #326), cleanup TODOs (cf.
> #83), Un*x examples ported to the fsio library, a working compiler explorer
> (#80), and many of the "tidying up" things you mentioned.

I wouldn't be as pessimistic as "might never happen". I'll make sure
"a working compiler explorer (#80)" happens because I want to use it.
I've given it some thought and come to the conclusion that it
shouldn't be too hard to produce as a command-line tool. However, I
don't intend to rush it to get it into version 2.

I would like to get #347 done before the version 2 deadline, and maybe
also append-op.

> I agree with the three points in your guidelines on what version 2 should
> contain. I think all of them are already on current master.

Yes, they are currently on master, but soon they will not if
syntactic-mti-proof is merged.

Cheers,
Magnus


On 23 October 2017 at 11:06, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
> Hi Magnus,
>
> I want to voice continued agreement with this paragraph:
>
>     We have previously decided that everything to do with the
>     install-and-run semantics changes belong to version 3. Currently, I
>     see master as a "finishing up version 2" branch. So if something
>     belongs to version 3, then it should not currently be merged into
>     master.
>
> However, below I will propose to change that policy soon.
>
> Having observed the development over the years, one (perhaps distasteful)
> prediction I make is that version 2 will never be finished. I mean
> "finished" in the sense of "every improvement we've thought of, that is
> consistent with version 2's goals (whatever they are), has been committed".
> Examples of things I'd like to see in version 2, but which might never
> happen: compiler bootstrap for all targets (#325, #326), cleanup TODOs (cf.
> #83), Un*x examples ported to the fsio library, a working compiler explorer
> (#80), and many of the "tidying up" things you mentioned.
>
> Therefore I would suggest we simply set a deadline (date) on which we
> declare version 2 finished, stop moving the version2 branch forward after
> that, and continue work on version 3 (on master when things build, and
> branches otherwise). I propose November 1 for this date. Why so soon?
> 1. We've done all the work on version 2 already.
> 2. Maintaining two versions / backporting fixes etc. isn't fun, and will
>    slow down development of version 3.
> 3. Nobody really cares about released versions of CakeML at this point in
>    history. In practice, we're usually going to tell people to use the
>    current tip of master for work on top of CakeML.
>
> I agree with the three points in your guidelines on what version 2 should
> contain. I think all of them are already on current master. So is there
> anything anyone is very keen on getting into version 2 before we archive it?
> You mention #71 - is that feasible within a week? Worthwhile?
>
> Cheers,
> Ramana
>
>
> On 23 October 2017 at 13:50, Magnus Myreen <magnus.myreen at gmail.com> wrote:
>>
>> Hi all,
>>
>> The time has come to decide what should be in version 2 of the
>> compiler and what should not.
>>
>> We have previously decided that everything to do with the
>> install-and-run semantics changes belong to version 3. Currently, I
>> see master as a "finishing up version 2" branch. So if something
>> belongs to version 3, then it should not currently be merged into
>> master.
>>
>> I propose the following guidelines:
>>  - having 12 intermediate languages belongs to version 2 (ICFP'16)
>>  - using clos_relation belongs to version 2 (ICFP'17)
>>  - having signatures on modules belongs to version 2 (POPL+ICFPs)
>>
>> I bring this up now because the syntactic-mti-proof branch
>> deletes clos_relation. This branch is a branch off of master, which
>> means that it naturally merges in there.  It is clear that
>> clos_relation was a lot of work and a big part of the contribution in
>> this year's ICFP paper. I therefore hesitate to just merge in and
>> delete clos_relation from master. (Yes, it would be in the version
>> history, but as we know once some time has passed and files have moved
>> around, version history is not so easy to navigate. This is
>> particularly true if the interested reader is not a CakeML developer.)
>>
>> The reason for why I reworked the proofs to avoid clos_relation is
>> that I couldn't see how to update it for install-and-run. As such, the
>> changes on syntactic-mti-proof sound like they belong to version 3.
>>
>> I note that we already have a branch called "version2". We could
>> simple merge in master into it and then have master be open to
>> version 3 material. However, what is currently on master (and thus on
>> the way into version 2) needs some tidying up and improving, e.g. the
>> basis library could do with some more work, similarly Yong Kiam
>> mentioned that some of the non-x86 targets don't have up-to-date
>> .S-file generation for bitmaps. (I also plan to add readme
>> comments/generation everywhere before version 2 is complete,
>> i.e. close issue #71.) As I said, we could do tidying up work as
>> branches of the "version2" branch, but then people need to keep this
>> in mind so that new tidying-up work isn't accidentally a branch off of
>> a version-3 master.
>>
>> What do you think of my guidelines above?
>>
>> Should master stay, for the time being, as a a "finishing up version
>> 2" branch? Or should be start using the "version2" branch for this
>> purpose and let version 3 material into master?
>>
>> Cheers,
>> Magnus
>>
>> _______________________________________________
>> Developers mailing list
>> Developers at cakeml.org
>> https://lists.cakeml.org/listinfo/developers
>
>