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

Mon Oct 23 07:23:43 UTC 2017

I agree with the most of the reasoning, but the date for changing master must be no earlier than 22 December, 2017. We just submitted an ESOP paper that simply refers to the GitHub repo, and so the master branch needs to be something that we’d be happy with the reviewers seeing up until that point, which is when we hear whether the paper is accepted or not.

Of course nothing stops us from making a version 3 branch and using the earlier date as the point to stop concentrating on master, and start concentrating on it. However, the Unix examples working on the fsio library is an urgent, version 2 thing, since they support the ESOP paper. I’m not sure why you think they might not ever happen, or should be a version 3 thing.

Scott

> On 2017/10/23, at 06:37, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
> 
> 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
> >
> >
> 
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers