Zulip Chat Archive

Stream: mathlib4

Topic: bump to v4.1.0-rc1

Scott Morrison (Sep 15 2023 at 06:03):

@Eric Wieser, is there a matching Mathlib bump for https://github.com/leanprover/std4/pull/187?

Scott Morrison (Sep 15 2023 at 06:04):

It is preventing the bump to v4.1.0-rc1. #7174

Mario Carneiro (Sep 15 2023 at 06:10):

I don't think there is, it was merged shortly after the issues in std were fixed

Mario Carneiro (Sep 15 2023 at 06:12):

If only we had a tool to help us rename things...

Scott Morrison (Sep 15 2023 at 06:14):

Okay, I'm doing it now, but if anyone wants to take over. :-)

Scott Morrison (Sep 15 2023 at 06:27):

Mario Carneiro said:

If only we had a tool to help us rename things...

I added a supportive emoji. :-)

Scott Morrison (Sep 15 2023 at 06:56):

Okay, I think I caught them all.

If someone could take a quick look at the diff https://github.com/leanprover-community/mathlib4/pull/7174/commits/64d6d07ee18163627c8f517eb31455411921c5ac, after that #7174 can be merged.

Johan Commelin (Sep 15 2023 at 07:29):

I took a look. LGTM. Gave you a bors d+.

Eric Wieser (Sep 15 2023 at 16:35):

We reverted this in #7198 because it failed linting (and also disabled linting which is why we didn't notice!)

Matthew Ballard (Sep 15 2023 at 16:56):

Slick.

Scott Morrison (Sep 17 2023 at 03:56):

Just back at the computer. Is there discussion anywhere yet of how/why it disabled linting?

Scott Morrison (Sep 17 2023 at 03:57):

It looks like perhaps it ran the Std linter but not the Mathlib linter.

Jireh Loreaux (Sep 17 2023 at 04:01):

I think see #7199. But because the linter didn't run there were a lot of lint issues from the bump.

Mario Carneiro (Sep 17 2023 at 05:01):

There are two programs called runLinter, and they are basically copies. I recommend deleting the mathlib runLinter and instead running the std runLinter with the right settings to check mathlib

Scott Morrison (Sep 17 2023 at 05:43):

I made https://github.com/leanprover/lean4/issues/2548 to note the change in behaviour in Lake.

Scott Morrison (Sep 17 2023 at 05:44):

I suggest in #7216 (the 2nd attempt to bump to v4.1.0-rc1) we just do the minimal thing, of renaming (in Mathlib) runLinter to runMathlibLinter, and then someone can unify them in a subsequent PR.

Eric Wieser (Sep 17 2023 at 08:44):

Scott, as of my PR you just merged, CI will run the std linter script against mathlib, so there is no need for runMathlibLinter

Scott Morrison (Sep 17 2023 at 08:54):

Unfortunately it didn't work. It reported errors in Std.

Scott Morrison (Sep 17 2023 at 08:55):

Problem is https://github.com/leanprover/std4/blob/main/scripts/runLinter.lean#L44

Scott Morrison (Sep 17 2023 at 08:56):

I propose we unify the linters after the bump.

Eric Wieser (Sep 17 2023 at 09:19):

Ah, nice find

Eric Wieser (Sep 17 2023 at 09:21):

Is there a lake bug here that there was no diagnostic when there were duplicate runLinter targets?

Scott Morrison (Sep 17 2023 at 11:26):

Well, leaving aside whether it is a bug or feature, a question about behaviour with duplicate targets is at https://github.com/leanprover/lean4/issues/2548.

Last updated: Dec 20 2023 at 11:08 UTC