https://github.com/dupuisf/BibtexQuery/pull/20

Stream: nightly-testing

[Kim Morrison]

@Frédéric Dupuis, could you merge this PR asap?

It is blocking the release of doc-gen4 for v4.17.0-rc1 (and thence blocking getting Mathlib onto v4.17.0-rc1).

[Kim Morrison]

Separately from that, it would be great if you could give the leanprover-community "team" called lean-release-managers sufficients rights to this repo so that we can merge PRs like this ourselves.

[Kim Morrison]

(Alternatively, we could consider moving BibtexQuery to leanprover-community)

[Kim Morrison]

In the meantime, I will have doc-gen4 depend on my fork.

[Frédéric Dupuis]

No problem, I should be able to do it in a few hours.

[Frédéric Dupuis]

Kim Morrison said:

(Alternatively, we could consider moving BibtexQuery to leanprover-community)

I would be interested in this option. Perhaps we could also decouple the command-line utility from the library, as far as I can tell, only the library is needed in doc-gen, right?

[Kim Morrison]

That seems reasonable. I propose:

• grant lean-release-managers the maintain rights, so we can merge during the release checklist
• split the library into the two components, at your leisure
• (after, or at the same time), we get approval from mathlib-maintainers / mathlib-admin (I'm not quite sure where the delegation lies! :-) for migrating the library part into leanprover-community.
• we do the move

(The usual setup for moving things into leanprover-community applies: you'd still be the maintainer, but ultimately the mathlib-admin team has final say in the unlikely event something goes wrong.)

[Frédéric Dupuis]

I don't seem to be able to give access rights to a team on github. Instead of a "Collaborators and teams" tab, I only have "Collaborators" and it only lets me add individuals. Is this because I have a free barebones github account ?

[Kim Morrison]

Ah my mistake, those teams are only usable within an organization. Maybe just add me and Johan for now?

[Frédéric Dupuis]

You should both have received invitations, let me know if this somehow didn't work.

[Kim Morrison]

Looks good. The "merge PR" button is there, although I didn't actually click it.

[Kim Morrison]

@François G. Dorais could you give both me and @Johan Commelin merge rights at UnicodeBasic, so that we can e.g. merge things like https://github.com/fgdorais/lean4-unicode-basic/pull/60 during the release process. It is really helpful if this doesn't have to happen asynchronously. (Tonight we will just proceed by releasing doc-gen4 depending on Johan's branch.)

[Kim Morrison]

Would it also be possible to turn on some CI (e.g. using lean-action)

[François G. Dorais]

The update script runs every 24 hours, I could accelerate that if you want. I could also try to figure out how give you guys a manual trigger.

[Kim Morrison]

Yes, that's too asynchronous, the release process touches many repos and we need to be able to blast through.

[François G. Dorais]

Well, we have some time to work things out. Let's find a time to talk about it.