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

[Ramana Kumar]

Sounds good.

In theory version2 (and even version1) can be updated after the "deadline".
But in practice I don't expect this to happen. We had a plan to make
version1 work on a particular HOL release, but that never actually came
together. I don't intend to lock down pushes to version2: fixups until the
next HOL release will be fine. (No big new features though, obviously.)

(I will hold off on the syntactic-mti-proof merge until we have some more
consensus on the plan and deadline, and version2 has been fastforwarded
etc.)

On 23 October 2017 at 15:42, Magnus Myreen <magnus.myreen at gmail.com> wrote:

> 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
> >
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20171023/07495476/attachment-0001.html>