implement soft memory limit for docker to use when invoking cpp2v - #103
simon-skylabs wants to merge 1 commit into
Conversation
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | f50d261 |
| fmdeps/BRiCk/ | main | 1a4e474 |
| fmdeps/auto/ | main | 58eae4b |
| fmdeps/auto-docs/ | main | f3ece99 |
| bluerock/NOVA/ | skylabs-proof | 488788c |
| bluerock/bhv/ | skylabs-main | ee95a75 |
| fmdeps/ci/ | main | 555a549 |
| vendored/elpi/ | skylabs-master | c0b9653 |
| vendored/flocq/ | skylabs-master | cf9cc84 |
| fmdeps/fm-tools/ | main | 70842c3 |
| psi/protos/ | main | 8fe3e7c |
| psi/backend/ | main | 8f2a32f |
| psi/ide/ | main | 6b596cf |
| psi/data/ | main | 8cd3ea7 |
| vendored/rocq/ | skylabs-master | bef7df5 |
| fmdeps/rocq-agent-toolkit/ | main | 53d9eb0 |
| vendored/rocq-elpi/ | skylabs-master | be1ffc5 |
| vendored/rocq-equations/ | skylabs-main | d1f944a |
| vendored/rocq-ext-lib/ | skylabs-master | a31ad69 |
| vendored/rocq-iris/ | skylabs-master | a7af9f7 |
| vendored/rocq-lsp/ | skylabs-main | 64ef78a |
| vendored/rocq-stdlib/ | skylabs-master | 00897b3 |
| vendored/rocq-stdpp/ | skylabs-master | 0c5e505 |
| fmdeps/skylabs-fm/ | main | 133e53a |
| vendored/vsrocq/ | skylabs-main | ee79e7a |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| +0.00% | 140849.7 | 140849.7 | +0.0 | total |
| +0.00% | 33024.2 | 33024.2 | +0.0 | ├ translation units |
| +0.00% | 107825.5 | 107825.5 | +0.0 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| +0.00% | 140849.7 | 140849.7 | +0.0 | total |
| +0.00% | 33024.2 | 33024.2 | +0.0 | ├ translation units |
| +0.00% | 107825.5 | 107825.5 | +0.0 | └ proofs and tests |
| (../cpp2v_docker as cpp2v)) | ||
| (env-vars | ||
| ; (CPP2V_DOCKER_ENABLED "if-libstdc++") | ||
| (CPP2V_DOCKER_MEM_CAP=5GB) |
There was a problem hiding this comment.
I think this belongs to the user environment, not the static config...
There was a problem hiding this comment.
I thought I'd provide a sensible default or any easy way to turn it on. We could comment it out and let the user uncomment and change it they want.
There was a problem hiding this comment.
I'd rather keep customizations out of dune as far as possible, so there's less to merge. People can export CPP2V_DOCKER_MEM_CAP=5GB in their normal configs if they want to. Having to configure it twice in dune syntax, and merge customizations with upstream changes, seems a bit too much.
Ideally, dune should either not exist or coincide with dune.disabled. Not sure about "if-libstdc++".
There was a problem hiding this comment.
And I think the only sensible default is off — "wait for ~5GB free to start cpp2v" makes some sense, but if I give 40GB to Docker, that means CPP2V_DOCKER_MEM_CAP should be 35GB.
Anyway, I wanted to approve and merging this for now ASAP, but I noticed other things that need tweaking.
| exit 2 | ||
| fi | ||
| while true; do | ||
| used_mem=$(docker stats --no-stream --format "{{.MemUsage}}" | awk '{print $1}' | head -n 1 | units) |
There was a problem hiding this comment.
This is printing the memory usage of the first container in the list. That can't be good.
2 participants
No description provided.