push to the public repo

[brabalan]

Now that we have arrays and a lot of interest after the CAV talk, it could be useful to push the recent modification to the public repo.

[IgnoredAmbience]

Agreed. We should also push over the tags I've created on this repo as they show the various stages of the popl14 results gathering. I should also probably tag the CAV submissions...

[brabalan]

I’m at the TC39 meeting right now so I may not have the time to work on this soon. We have a “public” branch here that is supposed to reflect the public jscert repo. I guess it’s just a matter of merging the “master” branch into it and pushing it to the other repo. I don’t know how to deal with the tags, however.

[IgnoredAmbience]

Do we want any of the jsjsref work that was on master to hit public, or @Mbodin's analyses directory?

[brabalan]

This is going to make things complicated if we don’t, won’t it? I did not realize the first step of jsjsref had reached master. Can we cherry-pick the commits we send to “public”?

[Mbodin]

Do we want any of the jsjsref work that was on master to hit public, or @Mbodin https://github.com/Mbodin's analyses directory?

Hi, There is currently almost nothing in the “analyses” directory: I’m fine with removing it (just put a flag “analyses” or such in the git repo) if it is problematic. Martin.

[IgnoredAmbience]

Unfortunately, the original jsjsref work was on master. I think there are two options:

• Keep all jsjsref work on the js_of_ocaml branch, and branch-filter it out of master (and other derivative branches). This would require everyone (who works on master) to do a git reset on their next fetch of the source repo.
• Copy across master to public, and then branch filter (or interactive rebase/cherry-picking). This would mean having to manage the diverged history between master and public in the future, which may be messy.

We should be stricter with our branching policy in the future :)

[IgnoredAmbience]

@Mbodin: Would moving it back onto the pbs branch be acceptable. I think we let it leak across when doing conrad's merges.

[Mbodin]

@Mbodin https://github.com/Mbodin: Would moving it back onto the pbs branch be acceptable. I think we let it leak across when doing conrad's merges.

It would be completely acceptable for me, yes. I don’t remember how I put this on master: it may completely be my bad, sorry about that. I don’t know how to change history in Git: is this “branch-filter” easy to perform if the changes are in different folders? Martin. P.S.: If I remember well, I found some irregularities of JSCert while trying to parse it: this may actually be the reason I have leaked stuffs here into master. If so, these changes (to JSCert, not to the “analyses” folder) should stay in master (and public if it leaks into there).

[brabalan]

@edgemaster : I’m for doing the branch filter, otherwise we’re going to regret it later. We should send a warning of the mailing list about the need to do a git reset.

[IgnoredAmbience]

Whilst at it, I'll have a go at recovering the pre-January 2013 commit history I've recently noticed we lost with the last tree rewrite.

[IgnoredAmbience]

Actually, that won't be a good idea, as then we'd also have to rewrite the public history, which is to be avoided.

[IgnoredAmbience]

My git rewriting skills aren't good enough to correctly erase the tracer directory due to its related modifications to the global Makefile. I can filter and then rebase master to edit out the modifications, but then the subsequent rebase of v8 onto the rebased master is impossible.

I'm going with the halfway house of just removing the jsjsref and analyses directories onto their own branches and leaving tracer as is.

[brabalan]

How about something simple: do a git rm in master. It will still show up in the history, but I don’t think it’s a problem.

[IgnoredAmbience]

I have pushed new-* versions of branches that have had the appropriate history rewrites applied. I've left all existing branches untouched as I'm on holiday for a week now and will be unable to firefight any breakages. We follow the same procedure as last time to activate them, flag up everyone's attention, (copy current to old-* for safety), force push new-* to , request everyone *fetch and reset --hard any local branches to prevent unwanted merges of the two diverged trees.

I've not applied the delete of the interp/tracer directory, as it may play awkward with future merges with the feature branches. (I have a feeling that both master -> feature and feature -> master merges respectively will: delete that directory; and won't make it reappear, so we'd have to be overly careful).

Sorry for the lack of coherence, I don't know why I'm working at 3am...

[IgnoredAmbience]

Since we seem to be inactive at the moment, I'm going to swap over the current branches to a old-* prefix and new-* ones to current. I've also rebased @tilk's new branch onto new-master. I hope PR#39 will survive(!)

[IgnoredAmbience]

Ok, history rewrite done as detailed in the email. This is now just blocking on confirmation of correct license in #37.