Andreas Abel

> Imported modules might belong to other libraries with other `.agda-lib` files. Yes, but how do you find them other than via the current include paths? So, you mean that...

_My teacher used to say: "don't just toss me a crumb" encouraging us to elaborate our arguments._ Please explain your scenario in more detail, so that we can make progress...

Converted to draft. Please switch it back once it is ready for review.

@plt-amy : You asked in our meeting whether you could add descriptions to the labels. That's not a mandate to single-handedly rework the label system. Please coordinate changes with me.

Red color is to alert, I think we are rather consistent with that. Dark green is to either green light for contribution (`help wanted`, `PR welcome`). Light green is for...

Yes, these prefixes are good when they suggest themselves. We shouldn't make this a _must_ though, since all categorizations are incomplete in the real world...

Thanks, @m0rphism, for the pointer. Would you be able to turn this into a pull request? On the Agda side, the new functionality would have to be added to `Agda.Interaction.InteractionTop`.

@plt-amy : Currently this issue is both labeled __language change__ (suggesting there should be a changelog entry explaining the change) and __regression on master__ (suggesting it should not be in...

Thanks for the clarification! I think we can omit this issue from the changelog then.

Turns out that its PR #6219 already is mentioned in the changelog.