How can I exclude X if I'm told to consider excluding it?

Stream: lean4

[Geoffrey Irving]

Lean v4.11.0-rc2 has error messages of the form

included section variable '[CompleteSpace E]' is not used in 'AnalyticAt.log', consider excluding it

But it doesn't give any hints as to how I should exclude it. From some searching I think I'm supposed to do omit [CompleteSpace E] in, but I think I need to import some particular file to make that work, and searching for omit in mathlib docs doesn't work.

[Eric Wieser]

I think omit doesn't exist yet in the version of Lean mathlib is on; you have to instead remove the local section variable, and add it just on the proofs that need it

[Geoffrey Irving]

Even though I'm on master?

[Geoffrey Irving]

I updated to master an hour ago.

[Eric Wieser]

Yes, you need to be using a version from the possible future where lean4#5000 is merged

[Geoffrey Irving]

Oh, sorry: I misread. Sounds good, I'll rephase to not imply those.