extend_docs persistence issue

Stream: mathlib4

[Thomas Murrills]

I noticed that extend_docs doesn't necessarily persist a docstring change across imports!

This is because of extension trickiness: the docstring extension maintains a List (Name × String) alongside a NameMap String; the NameMap is used for state, while the List is used for exports. addDocString calls out to a function which implicitly assumes that no docstring is being added twice, and simply prepends the new entry to the List, regardless of whether the name already appears in a pair there; a qsort with respect to the name that is used during serialization then might rearrange the entries. After import, when we conduct binary search through the entries associated with the module to retrieve the docstring, we might land on the wrong one.

Since this bug sensitive to the vagaries of qsort and binSearch, it doesn't always happen. For example, foo is necessary in the following:

Mathlib.Tactic.Test:

import Mathlib.Tactic.ExtendDoc

/-- A docstring. -/
def foo := 5

@[inherit_doc foo]
def bar := 5

extend_docs bar
  before "Sorry I'm late to the docstring—what'd I miss?"

Other file:

import Mathlib.Tactic.Test

#check bar -- Hover: "A docstring."
/- Should be:
Sorry I'm late to the docstring—what'd I miss?

A docstring. -/

[Thomas Murrills]

PR: #17043

[Damiano Testa]

Thanks for digging into this!

[Damiano Testa]

When i wrote extend_docs, my "real" motivation was to be able to extend the docs of rw by adding to it the docs of rewrite. However, I found out that I was not able to extend the docs of a declaration that was not in the present file.

[Damiano Testa]

Do you think that you could implement that as a modification of what you are doing now?

[Damiano Testa]

E.g., can you extend_docs for a declaration that is in the environment, but not in the current file?

[Thomas Murrills]

Sadly I don't think so—when a declaration is from another module, we find its docstring via binary search through the qsorted array of entries associated with that module, without even constructing the NameMap. (I'm now realizing my explanation was slightly wrong on the "reconstruction of the NameMap" point, by the way—that never happens! I've now edited the original message.)

[Damiano Testa]

Ok, thanks for the explanation, though!

[Thomas Murrills]

I'm late to the party, but I'm seeing some code about "tactic extensions" and "tactic alternatives" which seems to have landed relatively recently, though. Maybe that's a path to an ultimate solution somehow for rw? :eyes: (I think this is lean4#4490)