change docs from Sphinx to something else?

Since we are working just now on fixing a search bug (#748 (closed)), I am reminded that I dislike dealing with the documentation and wonder if we should change to something else. What annoys me:

• It's buggy. E.g., it took ages to fix the list spacing bug introduced in 2.x.
• Search is bad. Even after PR #834, search won't work right; e.g., it says "ch-grow" and "ch-run" have no results.
• I dislike ReST. For example, you can't nest markup like monospace (code) within bold or italic. (Note I don't care much better for Markdown, despite its trendiness.)
• It interacts weirdly with Make. For example, it re-builds the docs frequently for reasons I don't understand and seem unnecessary (make install will always rebuild the docs, twice IIRC).
• Even the supposedly top-of-the-line Read-the-Docs theme makes a lot of ugly choices, e.g. monospace for in-line code is bright red and boxed. Other themes don't seem any better.
• In general, Sphinx has been troublesome and a hassle.

Our requirements are something like:

• Decent HTML pages we can put on github.io or similar.
• Decent man pages, because packagers like those.
• Needs to be easy to package even on crusty distros like CentOS 7.
• We don't currently have any need to auto-generate API docs.

Options include:

• Keep Sphinx, and:
  • accept the cruddy search
  • remove the search box, letting users use a general web search e.g. Google
  • replace the search box with a link to Google site search
  • wire up the search box as Google site search somehow
  • use readthedocs.io, which has a better search
• Ditch Sphinx in favor of:
  • LaTeX: real professional tool, very nice PDF output, HTML and man pages less so
  • GNU Texinfo: real professional tool, old/obsolete, plays well with Autotools, PDF works, HTML looks old, no native man output
  • ... ?