Migration of the manual into odoc

[panglesd]

In #324, @pitag-ha explained the problems of the documentation of ppxlib, and gave a detailed plan on how to improve it.

This PR is one of the first step on this plan, and consists of an almost one-to-one translation of the manual from restructuredText odoc.

This improves a discoverability, because the API and the manual are now on the same system, with an index.mld presenting the library and linking all resources in one place. This homepage is also displayed in v3.ocaml.org. The interconnection between the API and manual is also improved, with many added links from the manual into the API.

There is one thing that I think should be discussed before merging this PR, to avoid too many commits with whole file rewriting: odoc currently does not allow to specify a multipage navigation bar on the left (see ocaml/odoc#479)). I see several workarounds:

• Make the documentation a single-page document
• Add Previous -- Next links at top and bottom of each page.

I would rather have a one page documentation. What do you think?

[panglesd]

After discussing with @pitag-ha, we opted for a one-page manual. (exemple here).

[pitag-ha]

Nice, thanks for this @panglesd, and sorry for the super delay in reviewing! I think it's a good improvement! A couple of minor comments:

We should also update the link in the README pointing to the manual. Can you do that? If you're busy, I can also do it myself quickly. (And we also need to rebase over main for the CI to pass.)

And the other thing: Given that there might be more places than our own README with a link to the old manual, it might be nice to keep the old manual with just one line: a link to the new manual. What do you think?

[panglesd]

The problem with changing the link in the README, is that we will need to update the html of the API in the github pages, but there has been changes in the API since the last release (eg #333).

So we don't want to incorporate those API changes in the current API until the next release.

Either we wait for a release to update the README and the API, or I rebase over 0.26, so that you can generate the API from since then but with the odoc manual. (is it clear? I feel unclear...)

What would you prefer?

Otherwise, I agree that I there should be a link (or better, an automatic redirection) from the old manual to the new manual.
I'll investigate if an automatic redirection is possible, or just add a link, when rebasing tomorrow!

[pitag-ha]

The problem with changing the link in the README, is that we will need to update the html of the API in the github pages, but there has been changes in the API since the last release (eg #333).

Ooh, very good point! Ok, let's just wait until the next release to update the README.

I'll investigate if an automatic redirection is possible, or just add a link, when rebasing tomorrow!

Perfect. Thanks!

[panglesd]

I'll investigate if an automatic redirection is possible

It seems https://stackoverflow.com/a/69928404/14792825 is exactly what we need.
You need to log in to the rtd interface, though, so I can't do it myself. (I'll do the "replace index.rst with a redirection" part)

[panglesd]

I added a commit at the root of this PR, corresponding to the last version of the readthedocs manual: a version where the index is only redirecting to the homepage of the new manual.

So to merge this commit, you need to:

• add the redirect on the rtd interface
• add the first commit of this PR and make rtd fetch it and update the docs
• add the rest of the commits
• build the new doc and deploy it on the github page

If for some reason we prefer not to set up the redirect in the rtd interface, I can also turn each page (there are only 3) into a redirect in the first commit.

[pitag-ha]

You need to log in to the rtd interface, though, so I can't do it myself.

The funny thing is that I don't have access to our rtd either. That's why I was suggesting back then to simply replace our rtd docs with a link to our new odoc docs site. Let me find out if there's still anyone around with access to our rtd, since the clean-up with redirection would be far nicer.

Would it be much work to just keep both for now to be able to merge this PR? It would be very nice to have this merged...

[panglesd]

Since readthedocs is reading the docs from master and the main branch is now called main, we can safely merge this. 🎉