fix: ignore errors on IO.FS.Handle finalization (#2935)

.github/workflows/ci.yml

@@ -132,7 +132,7 @@ jobs:
             # exclude seriously slow/problematic tests (laketests crash)
             CTEST_OPTIONS: -E 'interactivetest|leanpkgtest|laketest|benchtest'
           - name: macOS
-            os: macos-11
+            os: macos-latest
             release: true
             shell: bash -euxo pipefail {0}
             llvm-url: https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-apple-darwin.tar.zst
@@ -140,7 +140,7 @@ jobs:
             binary-check: otool -L
             tar: gtar  # https://github.com/actions/runner-images/issues/2619
           - name: macOS aarch64
-            os: macos-11
+            os: macos-latest
             release: true
             cross: true
             shell: bash -euxo pipefail {0}
@@ -223,7 +223,7 @@ jobs:
       - name: Install Brew Packages
         run: |
           brew install ccache tree zstd coreutils gmp
-        if: matrix.os == 'macos-11'
+        if: matrix.os == 'macos-latest'
       - name: Setup emsdk
         uses: mymindstorm/setup-emsdk@v12
         with:

src/runtime/io.cpp

@@ -89,7 +89,11 @@ static obj_res mk_file_not_found_error(b_obj_arg fname) {
 static lean_external_class * g_io_handle_external_class = nullptr;
 
 static void io_handle_finalizer(void * h) {
-    lean_always_assert(fclose(static_cast<FILE *>(h)) == 0);
+    // There is no sensible way to handle errors here; in particular, we should
+    // not panic as finalizing a handle that already is in an invalid state
+    // (broken pipe etc.) should work and not terminate the process. The same
+    // decision was made for `std::fs::File` in the Rust stdlib.
+    fclose(static_cast<FILE *>(h));
 }
 
 static void io_handle_foreach(void * /* mod */, b_obj_arg /* fn */) {