lake warnings about std

Stream: std4

[Scott Morrison]

@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]

use where instead

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

#eval Lean.versionString returns 4.2.0-rc4 as expected

[Mario Carneiro]

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]

I can see the deprecation warning on lean4 master

[Mario Carneiro]

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]

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

[Scott Morrison]

Yes, rc4 is rc3 + 6c206737370bc41139bb60100d0e69437d39c84d cherry picked.

[Scott Morrison]

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

[Mario Carneiro]

In that case, why is anyone getting deprecation warnings?

[Mario Carneiro]

It hasn't landed yet

[Mario Carneiro]

is this an issue in the PR release branches?

[Scott Morrison]

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]

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