prove-all: configurable memory headroom

[d-xo]

Proofs on CI are getting killed when many large specs (e.g. mint in k-uniswap-v2) are being run all at once, this introduces a configurable parameter (MEMORY_HEADROOM), that ensures that parallel will not start a new job if less than MEMORY_HEADROOM free RAM is available.

[asymmetric]

LGTM apart from a couple nits, but can we document this in the README? Maybe in the Limits section.

[asymmetric]

Oh, and it's not clear to me if --retries is necessary when a job is killed by parallel.

If less than size bytes are free, no more jobs will be started. If less than 50%
size bytes are free, the youngest job will be killed, and put back on the queue to be run later.

--retries must be set to determine how many times GNU parallel should retry a given job.

[d-xo]

nice catch re: --retries, and it seems as though there are some CI failures with this change, wonder if that's the reason.

However, I'm not sure if --retries is the behaviour that we want:

--retries n

If a job fails, retry it on another computer on which it has not failed. Do this n times. If there are fewer than n computers in --sshlogin GNU parallel will re-use all the computers. This is useful if some jobs fail for no apparent reason (such as network failure).