(Optimistic) Unify docs search

[penelopeysm]

Right now, our search bar (afaik) only indexes the content of two repositories: this one and https://github.com/TuringLang/turinglang.github.io.

This means that a lot of generated documentation (for the individual packages, see e.g. https://turinglang.org/DynamicPPL.jl) cannot be discovered via the search bar.

My first suggestion to deal with this is to restrict Documenter.jl documentation to only be used for API documentation, rather than usage guides. Usage guides should be moved to this repo if possible (the only case where this is not possible is if there are version / dependency conflicts, e.g. new features in DynamicPPL that don't have a corresponding Turing release yet).

---

Long-term though, we should like the search index to work over all repositories. Unfortunately, it's also a very non-trivial task, as it would require either:

• Putting together some sort of tool that builds the website, extracts some info about the generated html, and puts that info at a fixed location where the search can be pointed to.
• Reworking the entire documentation generation structure such that it is all built from a single location.

I think the latter is unworkable. For the former, we can probably take some inspiration from how the docs + turinglang.github.io search indexes are merged:

docs/.github/workflows/publish.yml

Lines 98 to 109 in 0667406

	- name: Fetch search_original.json from main site
	run: curl -O https://raw.githubusercontent.com/TuringLang/turinglang.github.io/gh-pages/search_original.json
	- name: Convert main site search index URLs to relative URLs
	run: |
	jq 'map(
	if .href then .href = "../" + .href else . end |
	if .objectID then .objectID = "../" + .objectID else . end)' search_original.json > fixed_main_search.json
	- name: Merge both search index
	run: |
	jq -s '.[0] + .[1]' _site/search_original.json fixed_main_search.json > _site/search.json

This makes use of search_original.json which is generated by Quarto (Quarto calls it search.json, the github runner renames it):

https://raw.githubusercontent.com/TuringLang/turinglang.github.io/gh-pages/search_original.json

and the corresponding entry for the docs repo:

https://raw.githubusercontent.com/TuringLang/docs/gh-pages/search_original.json

Perhaps unsurprisingly, Documenter.jl also generates a search index, see e.g.:

https://github.com/TuringLang/AbstractPPL.jl/blob/gh-pages/v0.9.0/search_index.js

So the task would be to

1. Convert Documenter's search_index.js and Quarto's search.json to a common format (which will probably be search.json as that's what needed for Quarto search to work out-of-the-box)
2. When any of the repos are built:
   • generate this json and and store it in a shared location somewhere
   • merge all of them into a single json
3. When this repo or the main site repo are built:
   • retrieve that single JSON and stick it into the search bar

---

Finally, note that the search function is only available on the main site + docs. As a stretch goal, we could also think about how the search bar can be added to other sites as well.

Also, even if we manage to unify the search across all repos, I believe it is still a good idea to restrict individual repo's Documenter.jl to contain only API documentation rather than guides. Even if we have a fully functional search bar, I think a doc that is on this repo is still far more discoverable than one in another repo, simply because there will be a link to it in the sidebar.