From f142d9f798d55f5e54ca54a353a2d7cf8ba9cd82 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 27 Nov 2023 09:17:33 +0100
Subject: [PATCH] fix: ignore errors on `IO.FS.Handle` finalization (#2935)

---
 .github/workflows/ci.yml | 6 +++---
 src/runtime/io.cpp       | 6 +++++-
 2 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 547b51e9cd..1ef6a5c259 100644
--- a/.github/workflows/ci.yml
+++ b/.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:
diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp
index a2335c0f5f..207e33b8c4 100644
--- a/src/runtime/io.cpp
+++ b/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 */) {