Stream: Coq devs & plugin devs

Topic: opam packaging conf-? for ulimit

view this post on Zulip Jason Gross (Oct 13 2022 at 17:22):

Is there's a conf-* opam package to require to make sure ulimit is available?

view this post on Zulip Guillaume Melquiond (Oct 13 2022 at 23:41):

ulimit is not a separate program, it is a builtin utility of any posix-compliant shell. So, a conf-ulimit package does not make sense. At best, it would be something like conf-bash or similar, but I don't think those exist.

view this post on Zulip Karl Palmskog (Oct 14 2022 at 07:17):

bash availability seems to be assumed in opam, e.g., package arg-complete has no dependency on any bash-related stuff, despite being for bash

view this post on Zulip Michael Soegtrop (Oct 14 2022 at 07:56):

ulimit is indeed posix, but the stack option I guess @Jason Gross is after is not. See (

Thinking about it I darkly remember that on some linux variants ulimit has no effect and that the preferred method is using prlimit these days, but I can't find proper references. prlimit is a separate executable, so one could have a conf package for it.

view this post on Zulip Anders Larsson (Oct 14 2022 at 08:48):

These settings is more about the process tree and system calls than about specific commands.

view this post on Zulip Paolo Giarrusso (Oct 14 2022 at 13:23):

@Michael Soegtrop ulimit -m is indeed useless (too complex) since ages, could that be what you're thinking? ulimit -s seems easier to guarantee

view this post on Zulip Michael Soegtrop (Oct 14 2022 at 13:54):

@Paolo Giarrusso sorry I can't remember the details but I darkly remember that I have read somewhere that cause of some changes in modern Linux ulimit is not reliable any more and one should use prlimit now. But the main point is that since prlimit is a separate executable it is easier to guarantee to exist, but then it is likely harder to use.

Anyway, I would say we can use ulimit -s without any extra precautions and further discuss this in case there are actual issues with it. Hopefully if a shell does not support it, it results in an immediate error.

view this post on Zulip Matthieu Sozeau (Oct 14 2022 at 14:58):

FYI, we use ulimit also in the certicoq package

view this post on Zulip Matthieu Sozeau (Oct 14 2022 at 14:58):

(for stack size)

Last updated: Feb 06 2023 at 00:03 UTC