docs# is slow

Stream: lean4

[Mario Carneiro]

I have often seen pauses of multiple seconds on a white screen before pages like docs#Nat or docs#AddMonoidAlgebra.domCongr_single show up. What are the possible reasons behind this? How does this link work in the first place?

[Mario Carneiro]

cc: @Henrik Böving

[Henrik Böving]

It forwards to the page generated by this snippet: https://github.com/leanprover/doc-gen4/blob/main/DocGen4/Output/Find.lean#L9 whose main job it is to call this javascript file: https://github.com/leanprover/doc-gen4/blob/main/static/find/find.js so the things it should be spending time on are:

1. Downloading declaration-data.bmp if it is not in cache
2. parsing the JSON
3. searching for the pattern

[Mario Carneiro]

I see, so any docs link has to download all of mathlib?

[Henrik Böving]

Not all of mathlib. I did reduce the decl data quite a lot while doing some optimization but it is still significant yes.

Note that if you open these links in chrome they are basically instant, it is only slow in firefox for me. But I (as so often) know far too little about webdev to be able to make a guess as to why that is the case.

[Mario Carneiro]

Testing the links again, I seem to consistently get a pause of about 1 second, even after the data file is presumably in cache (on FF)

[Mario Carneiro]

possibly also a useful data point, https://leanprover-community.github.io/mathlib4_docs/find/ also takes about a second to redirect to the 404

[Eric Wieser]

For lean 3 we generated a stub page for every definition, making the redirection pretty instantaneous

[Eric Wieser]

This was also great for Twitter, since the stub page had meta tags containing the docs for just that declaration

[Eric Rodriguez]

It's not slow in Safari too. Seems to be a firefox thing.

[Mario Carneiro]

I think I found a bug in find.js, when I breakpoint here I see that pattern is assigned to "undefined", not undefined which seems to be what the receiving code is expecting (when calling find/ with no arguments as above)

[Mario Carneiro]

Also the call to fetchCachedDeclarationData here is always returning undefined, even though the necessary files are cached

[Mario Carneiro]

oh, maybe this is expected because of doc-gen#133

[Mario Carneiro]

fix posted to doc-gen#153, although it is difficult to test locally (a local server shows no slowdown, although I suspect an outdated cache was to blame)

[Henrik Böving]

@Mario Carneiro it seems to be significantly faster on my firefox now, can you confirm?

[Mario Carneiro]

yes, all of the links seem to be much faster

[Mario Carneiro]

I didn't test src#Nat but I think that's just an alias for docs#Nat now?

[Henrik Böving]

yeah right now it is although that is fixable via the 2 step redirect as you suggested