[buster]

Which is not runnable in the first place. Interesting though, as this shows exactly the problem. It looks legit, but it's some generated fake text.

[ok123456]

It tends to invent whole fake packages.

[dunham]

Yup, I got some nice documentation (minor syntax error) for a Http package in Lean that doesn't exist. I asked about Lean4 and it helpfully explained that the non-existent package had moved from Lean to Std.