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

Sun Dec 17 06:00:37 UTC 2017

Hi all,

Just a reminder that this deadline is coming up. If there's anything you
want to get into version 2 that's not already on track, it's probably a
good idea to ask for an extension.

Cheers,
Ramana

On 23 Oct 2017 09:01, "Ramana Kumar" <Ramana.Kumar at cl.cam.ac.uk> wrote:

> In that case let's set the deadline date at 22 December for version2. Get
> whatever you like in (modulo Magnus's guidelines) before then :)
>
> For continued work towards version 3, I suggest using other named branches
> (like install-and-run etc.) - I prefer keeping "version<n>" branches for
> archived rather than ongoing work.
>
> I'm planning to get the Unix examples working for fsio (currently on the
> inputLine branch) - given the later deadline, this will certainly get
> merged to master before any new version 3 material does.
>
> On 23 October 2017 at 18:23, Scott Owens <S.A.Owens at kent.ac.uk> wrote:
>
>> 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
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20171217/3252f65e/attachment.html>