Stream: Coq devs & plugin devs

Topic: Weird test-suite failure

Pierre-Marie Pédrot (Nov 05 2021 at 20:26):

Have people seen https://github.com/coq/coq/pull/15129/checks?check_run_id=4120624976 somewhere else?

Pierre-Marie Pédrot (Nov 05 2021 at 20:26):

(note the segmentation fault)

Emilio Jesús Gallego Arias (Nov 05 2021 at 20:46):

Very rarely, could be some OOm

Emilio Jesús Gallego Arias (Nov 05 2021 at 20:46):

gonna rerun

Paolo Giarrusso (Nov 05 2021 at 21:16):

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…

Emilio Jesús Gallego Arias (Nov 05 2021 at 21:18):

That's a special test involving workers, which likely don't handle some failure conditions propertly

Gaëtan Gilbert (Nov 05 2021 at 21:19):

it doesn't use workers in test-suite:base

Emilio Jesús Gallego Arias (Nov 05 2021 at 21:20):

it does not?

Emilio Jesús Gallego Arias (Nov 05 2021 at 21:20):

hard to parse the makefile, but not sure

Emilio Jesús Gallego Arias (Nov 05 2021 at 21:20):

but seems to pass -async-proofs on

Gaëtan Gilbert (Nov 05 2021 at 21:21):

oh indeed

Gaëtan Gilbert (Nov 05 2021 at 21:56):

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

but then

  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?

Emilio Jesús Gallego Arias (Nov 06 2021 at 13:39):

:pumpkin:

Paolo Giarrusso (Nov 06 2021 at 14:27):

(deleted)

Last updated: Apr 19 2024 at 16:01 UTC