Autocompletion can't find `CategoryStruct`

Stream: lean4

[Jovan Gerbscheid]

I often rely on the autocompletion in https://leanprover-community.github.io/mathlib4_docs/ when I search for a lemma or definition. It works great, but every now and then it can be a bit annoying. A good example of this is that I searched for CategoryStruct, hoping to get the result CategoryTheory.CategoryStruct. But instead I only got results about CategoryTheory.StructuredArrow. Is this something that could be improved?

This seems to be the same autocompletion as the one in the Lean language server, which is why I put this in the lean4 channel.

[Marc Huisinga]

Jovan Gerbscheid said:

This seems to be the same autocompletion as the one in the Lean language server, which is why I put this in the lean4 channel.

How did you come to that conclusion?

[Jovan Gerbscheid]

I went in a Lean file and wrote

import Mathlib

#check CategoryStruct

And to me the autocomplete suggestions looked the same as the suggestions in the mathlib docs website.

[Marc Huisinga]

Auto-completion finds CategoryTheory.CategoryStruct as the first result in the MWE you posted, though?

[Jovan Gerbscheid]

afbeelding.png

Ah yes

[Marc Huisinga]

It's the first result in your screenshot

[Jovan Gerbscheid]

Oops. I was thrown off by the highlighting

[Jovan Gerbscheid]

So I guess then my question is, can the website use the same autocompletion as the Lean server?

[Henrik Böving]

At the time when this was written the precise completion algorithm of the server used to be far more computationally intense than today so we implemented a differen one that could be used for interactive web applications with less computational resources and higher interactivity requirements. I think nowadays we could actually port what the LSP is now using to doc-gen, I would be happy to review a PR for that.