Zulip Chat Archive

Stream: std4

Topic: lake warnings about std


Scott Morrison (Oct 22 2023 at 00:13):

@Mac Malone, lake is currently bugging every Lean user about

warning: ./lake-packages/std: `:=` syntax for configurations has been deprecated

Could you please tell me how to fix this?

Mario Carneiro (Oct 22 2023 at 00:13):

use where instead

Mario Carneiro (Oct 22 2023 at 00:13):

oh, it's warning downstream users about std? That's bad

Mario Carneiro (Oct 22 2023 at 00:14):

I don't get any such warning inside std4's lakefile.lean

Mario Carneiro (Oct 22 2023 at 00:15):

I knew this was coming but the deprecation hasn't landed yet, right?

Mario Carneiro (Oct 22 2023 at 00:21):

You should now be able to bump any projects to avoid the warning. But:

  1. I'm not getting the warning locally (on rc4), why is that?
  2. We need something like rust's cap-lints which prevents warnings in dependencies from being reported in downstream projects

Mac Malone (Oct 22 2023 at 00:33):

Mario Carneiro said:

I don't get any such warning inside std4's lakefile.lean

That is weird and unexpected. I wonder why?

Mario Carneiro (Oct 22 2023 at 00:37):

#eval Lean.versionString returns 4.2.0-rc4 as expected

Mario Carneiro (Oct 22 2023 at 00:40):

I ctrl-clicked my way to ~/.elan/toolchains/leanprover--lean4---v4.2.0-rc4/src/lean/lake/Lake/DSL/DeclUtil.lean and it indeed has no deprecation warning in it

Mario Carneiro (Oct 22 2023 at 00:40):

I can see the deprecation warning on lean4 master

Mario Carneiro (Oct 22 2023 at 00:59):

Oh, something seems to be a bit weird about the rc4 release (or possibly the release process in general). The commit used for constructing the release was 819b5eac, but this is not a commit on the master branch, and there is another commit 6c20673 with the same commit title, implying that some kind of rebase happened. 819b5eac does not have the deprecation warning but 6c20673 does.

Mario Carneiro (Oct 22 2023 at 01:00):

@Scott Morrison do you know how this release was cut? Did you cherry pick the bugfix onto rc3?

Scott Morrison (Oct 22 2023 at 01:22):

Yes, rc4 is rc3 + 6c206737370bc41139bb60100d0e69437d39c84d cherry picked.

Scott Morrison (Oct 22 2023 at 01:23):

Sorry, I should get in the habit of describing exactly how the releases are constructed in the release notes.

Mario Carneiro (Oct 22 2023 at 01:25):

In that case, why is anyone getting deprecation warnings?

Mario Carneiro (Oct 22 2023 at 01:25):

It hasn't landed yet

Mario Carneiro (Oct 22 2023 at 01:26):

is this an issue in the PR release branches?

Scott Morrison (Oct 22 2023 at 21:45):

Oh! I spent a lot of time yesterday on the nightly-testing and lean-pr-testing-NNNN branches. I must have only been seeing the warning there --- where the deprecation has landed already.

Scott Morrison (Oct 22 2023 at 21:46):

Sorry for the confusion there. I guess it had a good outcome: we changed std before it affected anyone else. :-)


Last updated: Dec 20 2023 at 11:08 UTC