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

[rwbarton]

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.

[bryangingechen]

It should be fine as long as the code that initializes the emscripten build (around here I think) is updated to use the correct option.

[gebner]

I don't have a strong opinion one way or the other.

[cipher1024]

One thing it might (or might not) be a problem for is that we could want to generate .olean files from other source languages than Lean (for instance, C++ or Haskell if we want to do verify that kind of code). I know Lean 4 is around the corner but it's still worth asking if we're better starting with Lean 3 and moving to Lean 4 when enough has been ported / implemented.

I'm not sure that generating .olean files would be the right approach there but my other candidate involves using an FFI or a plugin framework which is currently inexistent. And I don't like the idea of generating .lean files.

[rwbarton]

@cipher1024, by "it", do you mean the change in default behavior, or using the --old flag? I'm expecting that someone generating .olean files from a non-Lean source also has some sort of custom build setup (so that they know when to regenerate the .olean files for example) to which they can add --allow-standalone-oleans. I guess in principle someone could provide a binary-only package which other people use as a dependency and leanpkg getting confused by this, but for now this seems pretty far-fetched.

@bryangingechen, thanks. Would you mind testing the web editor once I have a patch? I expect to be able to figure out how to add the option but I'm not sure how to set up the emscripten build.

[bryangingechen]

@rwbarton No problem, just ping me again in the PR.

[cipher1024]

I meant the change in the default behavior. The point about the build system is reasonable. We could also make the flag available as set_option or even just allow one specific standalone olean file with something like run_cmd allow_standalone "generated.olean".