Skip to content

implement soft memory limit for docker to use when invoking cpp2v #103

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
simon-skylabs wants to merge 1 commit into
base: main
Choose a base branch
from
Open

implement soft memory limit for docker to use when invoking cpp2v #103

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions dune.disabled
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@
(../cpp2v_docker as cpp2v))
(env-vars
; (CPP2V_DOCKER_ENABLED "if-libstdc++") ; This will call `cpp2v` through `docker` only for files that require `libstdc++`
(CPP2V_DOCKER_MEM_CAP=5GB)
(CPP2V_DOCKER_ENABLED "y") ; This will use docker for all calls of `cpp2v`
))))

Expand All @@ -19,4 +20,5 @@
(../cpp2v_docker as cpp2v))
(env-vars
; (CPP2V_DOCKER_ENABLED "if-libstdc++")
(CPP2V_DOCKER_MEM_CAP=5GB)

@pgiarrusso-sl pgiarrusso-sl Jul 13, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this belongs to the user environment, not the static config...

@simon-skylabs simon-skylabs Jul 16, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

@pgiarrusso-sl pgiarrusso-sl Jul 17, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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++".

@pgiarrusso-sl pgiarrusso-sl Jul 17, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

(CPP2V_DOCKER_ENABLED "y"))))))
25 changes: 25 additions & 0 deletions rocq-brick-libstdcpp/cpp2v_docker.in
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
#!/usr/bin/env bash

REALPATH=$(which grealpath || which realpath)
SED=$(which gsed || which sed)
REL_PATH="$($REALPATH `pwd` --relative-to "$DUNE_SOURCEROOT")"

map_absolute_paths () {
Expand Down Expand Up @@ -46,6 +47,15 @@ if [ "$CPP2V_DOCKER_ENABLED" = "y" ] && ! which docker > /dev/null; then
:
fi

units () {
local pat='s/G/000M/;s/M/000K/;s/K/000B/;s/B//g'
if [[ $# -eq 1 ]]; then
echo "$1" | $SED $pat
else
$SED $pat
fi
}

if [ "$CPP2V_DOCKER_ENABLED" = "y" ] && which docker > /dev/null; then
if [ -z "$CPP2V_DOCKER_IMAGE" ]; then
# We skip the warning if no docker is available
Expand All @@ -61,6 +71,21 @@ if [ "$CPP2V_DOCKER_ENABLED" = "y" ] && which docker > /dev/null; then
ARGS+=( "--workdir" "$BRICK_LIBCPP/$REL_PATH" )
ARGS+=( $(map_absolute_paths "$@") )

if [[ -n "$CPP2V_DOCKER_MEM_CAP" ]]; then
MEM_CAP=$(units $CPP2V_DOCKER_MEM_CAP)
if ! [[ $MEM_CAP =~ [0-9]+ ]]; then
echo "Misconfiguration: CPP2V_DOCKER_MEM_CAP = '$CPP2V_DOCKER_MEM_CAP', invalid memory amount"
exit 2
fi
while true; do
used_mem=$(docker stats --no-stream --format "{{.MemUsage}}" | awk '{print $1}' | head -n 1 | units)

@pgiarrusso-sl pgiarrusso-sl Jul 17, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is printing the memory usage of the first container in the list. That can't be good.

if [[ "$used_mem" -lt $MEM_CAP ]]; then
break
fi
sleep 0.01
done
fi

cpp2v_args="$( printf '"%q" ' "$@" )" # ensure each argument is quoted as a whole.
docker run "${ARGS[@]}" "$CPP2V_DOCKER_IMAGE" \
/bin/bash -c 'eval $(opam env)'"; cpp2v $cpp2v_args"
Expand Down