checking that mathbin and mathlib port capture decls

Stream: mathlib4

[Yakov Pechersky]

I'd like to build a linter/tool to make sure that during our port, we don't lose any mathlib3 decls we don't mean to. Ideally, this involves pointing the tool at a mathlib4 file, and a mathlib3port file, and making sure that all mathlib3 decl names are represented in both sets. That means reading in the decls from a module, un-aligning the identifier, and checking the difference of sets. I'm trying to learn the metaprogramming to make this possible. Is Std.Tactic.Lint.Frontend and Mathlib.Mathport.Rename the places to look for inspiration?

[Eric Wieser]

we don't lose any mathlib3 decls we don't mean to.

Maybe we already have this, but is there some equivalent to align that we could use to record "this has been deliberately removed"?

[Arien Malec]

there's the deprecated attribute, but nothing to mark "deliberately not ported" AFAIK.

[Scott Morrison]

We should add this, I agree.

[Scott Morrison]

Maybe just #noport?

[Scott Morrison]

Oh --- Mario already did this, see https://github.com/leanprover-community/mathlib4/pull/663