superfluous proof_1 items in docgen

Stream: metaprogramming / tactics

[Tony Beta Lambda]

There are many "blah.proof_1" items in the mathlib doc, such as this one. I believe they are generated by to_additive. I consider this a bug since apparently these come from conGen.proof_1 during the to_additive translation process, but conGen.proof_1 itself is hidden in the docs. Can someone fix it?

[Floris van Doorn]

@Henrik Böving I think this would be fixed by using docs#Lean.Name.isBlackListed instead of DocGen4.Process.DocInfo.isBlackListed.

[Floris van Doorn]

(or by running Lean.Name.isBlackListed after a successful findDeclarationRanges? if that's also something you need to test for)

[Floris van Doorn]

I could also independently avoid giving these auxiliary declarations declaration ranges, if you think that's better. Presumably that is how conGen.proof_1 is filtered out?

[Henrik Böving]

The implementations of those two functions look almost the same?

[Henrik Böving]

given that they were both copied from the LSP that is to be expected

[Henrik Böving]

Yeah I don't see how using that function would fix anything. Besides the fact that its in mathlib so it would have to be copied over yet again.

[Tony Beta Lambda]

Floris van Doorn said:

I could also independently avoid giving these auxiliary declarations declaration ranges, if you think that's better. Presumably that is how conGen.proof_1 is filtered out?

Yes, I think that's how they are filtered out. It might make sense to set the declaration range of translated declarations to none whenever the original declaration has none?

[Floris van Doorn]

Henrik Böving said:

The implementations of those two functions look almost the same?

Lean.Name.isBlackListed uses docs#Lean.Name.isInternalDetail which precisely filters out the proofs we're talking about here. The latter is in core, so maybe you can just modify your version to include that check?

[Floris van Doorn]

Tony Beta Lambda said:

Yes, I think that's how they are filtered out. It might make sense to set the declaration range of translated declarations to none whenever the original declaration has none?

I have to double check whether declaration ranges are added before attribute application. If so, that should be easy to do.

[Henrik Böving]

Fixed