Skip to content

Conversation

@github-actions
Copy link
Contributor

Automated changes by create-pull-request GitHub action

@lgoettgens lgoettgens marked this pull request as draft November 12, 2025 11:17
Comment on lines +66 to +74
### Tropical Geometry

### Changes related to the package GAP

### Changes related to the package Hecke

### Changes related to the package Singular
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

why are there empty headers here without any content?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This happens when a PR was tagged with a topic label, but not with a type label. The script finds non zero number of things under tropical geometry, so generates a heading for it. But it never finds a type label, so, neither the secondary heading, nor the PR itself is printed here. They end up in the TODO section. IMO, leaving it like this might be fine, so, we know where to (manually) insert something.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'd say it's better then to move these things with "missing labels into the right topic section, but in subsection #### TODO: missing type label or so

CHANGELOG.md Outdated

- [#5267](https://github.com/oscar-system/Oscar.jl/pull/5267) Add `order_bound` keyword argument to `subgroup_classes`
- [#5284](https://github.com/oscar-system/Oscar.jl/pull/5284) Implement chamber counting algorithm for toric line bundles
- [#5288](https://github.com/oscar-system/Oscar.jl/pull/5288) Add `p_rump` for `GAPGroup` and extend `torsion_subgroup` for `GAPGroup` and `WeylGroup`
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This has a "topic: groups" label, but is not sorted into the appropriate section above

Copy link
Member

@aaruni96 aaruni96 Nov 12, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This should be fixed whenever #5279 is merged


Maybe it was unwise to add patches for this into that PR, from a keeping PRs on topic point of view, but its currently probably the fastest way of patching this.

@joschmitt
Copy link
Member

Looking at some of the entries in the "TODO" categories, I realize that I don't know how many or what labels a pull request needs to make the script happy.
My impression is:

  1. A release notes: ... label
  2. A topic: ... label
  3. Some other label like enhancement but I don't know what exactly falls into this category.

Is this correct? Is it written down somewhere? I so far I followed the two-label-approach from https://docs.oscar-system.org/stable/DeveloperDocumentation/changelog/ but apparently that's not enough anymore?

@lgoettgens
Copy link
Member

Looking at some of the entries in the "TODO" categories, I realize that I don't know how many or what labels a pull request needs to make the script happy. My impression is:

  1. A release notes: ... label
  2. A topic: ... label
  3. Some other label like enhancement but I don't know what exactly falls into this category.

Is this correct? Is it written down somewhere? I so far I followed the two-label-approach from https://docs.oscar-system.org/stable/DeveloperDocumentation/changelog/ but apparently that's not enough anymore?

As I noted in #5544 (comment), there is currently some issue with how these things are put into categories. I would assume that this also affects your examples

@aaruni96
Copy link
Member

aaruni96 commented Nov 12, 2025

apparently that's not enough anymore?

Your impression should be correct. Can you look at the new changelog ( 06019bf ), and if there is still unexpected behaviour, point out the exact PRs which are miscategorised ?

Some other label like enhancement but I don't know what exactly falls into this category.

The two kinds of labels (topics, and types) have been expanded upon, but this is still in the dev docs, not yet in stable.

https://docs.oscar-system.org/dev/DeveloperDocumentation/changelog/#Multi-level-topics


### **TODO** insufficient labels for automatic classification

The following PRs only have a topic label assigned to them, not a PR type. Either assign a type label to them (e.g., `enhancement`), or manually move them to the general section of the topic section in the changelog.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you instead put the into their respective general section, but with a todo note each? I think it is easier to just manually remove todo notes than moving things around in this file.
I am asking because I see a bunch of things here, that don't fit into any subsection, e.g. updates of dependencies

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Day's event have started. I shall look at it again today at night.

@joschmitt
Copy link
Member

apparently that's not enough anymore?

Your impression should be correct. Can you look at the new changelog ( 06019bf ), and if there is still unexpected behaviour, point out the exact PRs which are miscategorised ?

Some other label like enhancement but I don't know what exactly falls into this category.

The two kinds of labels (topics, and types) have been expanded upon, but this is still in the dev docs, not yet in stable.

https://docs.oscar-system.org/dev/DeveloperDocumentation/changelog/#Multi-level-topics

Okay, sorry, I did not look at the most recent documentation. So the gist is that every pull request now needs three labels? And wouldn't it be good to have all the "type" labels start with "type:" and possibly all have the same colour?

@fingolfin
Copy link
Member

Okay, sorry, I did not look at the most recent documentation. So the gist is that every pull request now needs three labels?

Yes that's how it has been since we introduced this system. (Well, you can get away with one label if it is release notes: not needed ;-) but in general: three)

And wouldn't it be good to have all the "type" labels start with "type:" and possibly all have the same colour?

I don't want this for the colors: both "bug" and "enhancement" are types, but one is red and the other not, and I'd like to stay it that way.

Wouldn't mind for them to share a common prefix, though. But perhaps we can not use "type" but rather something else, like "kind" or "category" -- the word "type" already is used heavily in our code and I'd like to avoid yet another overload of the meaning.

Regarding the topics, note that they have either prefix topic: or package:. But I think that's manageable. Then there is release notes: highlight which is a bit of an odd one; and so I also kinda think it is OK to leave it like that. It is really meant in addition to whatever other labels you have, to mark select PRs / new features that we want to highlight.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants