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:
- I'm not getting the warning locally (on rc4), why is that?
- 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