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