Have people seen https://github.com/coq/coq/pull/15129/checks?check_run_id=4120624976 somewhere else?
(note the segmentation fault)
Very rarely, could be some OOm
An OOM doesn't look like a segfault, unless you have a
malloc (or such) which returns
null and whose result isn’t checked (I’ve seen this in the GHC runtime system). But failing mallocs are rare unless you disable overcommit…
That's a special test involving workers, which likely don't handle some failure conditions propertly
it doesn't use workers in test-suite:base
it does not?
hard to parse the makefile, but not sure
but seems to pass -async-proofs on
wtf is going on in persistent_cache?
(** We used to only lock/unlock regions. Is-it more robust/portable to lock/unlock a fixed region e.g. [0;1]? In case of locking failure, the cache is not used. **) type lock_kind = Read | Write let lock kd fd = let pos = lseek fd 0 SEEK_CUR in let success = try ignore (lseek fd 0 SEEK_SET); let lk = match kd with Read -> F_RLOCK | Write -> F_LOCK in lockf fd lk 1; true with Unix.Unix_error (_, _, _) -> false in ignore (lseek fd pos SEEK_SET); success
let do_under_lock kd fd f = if lock kd fd then fun_protect f ~finally:(fun () -> unlock fd) else f ()
so if locking fails we do exactly the same as if it succeeds except for the unlock?
Last updated: Dec 07 2023 at 09:01 UTC