feat(tactic): make docstrings of imported modules accessible

[Vtec234]

Changes the semantics of module_doc_strings to contain a list of (some filename, top-level-docstring) pairs, plus a (none, top-level-docstring) for the current module. If a single module contains multiple top-level docstrings, they're concatenated with newlines (but I could make it a list like before if people want). Declaration docstrings are no longer present in the output, since they're accessible via doc_string anyway.

CC @robertylewis

[robertylewis]

Cool, thanks!

If a single module contains multiple top-level docstrings, they're concatenated with newlines (but I could make it a list like before if people want).

I think a list would be better. No reason to throw away information about how they're separated. Even better: would it be possible to pair each docstring with its location in the file?

[robertylewis]

The motivation there is that when we're generating docs, it would be nice to have some kind of sectioning. Module docs in the middle of the file would be the easiest way to do this. But we need to know where to put them in the generated docs.

[Vtec234]

It's now a list of (source filename, [(position info, doc string)]).

[Vtec234]

Here is a possible log entry for this:

• Changes the semantics of tactic.module_doc_strings to return a list of module-level documentation entries for each imported file, and not just the currently open one.

[Vtec234]

New version adds olean_doc_strings and reimplements module_doc_strings on top of that.

[Vtec234]

Hm, that CI failure is really quite mysterious. I have no clue why this PR would change the column number printed in an unrelated test, and only on MacOS of all things.

[bryangingechen]

It's yet another instance of #72. It should go away if the job is re-run. @cipher1024

[robertylewis]

I haven't pushed it yet (still needs some cleanup), but I updated my doc generation tool to use this. Worked exactly as expected. Thanks again!