Merging PRs

Stream: iris-lean

[Zongyuan Liu]

Hi, I’ve noticed a few PRs are waiting for review for a while. How does the reviewing and merging process work for Iris-Lean? Is there anything one can do to help move these PRs along?

[Mario Carneiro]

there are a few people who can help with general review, and when that's done ping me and I will give a final review and merge. I benefit a lot from people letting me know that things are actually ready since they spend a while on the PR queue while they are still in development, and I don't have much dedicated time for maintaining iris-lean ATM. I will try to do a pass over the PR queue in the next day or two; please post the numbers of PRs you want me to look at

[Zongyuan Liu]

I think several people, including me, would like to have the iapply PR, #80, merged. @Oliver Soeser Do you think it is okay to merge it as it is in its current state?

[Oliver Soeser]

Yes, the iapply PR is complete

[Shreyas Srinivas]

Mario Carneiro said:

there are a few people who can help with general review, and when that's done ping me and I will give a final review and merge. I benefit a lot from people letting me know that things are actually ready since they spend a while on the PR queue while they are still in development, and I don't have much dedicated time for maintaining iris-lean ATM. I will try to do a pass over the PR queue in the next day or two; please post the numbers of PRs you want me to look at

Whom should we ping?

[Mario Carneiro]

Either myself, or other iris-lean contributors such as Markus de Medeiros , Oliver Soeser and suhr

[Markus de Medeiros]

Anything with the awaiting review tag is good enough that it should be merged, to my eyes. I'll admit I don't know as much about the metaprogramming stuff (though I can definitely vouch for the iapply PR since I've been using it).

I've also not had a lot of time to spend on Iris-Lean. I'm focusing on iProp with the time that I have, though if you want me to look something over please ping me and I will do it.

[Oliver Soeser]

Same here, let me know if there's anything I can help review (metaprogramming stuff in particular)

[Zongyuan Liu]

@Mario Carneiro Did you have a chance to look at the iapply PR?

[Shreyas Srinivas]

Should we have more maintainers for iris-lean? If there are openings I would love to nominate @Markus de Medeiros, @Oliver Soeser, and @suhr

[Mario Carneiro]

I did look at the PR, but I did not get the time to properly review it as I intended

[Markus de Medeiros]

Shreyas Srinivas said:

Should we have more maintainers for iris-lean? If there are openings I would love to nominate Markus de Medeiros, Oliver Soeser, and suhr

I feel like I have done what I can for the PR's marked "ready for review"-- I do my best to learn from Mario's git diffs what makes a PR easy to review, which I think is the easiest way to reduce the time it takes for things to get merged.

[Markus de Medeiros]

It would be nice if we could have a "dev" branch or something so that people could use features awaiting final review without forking (for example, KLR depends on my personal fork at the moment!).

[Markus de Medeiros]

Not sure what this would look like though.

[Mario Carneiro]

you are welcome to do exactly that, have a series of PRs depending on a local fork

[Mario Carneiro]

you could push it to a branch on the main repo but I'm not sure that helps really

[Markus de Medeiros]

OK I think I will start doing this for the ready to review PR's! It will be nice for downstream dependencies, of which we have a few now, to be able to just require the Iris-Lean "experimental" branch without doing all the merging themselves.

One other thing--I'd like to start cutting releases for each Lean version (synchronized with the Lean releases). Just makes managing dependencies a little easier as well. This OK with you?

[Mario Carneiro]

yes, those are easy to merge

[Markus de Medeiros]

Good, thanks. I'll take care of this this evening.

[Shreyas Srinivas]

There is already a CI script for updating the toolchain every month in the main branch

[Markus de Medeiros]

Yes, definitely! It is useful.

[Markus de Medeiros]

I have been late on updating it

[Markus de Medeiros]

Okay, done. I have

• Cut releases for v4.21-v4.23
• Added an unstable tag, with all of the pending ready for review PR's (thanks everyone!) so that downstream projects can use the new features while they're being reviewed
• Updated the README to reflect the current status of the project (Mario I assume you might want to give this a look)

[Michael Sammler]

Should unstable be a tag or a branch? I would have expected it to be a branch that is updated when new ready to review PR's are added instead of a tag that cannot be updated.

[Markus de Medeiros]

I could go either way--a tag can be (force) updated, and using a single branch named "unstable" would also mean it would have to be frequently (force) updated. If the latter is better I'll switch!

[Mario Carneiro]

do you have PR links for the above?

[Mario Carneiro]

or branches on your repo

[Markus de Medeiros]

I'm not sure what you mean, everything I described is in the main Iris-Lean repo now

[Mario Carneiro]

oh I misunderstood. Still, links are good

[Markus de Medeiros]

Master and unstable have been updated to 4.24.0