Configuring Read the Docs to publish the MPS manual

[rptb1]

Adds CI configuration to build the MPS manual and publish it at https://memory-pool-system.readthedocs.io/ .

CI will help us know sooner if the manual breaks.

Migrates away from Ravenbrook internal automation that publishes at https://www.ravenbrook.com/project/mps/master/manual/html/ . See #98 (comment) .

Fixes #118.

[rptb1]

Bootstrap issue: If the Read the Docs manual goes away, and someone has a bare MPS tree, how can they read the manual? The readme.txt does not lead to instructions for how to build and read it.

[rptb1]

https://memory-pool-system.readthedocs.io/en/latest/design/index.html is blank, so Read the Docs didn't run Sphinx in the same way as "make html" would.

[rptb1]

https://memory-pool-system.readthedocs.io/en/latest/design/index.html is blank, so Read the Docs didn't run Sphinx in the same way as "make html" would.

Examining the Read the Docs build output at https://readthedocs.org/projects/memory-pool-system/builds/19364054/ reveals that it's invoking Sphinx with

python -m sphinx -T -E -b html -d _build/doctrees -D language=en . ../../_readthedocs/html

whereas we invoke it with

mps/manual/Makefile

Line 48 in 4108cc4

$(SPHINXBUILD) -b html $(ALLSPHINXOPTS) $(BUILDDIR)/html

So Read the Docs is building with "manual/source" as the current working directory. That causes this glob to find no design documents

mps/manual/source/extensions/mps/designs.py

Line 162 in 4108cc4

for design in glob.iglob('../design/*.txt'):

[rptb1]

That causes this glob to find no design documents

Fixed in 409aea1 by using app.srcdir as the base directory for the glob etc.

You can see that the designs are converted in https://readthedocs.org/projects/memory-pool-system/builds/19364368/ output from the Sphinx command and at https://memory-pool-system.readthedocs.io/en/branch-2023-02-02-readthedocs/design/index.html

[rptb1]

Bootstrap issue: If the Read the Docs manual goes away, and someone has a bare MPS tree, how can they read the manual? The readme.txt does not lead to instructions for how to build and read it.

Fixed in 380b43d which also closes #144 .

Results visible at https://memory-pool-system.readthedocs.io/en/branch-2023-02-02-readthedocs/guide/build.html#building-the-mps-manual

[rptb1]

Review suggestion: Check https://memory-pool-system.readthedocs.io/en/branch-2023-02-02-readthedocs/index.html against https://www.ravenbrook.com/project/mps/master/manual/html/ to make sure building with Read the Docs hasn't broken anything. They ought to be identical in content, except for changes made in this branch.

[rptb1]

@UNAA008 spotted a couple of warnings from Read the Docs:

WARNING: while setting up extension extensions.mps: directive 'deprecated' is already registered, it will be overridden
WARNING: while setting up extension extensions.mps: node class 'note' is already registered, its visitors will be overridden

Investigate.

[rptb1]

@UNAA008 spotted a couple of warnings from Read the Docs

https://github.com/Ravenbrook/mps/blob/631d30ea5cc1307f801ec2b6d0c3444e6f411172/manual/source/extensions/mps/__init__.py is not well commented, and it's hard to discern the intention, but these are definitely deliberate overrides.

I think adding commentary or working out whether and how to suppress these warnings is outside the scope of this pull request and not very important.

[rptb1]

The manual on Read the Docs doesn't seem to have a search. Investigate.

https://dnd-srd-sphinx.readthedocs.io/en/latest/index.html has a search. I suspect this is to do with our custom theme. We may be able to inherit the search from Read the Docs themes.

[rptb1]

GitHub deleted my express review record. Reconstructing...

We executed proc.review.express.

1. @UNAA008 and @thejayps attending.
2. @UNAA008 had a PI: "TODOs" are for nice-level stuff.
3. @rptb1 has a new PI: Press the Comment button to save the review record before doing anything else with your tab.
4. We found no major defects and three minor defects.
5. @rptb1 I wonder if we could have a general duplicate text finder to prevent Configuring Read the Docs to publish the MPS manual #141 (comment)
6. @rptb1 Iwbni we had a global tag checker to prevent Configuring Read the Docs to publish the MPS manual #141 (comment)
7. Edits made together 170d805
8. Starting exit at 15:20.
9. Estimated defects remaining: zero.
10. Revised change passed.
11. Express review took 55 minutes.

[thejayps]

proc.review.exit.pass

#141 (comment)

[rptb1]

Executing proc.merge.pull-request.

1. Start time 16:17.
2. An automated test case isn't feasible because it would need to publish a readme.txt via GitHub and check that the link to the manual was broken.
3. End time 16:22.
4. Merging procedure took 5 minutes.

[rptb1]

• @UNAA008 had a PI: "TODOs" are for nice-level stuff.

Added to #140 (comment)

• @rptb1 has a new PI: Press the Comment button to save the review record before doing anything else with your tab.

Fixed in 6fa80f4

• @rptb1 I wonder if we could have a general duplicate text finder

Created #160

• @rptb1 Iwbni we had a global tag checker to prevent ..

Created #161