PANIC at Lean.MapDeclarationExtension.insert

Stream: mathlib4

[Eric Wieser]

In #10962 with extend_docs I'm getting

PANIC at Lean.MapDeclarationExtension.insert Lean.Environment:607:2: assertion violation: env.getModuleIdxFor? declName |>.isNone -- See comment at `MapDeclarationExtension`

followed by a long backtrace that goes through the compiled version of Lean.addDocstring

[Richard Copley]

It looks like extend_docs is otherwise unused, so if a change elsewhere broke it, that could easily have gone unnoticed.
Can you just change the original docstring?

[Eric Wieser]

This seems to be a problem with add_decl_doc

[Eric Wieser]

I guess this is

@Mario Carneiro said:

Nope, it panics if you call addDocString on a declaration from another module

though I'm puzzled why extend_docs even exists if this is the case

[Eric Wieser]

lean4#3497

[Damiano Testa]

I'm not at a computer, but extend_docs works on declarations that are introduced in the current file.

I think that to make it reassign a pre-existing doc-string was hard/hacky.

A typical usage is to add extend_docs in combination with inherit_docs.

My initial push to introduce extend_docs was indeed to modify docs, e.g. of rw, but in the process it transpired that this was not going to work.

See for instance

https://github.com/leanprover-community/mathlib4/pull/7446#discussion_r1342010750

and

https://github.com/leanprover/lean4/issues/2622