Zulip Chat Archive

Stream: general

Topic: attribute documentation


view this post on Zulip Reid Barton (Aug 17 2020 at 13:53):

Would it be possible for attributes to be indexed by whatever handles the documentation search, so I can just use docs#norm_cast, for example?

view this post on Zulip Rob Lewis (Aug 17 2020 at 13:59):

Not really, since there can be name clashes, but attr#ext attr#norm_cast%20attributes

view this post on Zulip Rob Lewis (Aug 17 2020 at 14:00):

The doc entry for @[norm_cast] should be renamed anyway

view this post on Zulip Johan Commelin (Aug 17 2020 at 14:01):

That link is brok       en

view this post on Zulip Gabriel Ebner (Aug 17 2020 at 14:09):

(deleted)

view this post on Zulip Reid Barton (Aug 17 2020 at 14:10):

oh I didn't know attr#. But there's also the search box which could be more helpful.

view this post on Zulip Reid Barton (Aug 17 2020 at 14:10):

BTW, did you know we have a lemma called docs#ext?

view this post on Zulip Rob Lewis (Aug 17 2020 at 14:13):

attr# is new as of 13 minutes ago, but my point is docs# can't find both an attribute and a declaration name if they can overlap.

view this post on Zulip Rob Lewis (Aug 17 2020 at 14:14):

Johan Commelin said:

That link is brok       en

Yes, linkifiers with spaces don't work very well :/

view this post on Zulip Reid Barton (Aug 17 2020 at 14:16):

I would just ignore the possibility of overlap

view this post on Zulip Reid Barton (Aug 17 2020 at 14:16):

documentation search is pretty much a "do what I mean" domain

view this post on Zulip Rob Lewis (Aug 17 2020 at 14:18):

Are you talking about the search box on the web page or really the docs# here? The overlap isn't theoretical, see tactic#ring vs docs#ring or tactic#group vs docs#group etc.

view this post on Zulip Reid Barton (Aug 17 2020 at 14:19):

I don't know! Just make it better! :upside_down:

view this post on Zulip Reid Barton (Aug 17 2020 at 14:20):

Attribute overlap is more theoretical, right? As I recall you can actually get rather confusing behavior otherwise

view this post on Zulip Reid Barton (Aug 17 2020 at 14:21):

So specifically what triggered this was "ml norm_cast" in my search bar not doing anything useful

view this post on Zulip Rob Lewis (Aug 17 2020 at 14:21):

I mean, you just pointed out an example!

Reid Barton said:

BTW, did you know we have a lemma called docs#ext?

view this post on Zulip Rob Lewis (Aug 17 2020 at 14:21):

It feels really weird to make this work for attributes but not tactics though. Why should ml norm_cast send you to the attribute and not the tactic?

view this post on Zulip Kevin Buzzard (Aug 17 2020 at 14:21):

Reid is clearly just observing now that the problem is impossible to solve in some sense

view this post on Zulip Rob Lewis (Aug 17 2020 at 14:21):

ext is a declaration, a tactic, and an attribute, hah.


Last updated: May 15 2021 at 23:13 UTC