Linter for `deprecated (since := _)`

Stream: mathlib4

[Yury G. Kudryashov]

In #13678, I started to write a linter (not tested yet) that should fail on @[deprecated] without since := . I have 3 questions:

• do you think that we should enforce this (by a linter like this one)?
• what's a better way to deal with "discard the case an Option is none"? I do match but I would prefer to write a line that discard the none case, then continue with the some case.
• how do I enforce the YYYY-MM-DD format?

[Thomas Murrills]

Re: second bullet, are you looking for something like let some info := (…) | return none?

[Adam Topaz]

For the date format, you could try to parse such a date (e.g. with parsec) and throw an error on failure

[Yury G. Kudryashov]

Where do I read about parsec?

[Adam Topaz]

docs#Lean.Parsec

[Adam Topaz]

I’m not sure how much documentation we have. But most of the docs about the Haskell implementation should translate

[Yury G. Kudryashov]

Thank you!

[Damiano Testa]

I had written a (partial) check for something that looks like a date here, in case it is useful.

[Yury G. Kudryashov]

I don't think I have access to TSyntax at this stage.

[Damiano Testa]

Maybe docs#String.toNat? can be useful?

[Yury G. Kudryashov]

#13723 and #13839 add since := dates to all @[deprecated], then #13678 adds a linter.