search Demo (version 3)

Stream: mathlib documentation

[Polina Boneva]

Hello to all interested in searching through the documentation of mathlib :)
Version 1 of the search involved a simple reference to a Google search.
Version 2 allows a search through the names of all declarations in the library. This is the one that's used in the documentation currently.
Version 3 allows a search through the names of the declarations, the name of the modules they are in, and the descriptions for each declaration, as it is found in the library itself as a comment next to the declaration tag and contents. Filtering is possible attributes and kind has also been added as well. Please check out the demo at https://leanprover-community.github.io/mathlib_docs_demo/
Some issues have been found and are being discussed in the PR: https://github.com/leanprover-community/doc-gen/pull/131
Feel free to test it out and report any and all bugs and features you find. The bugs will take highest priority for now :)

[Polina Boneva]

Hello to all interested in searching through the documentation of mathlib :)
Version 1 of the search involved a simple reference to a Google search.
Version 2 allows a search through the names of all declarations in the library. This is the one that's used in the documentation currently.
Version 3 allows a search through the names of the declarations, the name of the modules they are in, and the descriptions for each declaration, as it is found in the library itself as a comment next to the declaration tag and contents. Filtering is possible attributes and kind has also been added as well. Please check out the demo at https://leanprover-community.github.io/mathlib_docs_demo/
Some issues have been found and are being discussed in the PR: https://github.com/leanprover-community/doc-gen/pull/131
Feel free to test it out and report any and all bugs and features you find. The bugs will take highest priority for now :)

[Polina Boneva]

P.S. For a better and saver experience clean your app cache, cache, form data, indexed DB, and local storage for the domain of leanprover-community.github.io because it might not work as expected otherwise. I'm using an extension for this - Clean Cache, but there are many others and of course you can use your browser's settings directly if you prefer.

[Kevin Buzzard]

I don't know what any of that PS means

[Kevin Buzzard]

Is this really worth a new stream BTW?

[Scott Morrison]

I think the PS means: modern browsers cache lots of things, but this new docs demo is being actively changed, and weird things may happen as a result of some things being cached when other things are being updated. I wouldn't worry.

[Polina Boneva]

exactly, @Scott Morrison :) There is a reported problem for the search capabilities on Firefox on macOS, but I tested it there too and it works fine for me. I have never before opened this domain there though, so I think that is a big part of whether something works or doesn't.
On this note, the SharedWorker that is currently being used to run the searching script separately in a parallel thread is actually not supported extensively. For example, it doesn't have any support on Safari on desktop and any Android browser except Firefox, unfortunately. Internet Explorer of course is also out of the game. Thus it's probably best to find another approach in the future that is both flexible and compatible with more browsers.