Stream: Coq Platform devs & users

Topic: CI Timeouts


view this post on Zulip Michael Soegtrop (Sep 23 2022 at 09:48):

@Théo Zimmermann : I recently have on Windows a timeout failure rate of guessed 1/3. Usually it gets through in 5h20 or so, but it happens regularly that it exceeds 7h. Can we extend the timeout to 8h? I think after the release I will create an option for "long compile time packages" and check these less frequently - or in a separate CI run. They tend to be not problematic.

If I remember right, you extended it to 6h last time I had issues.

view this post on Zulip Théo Zimmermann (Sep 23 2022 at 11:07):

No, you are confusing with GitLab. On GitHub Actions there is a hard limit at 6 hours per job.

view this post on Zulip Théo Zimmermann (Sep 23 2022 at 11:08):

The only solution to workaround such a timeout issue is to split the job into multiple jobs.

view this post on Zulip Théo Zimmermann (Sep 23 2022 at 11:08):

Is this something that would be realistic to do? The jobs can share artifacts.

view this post on Zulip Théo Zimmermann (Sep 23 2022 at 11:09):

Note that such splitting could also be used to reduce the workflow time by parallelizing some builds (if realistic).

view this post on Zulip Michael Soegtrop (Sep 23 2022 at 12:10):

OK, that looks useful. For threads the META file is:

# Specifications for the "threads" library:
version = "[distributed with Ocaml]"
description = "Multi-threading"
requires(mt,mt_vm) = "threads.vm"
requires(mt,mt_posix) = "threads.posix"
directory = "^"
type_of_threads = "posix"

browse_interfaces = ""

warning(-mt) = "Linking problems may arise because of the missing -thread or -vmthread switch"
warning(-mt_vm,-mt_posix) = "Linking problems may arise because of the missing -thread or -vmthread switch"

package "vm" (
  # --- Bytecode-only threads:
  requires = "unix"
  directory = "+vmthreads"
  exists_if = "threads.cma"
  archive(byte,mt,mt_vm) = "threads.cma"
  version = "[internal]"
)

package "posix" (
  # --- POSIX-threads:
  requires = "unix"
  directory = "+threads"
  exists_if = "threads.cma"
  archive(byte,mt,mt_posix) = "threads.cma"
  archive(native,mt,mt_posix) = "threads.cmxa"
  version = "[internal]"
)

package "none" (
  error = "threading is not supported on this platform"
  version = "[internal]"
)

which has the only effect that it does not work if there is no threads.cma file at runtime - which I don't think makes sense.

view this post on Zulip Michael Soegtrop (Sep 23 2022 at 12:14):

@Théo Zimmermann : it makes sense to disable 3 or 4 long runners in CI - things like unimath. They anyway don't have a tendency to create install issues (this is what Coq Platform CI detects). But of course one has to enable them for release build. Modular builds I would delay until we have modular installers.


Last updated: Jan 30 2023 at 11:03 UTC