lean4-htt/src
Mac Malone f7102363de
fix: lake: race condition in Cache.saveArtifact (#13110)
This PR fixes a race condition in `Cache.saveArtifact` that caused
intermittent "permission denied" errors when two library facets (e.g.,
`static` and `static.export`) produce artifacts with the same content
hash and attempt to cache them concurrently.

The race occurs because `saveArtifact` checks `cacheFile.pathExists`,
then writes the file and makes it read-only. When two tasks race past
the existence check, the second task's write fails because the first
task already created the file and set it to read-only. On Linux, this is
common for `static` vs `static.export` since both resolve to the same
`coExport` object files, producing byte-identical archives.

The fix introduces `writeFileIfNew` and `writeBinFileIfNew` helpers that
use `O_CREAT | O_EXCL` (via `IO.FS.Mode.writeNew`) to atomically
create-or-skip, eliminating the race window. For the binary path, hard
link `alreadyExists` errors are also handled explicitly to avoid an
unnecessary copy fallback.

Additionally, `IO.setAccessRights` for the cache file is moved outside
the `unless pathExists` block so that permissions are always enforced,
and the `getMTime` call no longer silently swallows errors.

🤖 Prepared with Claude Code
2026-03-24 19:05:56 +00:00
..
bin perf: separate meta and non-meta initializers (#12016) 2026-02-26 08:05:19 +00:00
cmake
include/lean perf: mark inhabited arguments to extern as borrowed (#13094) 2026-03-24 13:54:06 +00:00
Init feat: String.drop lemmas (#13109) 2026-03-24 17:51:06 +00:00
initialize
kernel feat: theorems are opaque (#12973) 2026-03-23 13:57:07 +00:00
lake fix: lake: race condition in Cache.saveArtifact (#13110) 2026-03-24 19:05:56 +00:00
Lean doc: typo fix for strict implicit binder (#13099) 2026-03-24 13:15:23 +00:00
library feat: increase default stack size from 8MB to 1GB (#12971) 2026-03-20 15:40:00 +00:00
runtime perf: mark inhabited arguments to extern as borrowed (#13094) 2026-03-24 13:54:06 +00:00
shell
Std feat: lemmas comparing List.Cursor.pos to List.length (#13096) 2026-03-24 10:40:03 +00:00
util chore: update to c++20 (#12117) 2026-02-11 01:17:40 +00:00
cadical.mk
CMakeLists.txt feat: experimental option to move non-meta compilation out of lean build step (#10291) 2026-03-20 10:39:39 +00:00
config.h.in
githash.h.in
Init.lean feat: add cbv_simproc infrastructure for user-extensible cbv simplification procedures (#12597) 2026-03-10 10:59:13 +00:00
lakefile.toml.in chore: pass the previous stage libLake as plugin (#13000) 2026-03-20 12:23:20 +00:00
lean-toolchain chore: relative lean-toolchains (#12652) 2026-02-25 10:23:35 +00:00
Lean.lean
lean.mk.in
Leanc.lean
LeanChecker.lean refactor: remove Lean.Environment.replay from core (#12972) 2026-03-18 22:11:42 +00:00
LeanIR.lean feat: experimental option to move non-meta compilation out of lean build step (#10291) 2026-03-20 10:39:39 +00:00
out
Std.lean
stdlib.make.in feat: experimental option to move non-meta compilation out of lean build step (#10291) 2026-03-20 10:39:39 +00:00
stdlib_flags.h chore: consistent build flags between USE_LAKE ON and OFF (#12941) 2026-03-17 11:02:55 +00:00
version.h.in