search

coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
https://coq.inria.fr/
GNU Lesser General Public License v2.1
4.85k stars 648 forks source link

Coq documentation search is terrible #12811

Open JasonGross opened 4 years ago

JasonGross commented 4 years ago

Description of the problem

https://coq.inria.fr/refman/search.html?q=%22print+sorted+universes%22&check_keywords=yes&area=default# gives

image

None of these seem to contain the phrase "print sorted universes".

Coq Version

8.12

silene commented 4 years ago

As explained in Sphinx' documentation, a potential solution is to use Google's search engine instead of the builtin one:

  1. Create a search engine on https://cse.google.com/cse/all
  2. Dump the produced code into doc/sphinx/_templates/searchbox.html.
  3. Modify accordingly html_sidebars in doc/sphinx/conf.py.