don't use "standalone" .olean files by default

It's fairly common to end up with accidentally end up with .olean files whose corresponding .lean file is gone (because it has been renamed, for example) and it can cause confusion when Lean continues to use the old .olean file anyways. I was going to fix this "bug", but then I happened to notice a changelog entry indicating that this behavior is intended, and used to support the Lean web editor. So I propose to control this behavior with a command-line flag, defaulting to "don't use standalone .oleans", because it's easier to change how the Lean web editor works, I imagine.

Question: Should this behavior be controlled by --old, so that lean --old will use standalone .olean files (since it doesn't care about the .lean files anyways)? Or should we add a new flag like lean --allow-standalone-oleans?

@bryangingechen or others involved with the Lean web editor: please let me know whether the proposed change will be okay for the Lean web editor.

The issue does not name implementation files or tests. Start by reviewing the existing --old command-line handling and the changelog entry describing standalone .olean files; resolve the flag design with the Lean web editor stakeholders, then verify that the chosen default and compatibility behavior work as specified.