File references in the manual get silently invalidated by file changes

[Kukovec]

Often, manual sections will link to hard-coded segments in source .tla files. For example, https://github.com/informalsystems/apalache/blob/a7b670cb700683554e933aef81a189a9843ae059/docs/src/apalache/principles/recursive.md?plain=1#L15-L19 used to point to the definitions of FoldSeq and FoldSet, but as Apalache.tla has changed in the meantime, the manual displays unrelated sections from Apalache.tla

We need a manual watchdog in CI, where whenever a file that is referenced anywhere in the manual gets changed, the PR author is notified and incentivized to fix manual references.

[Kukovec]

@shonfeder do you have any idea how complex this would be?

[thpani]

Somewhat related, in #1612 the tool output changed from what was recorded in the manual. We should perhaps keep it in mind when addressing this issue.

[thpani]

We probably want to migrate to using mdBook anchors. @p-offtermatt discovered this 🤩.

[shonfeder]

Yes! That will be much better :)