Infra: Add search to the PEP index

[nineteendo]

I currently search like this: https://github.com/search?q=repo%3Apython%2Fpeps+lang%3AreStructuredText&type=code
It would be easier if the was a search box on https://peps.python.org.

[hugovk]

Agreed that it would be useful, it's something I often miss.

[willingc]

Nice idea @nineteendo.

[miketheman]

I spent some time looking into this today, and here's what I've found so far:

sphinx search was intentionally disabled in #1934 (comment) , recommending folks use public search engines with site-scoping.
While that's not a bad solution, it's not advertised anywhere user-facing, and implementing a search box on the site that would use a public (maybe even popular) search engine may be counter to some folks' desires to keep their searches private, and I'd hate to drag people into a weird search.

I tried reenabling sphinx search, and it's not too bad of a change, but since the general approach sphinx "wants" is to have a theme that extends an existing one (like basic) to inject the right JS snippets, so in order to make this work we'd need to either vendor the JS or figure our a smart JS loader from the pre-packed code - I couldn't figure that out yet.

Largely, it comes from here:

peps/pep_sphinx_extensions/pep_processor/html/pep_html_builder.py

Lines 9 to 23 in 1fb889b

	class FileBuilder(StandaloneHTMLBuilder):
	copysource = False # Prevent unneeded source copying - we link direct to GitHub
	search = False # Disable search
	# Things we don't use but that need to exist:
	indexer = None
	relations = {}
	_script_files = _css_files = []
	globalcontext = {"script_files": [], "css_files": []}
	def prepare_writing(self, _doc_names: set[str]) -> None:
	self.docwriter = HTMLWriter(self)
	_opt_parser = OptionParser([self.docwriter], defaults=self.env.settings, read_config_files=True)
	self.docsettings = _opt_parser.get_default_values()
	self._orig_css_files = self._orig_js_files = []

I'd be happy to continue to poke at this if there's continued interest in having a PEP web search, and don't want to invest the effort if it's not going to pass a review ;)

[AA-Turner]

Indeed, disabling search was intentional, both to improve performance and as Sphinx's search isn't that great, so readers are better served by using their favourite search engine (there are many discussions about this on Sphinx's side, notably https://github.com/orgs/sphinx-doc/discussions/12419, but the précis is that improving search is costly and will take a not insignificant amount of effort to do right).

A