Real Closed Field

Stream: PR reviews

[Artie Khovanov]

This thread will track, and solicit reviews for, PRs upstreaming my formalisation of real closed fields.

[Artie Khovanov]

#33697 - Definition of real closed field

[Artie Khovanov]

#33698 - Characteristic of semireal ring

[Artie Khovanov]

#33699 - Semireal definition lemmas

[Violeta Hernández]

Left reviews on all three :slight_smile:

[Artie Khovanov]

#33944 - Definition of formally real field

[Artie Khovanov]

#33942 - Support of a submonoid (part 1 of positive cone refactor)

[Artie Khovanov]

#34069 - Algebra is ordered iff inclusion is monotone

[Artie Khovanov]

#33697 has been assigned to @Violeta Hernández, who I do not believe has the power to put it on the maintainer queue. How should review proceed?

[Violeta Hernández]

(I approve of the PR)

[Snir Broshi]

I think you can unassign then the PR will be auto-assigned after some time

[Moritz Doll]

Violeta Hernández said:

(I approve of the PR)

You can approve of a PR in a comment (there is a button for that) and that is a good indication for maintainers that somebody has looked over it.
As for the PR: I think the module doc-string should at least explain what a real closed field is, at the moment it says nothing really.

[Kim Morrison]

Yes, teaching reviewers how to click the Github "approve" button is super helpful. :-)

@Bryan Gin-ge Chen, can we make sure the queueboard reflects Github approvals?

[Bryan Gin-ge Chen]

It's possible! But we haven't been scraping approval data so far so it'll take some time to incorporate.

[Kim Morrison]

@Artie Khovanov, it looks like CI is in a weird state. Perhaps merging master will resolve it.

[Artie Khovanov]

Kim Morrison said:

Yes, teaching reviewers how to click the Github "approve" button is super helpful. :-)

Bryan Gin-ge Chen, can we make sure the queueboard reflects Github approvals?

I agree but in this case Violeta had already done this. They were just assigned to the PR for some weird reason.

[Ruben Van de Velde]

Dagur Asgeirsson assigned it to Violeta Hernández, I assume because she'd already been reviewing

[Artie Khovanov]

I see
That's confusing to me because then like
How is the PR meant to be merged once Violeta approves it? Am I supposed to unassign them?

[Kim Morrison]

I don't think unassigning is necessary. The usual process of waiting for someone to get it to, plus posting here in PR reviews to ask for attention.

[Artie Khovanov]

I'm still confused - my understanding was that the point of the bot assigning reviewers was so they could use maintainer-merge once review converged. Indeed that's been the workflow on previous PRs where I didn't want to bother anybody. If a non-reviewer is assigned, then there is no longer that delegated responsibility.

[Ruben Van de Velde]

The assignment just indicates that this person will look at it. Everyone is welcome to do reviews, even if they aren't assigned as reviewers

[Artie Khovanov]

I'm talking about the converse responsibility

[Artie Khovanov]

Sorry I feel like I'm talking past everyone else, I'm genuinely just confused

[Ruben Van de Velde]

I don't understand what you don't understand :)

[Violeta Hernández]

i don't think assignment confers any formal responsibility? it's just a "this person should/will take a look"

[Ruben Van de Velde]

Exact

[Violeta Hernández]

I sometimes assign myself on PRs as a way to say "don't worry, someone is already reviewing this"

[Artie Khovanov]

oh right I see
sorry I thought there was a level of (informal) responsibility assignment for the people with the power to do maintainer merges
the bot is just a system to make sure someone looks
I'll reassign you V

[Artie Khovanov]

Could I get a review on #33944 and #34069? They've both been sitting idle for a while now.

[Violeta Hernández]

You have my approval on #33944

[Violeta Hernández]

I'm not very familiar with the math on #34069, sorry