exceptions when saving oleans are not user-visible

[collares]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

The olean compilation process emits user-friendly messages for several failure scenarios, such as https://github.com/leanprover-community/lean/blob/v3.45.0/src/library/module_mgr.cpp#L128. However, the failure is not notified to the user. This includes heartbeat exception reporting, as in #749.

Steps to Reproduce

1. Create an empty olean and remove write permissions
2. Use lean --make to compile something that would overwrite the above file

Expected behavior: Non-zero exit code and a message

Actual behavior: No reported error

Reproduces how often: 100%

Versions

Lean (version 3.45.0, commit 22b09be, Release)