Bryan Gin-ge Chen
Bryan Gin-ge Chen
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...
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...
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:...
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...
I usually run `leanproject up` to update the project to depend on the latest mathlib master, or simply `leanproject get-mathlib-cache` if I don't care what version of mathlib I'm generating...
> what exactly will be extremely slow otherwise? If the `.olean` files are not present, generating the docs will take a long time since Lean will have to compile all...
We could add a new field to the tactic doc entry structure to store a list of anchors, and then make `doc-gen` add all of those to the HTML.
In fact, spaces are not even really allowed in `id` attributes: https://validator.w3.org/nu/?doc=https%3A%2F%2Fleanprover-community.github.io%2Fmathlib_docs%2Ftactics.html (This also affects the attributes, commands, hole_commands and notes pages.) One simple fix for the spacing issue is...