Open polibb opened 3 years ago
This is great! Thanks Polly!
Let's let GitHub do its thing and build it for all of us to try out:
Or, maybe that needs to be in its own comment?
Hmm, our deploy action is broken...
It might not work for PRs opened from external forks? See e.g. https://github.com/leanprover-community/doc-gen/pull/115#issuecomment-779953415
It might not work for PRs opened from external forks? See e.g. #115 (comment)
Aha, yes, that seems to be it. I think we can delete all of those checks, right? The deploy action is being run from the master branch of this repo, not from the PR, so it should have permission.
This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo!
Are there some good examples we should try in the demo? I tried applying only the "simp" filter and then searching "nat" but the search seems to be stuck on octopuses forever.
Hmm, checking my browser console, I also see a message " TypeError: text is undefined" coming from "const indexedData = req.response;" in searchWorker.js
line 16. I'm using Firefox 88.0.1 on macOS if that matters.
Hmm, that search works for me on Chrome, so it might be browser specific?
It also works for me in Firefox (87.0 on Ubuntu). The octopi are a different color than in Chrome!
However, the search doesn't work at all for me on Android (Chrome 90.0). The query just disappears when I click search. Can anyone else duplicate?
Hi @bryangingechen :) thanks for testing the demo! Seeing " TypeError: text is undefined" is very weird because there's not references to "text" anymore anywhere, that was part of the previous implementation. On the other hand the "const indexedData = req.response;" is in fact part of the new implementation. Would you clean up and delete app of your app cache, cache, form data, indexed DB, and local storage for the domain of "https://leanprover-community.github.io/" and let me know if the problem persists, please? In the meantime I'm looking for ways to try it on macOS as well, I wouldn't be surprised if there has to be a slight tweak in the implementation for different browsers indeed.
Good demo searches I use are "sa" with and without filter "nolint", "la" with and without "theorem", and "a" to see thousands of results once it has started loading freely and quickly after the first search.
@robertylewis The octopi is so much better in Firefox indeed, the whole UI is in my opinion hahaha. You're right about the Android bug - it doesn't work when I try it out either. I will look into it, but I'm also noticing that the version of the search used now hangs forever on Chrome on Android at the moment, which might suggest incompatibility of some sort with the sharedWorker maybe, I'm not sure.
Thank you so much for testing, guys! I'm open to further discussions on how to make it good for everyone.
Thanks, after clearing various caches it works! I did manage to trigger some more console errors by typing in the search box and then hitting apply filters a few times:
Uncaught (in promise) TypeError: searchResultsShowAllBtn is null submitSearchFormHandler https://leanprover-community.github.io/mathlib_docs_demo/nav.js:176 submitFiltersFormHandler https://leanprover-community.github.io/mathlib_docs_demo/nav.js:352
I'll play around with it more before giving more thoughts though!
UPDATE: Fixes pushed, please pull to see them.
The script that has been used for almost a year and is running in the background for the search to function in this PR too is being ran by a SharedWorker which is not compatible with most browsers on a phone and Safari and IE on a desktop. This is not ideal, I understand, but will be improved in the future as it is not part of the scope at this time for this PR.
This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo!
This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo!
This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo!
One other thing that would be great to have before this goes live is an easily accessible / easy-to-find page describing all the search features. Maybe an extra section on the mostly-blank index page https://leanprover-community.github.io/mathlib_docs_demo/ will do?
I think the only blocking thing here is the size of the json file as Eric points out. Was the reason for using a bmp before compression or caching? If we zip the json file when we generate it and unzip locally, I guess browsers won't cache the unzipped version, right?
For @bryangingechen 's suggestion, I think that's a good place to describe the search features and we could probably use some text from this PR.
The reason for the .bmp
extension instead of .json
is that github will then automatically gzip it. See https://github.com/leanprover-community/doc-gen/pull/125
This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo!
The bmp is now 1660854 bytes, and loads in half a second on my machine - I think it was 15mB before compression before, so the file extension change definitely helps.
However, the call to miniSearch.addAll(indexedData)
takes 28 seconds for me, vs 6 seconds it takes on the live site.
I've created https://github.com/polibb/doc-gen/pull/4 to briefly document the search.
I agree with Eric that there's still a slowdown, but it's not near 28 seconds for me. To me the new performance is acceptable, and I'm okay merging, what do others think?
This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo!
Hmm, the 404 page needs to be updated as well: https://leanprover-community.github.io/mathlib_docs_demo/find/nat.addo
This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo!
This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo!
Searching the mathlib library contents in the documentation and filtering of the resulting set of declarations. One is now able to:
More information: