Stream: Coq devs & plugin devs

Topic: Weird test-suite failure


view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Nov 05 2021 at 20:26):

(note the segmentation fault)

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 20:46):

Very rarely, could be some OOm

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 20:46):

gonna rerun

view this post on Zulip 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…

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Nov 05 2021 at 21:19):

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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 21:20):

it does not?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 21:20):

hard to parse the makefile, but not sure

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 21:20):

but seems to pass -async-proofs on

view this post on Zulip Gaëtan Gilbert (Nov 05 2021 at 21:21):

oh indeed

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 06 2021 at 13:39):

:pumpkin:

view this post on Zulip Paolo Giarrusso (Nov 06 2021 at 14:27):

(deleted)


Last updated: Feb 06 2023 at 20:02 UTC