Zulip Chat Archive

Stream: general

Topic: searching mathlib Docs: declarations, descriptions, modules


Polina Boneva (May 15 2021 at 13:19):

Hello to all interested in searching through the documentation of mathlib :)
@Rob Lewis and I have been working on improving the searching method in the documentation of mathlib and would like your take on the development until now. This improvement on the search box allows for a detailed exact-word-matching 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 misses you find. The bugs will take highest priority for now :)


Last updated: Dec 20 2023 at 11:08 UTC