This PR migrates most remaining tests to the new test suite. It also
completes the migration of directories like `tests/lean/run`, meaning
that PRs trying to add tests to those old directories will now fail.
These examples are checked in Lean's CI to ensure that they continue
to work. They are included in the documentation section of the Lean
website via a script that copies the latest version, in order to
ensure that the website tracks Lean releases rather than master.