Zulip Chat Archive

Stream: general

Topic: Linter for doc strings

Riccardo Brasca (Mar 01 2022 at 17:13):

Is it possible to have a linter that checks the names in the doc strings? For example the beginning of finite_dimensional is full of theorems names that are not hyperlinks. More seriously, I am sure there are quite a lot of examples where the actual theorem doesn't exist anymore.

Gabriel Ebner (Mar 01 2022 at 17:17):

The hard part here is figuring out whether it's a misspelled declaration name or just a regular word (since there's no special syntax for declaration links, the documentation generator just looks for words that happen to be declaration names and then linkifies them).

Eric Wieser (Mar 01 2022 at 17:17):

I think we might need a more structured markup language than markdown if we want to go down this route

Gabriel Ebner (Mar 01 2022 at 17:17):

We might think about adopting the doc-gen4 convention for declaration links, which is this:
[additive commutative monoids](##add_comm_monoid)

Eric Wieser (Mar 01 2022 at 17:18):

[##add_comm_monoid][] is valid markdown for a link to ##add_comm_monoid, right?

Gabriel Ebner (Mar 01 2022 at 17:18):

I don't know. If it is a valid markdown link, then it should be supported in doc-gen4.

Eric Wieser (Mar 01 2022 at 17:19):

We could probably customize its expansion to [`add_comm_monoid`][##add_comm_monoid]

Eric Wieser (Mar 01 2022 at 17:20):

(I think by default it means [##add_comm_monoid][##add_comm_monoid])

Riccardo Brasca (Mar 01 2022 at 17:21):

I have no idea how this works, so I apologize if what I am saying is nonsense. In practice if the name I write between `` exists, an hyperlink is created, and nothing happens if the name doesn't exist, right? It would be nice if the linter tells me "hey, there will be no hyperlink here!".

Eric Wieser (Mar 01 2022 at 17:23):

Right, but what about when you write `x + y` ?

Eric Wieser (Mar 01 2022 at 17:24):

I would guess less than half of the ` use in docstrings refers to lemma names

Riccardo Brasca (Mar 01 2022 at 17:24):

Ah, you're right.

Riccardo Brasca (Mar 01 2022 at 17:28):

Maybe check only the "words" with more then, say, five characters? There will still be false positives/negatives, but much less I think. (So it should only be a warning, or something similar).

Johan Commelin (Mar 01 2022 at 18:07):

We could check for

* `i_am_the_start_of_a_bullet_point` is the main theorem of unordered lists

Damiano Testa (Mar 01 2022 at 19:49):

In this line, at least one underscore and no spaces between ticks is likely a hit!

Eric Wieser (Mar 01 2022 at 20:00):

* `i_am_the_start_of_bullet n` is also fairly common

Mario Carneiro (Mar 01 2022 at 23:22):

rustdoc uses [`foo`] to generate links to entities. This isn't quite valid markdown (it will generate literal brackets if used by a non-lean-markdown aware parser) but we can intercept it in docgen and vscode hovers at least

Mario Carneiro (Mar 01 2022 at 23:23):

I'm not a fan of autolinkifying these, there is no declaration of intent that way

Eric Wieser (Mar 01 2022 at 23:27):

[`foo`][] is valid markdown though, so might be better - it works as long as the link lookup dictionary (the one we already use for bibtex references) knows how to turn backticks into a url

Last updated: Dec 20 2023 at 11:08 UTC