I would like to be sure about what was discussed on collaboration (in Skype call)

[jeehoonkang]

Dear Mr. Garbuzov,
Hello, this is Jeehoon Kang.

1. First of all, please inform me if you are not comfortable for me asking in this issue tracker.
   I think my question is more or less pertaining to development; so I did not send an email for this issue and used the issue tracker.
   If you like to restrict our communication channel, please give me a feedback.
2. This repo has been recently renamed into "vellvm-legacy"; is there a reason?
   I feel like you are preparing another version; but you are currently updating this repo (like two days ago).
   So I am not confident this is the right repository I am good at working at.
   Probably this issue was discussed in Skype talk; and maybe I missed the discussion. (Sorry!) Please clarify on this issue, please.
3. I would like to make clear what we have discussed how we collaborate.
   I generally prefer the "Github" style development:
   1. If I intend to do something, I will make an issue. Discussion in this stage would be much helpful.
   2. If I intend to work on the issue, I will assign the issue to myself. Maybe issue can be tossed among us. (How to toss may be an issue, too..)
   3. After 2), I will work in a branch, named like "jeehoon_newfeatureX". And then push. (Forking is discouraged since we are in a private repo.)
   4. Send a merge request to the owner of the "master" branch (or other relevant one). Maybe lots of discussion is required in this stage. Of course, discussion in stage 1) is much better than in stage 4).

My questions are:

• Do you like this way?
• If so, to whom should I send the merge request? (For now I assume it is you!)

After this issues are resolved, I will post some issues that are really pertaining to development :-)
BTW I just cloned the repo. Really excellent job you did on migrating and maintaining the repo! Thank you!

Jeehoon

[jeehoonkang]

As an example, I sent a pull request #2.

[dgarbuzov]

1. No, the issue tracker is definitely the right venue for these questions. Let's use it unless it's clear no one else working on the project could benefit from the discussion.
2. Other than the practical issues with the organization of the code and the particulars of how we handle e.g. undef and initialization of globals, we are interested in addressing some overarching issues that arose during previous work. These have to do more with the structure of the semantics, ease of extensibility, and proof techniques. We're referring to this work as the "next version" of Vellvm, though it will likely be a while before we will support a subset of LLVM as large as the current development. It's more of a long-term goal and we're still at a stage where we are mostly just experimenting with ideas.
   At the same time, we would like to continue to support the existing code, track new versions of Coq, and make sure it's usable for ongoing work. Calling this repository "legacy" just means we would like to avoid major breaking changes (at least without some discussion first) and focus on bug fixes and making it easy to collaborate on incremental improvements. That still includes quite a bit of work, mostly focused on supporting newer versions of LLVM, not to mention a good deal of documentation and clean up.
3. The workflow you describe is very reasonable. It might not be necessary to be quite so formal all the time. For example, I think everyone would be OK with someone committing Resolve some compilation problems. #2 without discussion, since it doesn't affect the semantics. Of course it was just an example, but yes, for anything you feel could benefit from discussion, a merge request would be great.
   As for the receiver of merge requests -- I've never administered a GitHub repo before, but I don't think it's necessary for the creator of the request to assign a specific recipient. I think you can assign a specific person because you are an admin of the repository as well, but I should still get an email about a new issue whether or not you select someone.

Hope that answers your questions!
Dmitri

[dgarbuzov]

Actually, there are a few more options than I first realized:

Forking a private repository does not make it public. We can use commit to local forks and issue pull requests rather than merge requests for changes we feel warrant some discussion. We could reserve merge requests for logically separate branches, e.g. with substantial new features and multiple separate commits.

For small changes like #2, it looks like it's possible to either commit directly to the organization's repository or open a pull request and merge it yourself. It seems like the former is slightly less complicated and would avoid unnecessary email getting sent out.

[jeehoonkang]

About repos (vellvm-legacy repo, etc), I would like to further discuss. But I will talk to my boss first.

For development method (pull request, etc):

• I definitely misunderstood private repo. Yes I can fork without worrying about leak.
• I cannot see meaningful difference between merge request and pull request, so I would like to stick to one. I prefer pull request, since I can avoid accidentally pushing to master branch in this way. Of course if in case you don't mind (you said email issue above).
• For simple requests I will self-approve. For requests that require discussion I will leave it without recipient.

I think everything is clear now. Thank you for the discussion!