Zulip Chat Archive

Stream: mathlib4

Topic: Emitting warnings in mathlib3 CI

Eric Wieser (Dec 09 2022 at 14:02):

I've made a PR at #17867 which adds a warning annotation on files in the diff which are ported. Does it look good? We can always improve upon it later, but the sooner we have it merged the sooner we can start catching this type of thing.

It's currently marked not-ready-for-merge because it contains a garbage change to one such file in order to test the PR. I'll remove that once it has a bors d+.

Heather Macbeth (Dec 09 2022 at 14:03):

This is great!

Eric Wieser (Dec 09 2022 at 18:34):

Who would be a good person to review it? I think it would be to get something like this merged ASAP to avoid further divergence

Johan Commelin (Dec 09 2022 at 18:36):

LGTM!

Eric Wieser (Dec 09 2022 at 18:55):

Is that a bors d+?

Johan Commelin (Dec 09 2022 at 18:57):

I guess so

Eric Wieser (Dec 09 2022 at 18:58):

Or we could wait for @Scott Morrison to take a look

Scott Morrison (Dec 09 2022 at 18:59):

Sorry, low bandwidth for 36 hours, so please proceed.

Last updated: Dec 20 2023 at 11:08 UTC