Add clarification to docs about modifying old docs versions

[voisey]

Due to the way in which versioned docs work with Docusaurus, it can be confusing to work out how to modify previous docs versions in a certain scenario. Namely, when you want to make changes to a file in version X.X.1 of the docs, which had not been changed since the previous version X.X.0. In this scenario, the file will not exist in the versioned_docs/version-X.X.1 tree, with the file in the versioned_docs/version-X.X.0 tree being used instead. How to deal with this scenario should be clarified.

[voisey]

I propose adding the following paragraph to below the third bullet point here:

:warning: Note that due to the versioning system used by Docusaurus, if a doc has not been
updated between versions, say between version X.X.0 and X.X.1, then this doc will not appear
in the tree of `versioned_docs/version-X.X.1`. Instead, the X.X.1 documentation will use the
version of the doc in `versioned_docs/version-X.X.0`. Therefore, if you want to make changes
to such a doc in version X.X.1 but not in X.X.0, you need to copy the file from
`versioned_docs/version.X.X.0` to `versioned_docs/version.X.X.1` before making your changes.
An example of this can be seen in this [pull request](https://github.com/magma/magma/pull/14512).

@LKreutzer Could you please let me know what you think of this suggested addition?

[LKreutzer]

I propose adding the following paragraph to below the third bullet point here:

:warning: Note that due to the versioning system used by Docusaurus, if a doc has not been
updated between versions, say between version X.X.0 and X.X.1, then this doc will not appear
in the tree of `versioned_docs/version-X.X.1`. Instead, the X.X.1 documentation will use the
version of the doc in `versioned_docs/version-X.X.0`. Therefore, if you want to make changes
to such a doc in version X.X.1 but not in X.X.0, you need to copy the file from
`versioned_docs/version.X.X.0` to `versioned_docs/version.X.X.1` before making your changes.
An example of this can be seen in this [pull request](https://github.com/magma/magma/pull/14512).

@LKreutzer Could you please let me know what you think of this suggested addition?

Could we maybe also add

• How to remove docs and update the index etc.
• I think after basically any change in the file structure/renaming of files etc. make dev has to be run - correct me if I am wrong - but this is not completely clear from the docs atm imo.

Maybe these points from #14936 could also be mirrored here?

• ⚠️ It should be explained that documentation for the docusaurus is never backported to release branches, because the docusaurus is deployed from the versioned docs on the master branch, see docs/docusaurus/versioned_docs.
• README.md files can be backported if it makes sense.

[voisey]

Thanks for the suggestions! I've made an edit to address your first two bullet points, which you can see here. Do the changes look okay to you? I'll come back to the next two points later.

[voisey]

I've addressed the final two bullet points in the following:

Update a versioned doc: if appropriate, first update the corresponding current doc, then edit the relevant
doc under docs/docusaurus/versioned_docs. Note that the documentation for the docusaurus is never backported
to release branches, because the docusaurus for past versions is deployed from the versioned docs on the
master branch. This does not apply to documentation in README files that are not part of the docusaurus.

Does that look okay to you @LKreutzer? If so, are you happy for this issue to be closed?

[LKreutzer]

Yes, lgtm - feel free to close the issue. 👍