Zulip Chat Archive

Stream: mathlib4

Topic: Documentation on lint overrides?


Arien Malec (Nov 18 2022 at 15:44):

Is there documentation on lint overrides?

I have a PR that needs to allow deprecated references & sorrys (because I'm porting to expose code that's deprecated to Std implementations), but don't know the magic invocations needed.

Arien Malec (Nov 18 2022 at 21:11):

Ping?

Jireh Loreaux (Nov 18 2022 at 21:15):

section
set_option linter.deprecated false

-- deprecated code

end

However, I highly doubt you are actually going to be allowed sorrys. Are you sure the approach you're taking regarding porting these is the right one?

Arien Malec (Nov 18 2022 at 21:54):

Thanks -- yes, was requested by @Mario Carneiro to preserve theorems to backport to Std4

Mario Carneiro (Nov 18 2022 at 21:56):

the sorrys are pending migration to Std. You should use this to placate CI:

-- FIXME: remove this when the sorries are gone
set_option warningAsError false

Last updated: Dec 20 2023 at 11:08 UTC