-
Notifications
You must be signed in to change notification settings - Fork 63
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.
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
Get RPC Java proofs working under Docker #1457
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A couple of suggestions, but otherwise this looks just fine.
@@ -44,6 +45,7 @@ popd | |||
echo "killing saw-remote-api docker container" | |||
|
|||
docker container kill saw-remote-api | |||
docker container rm saw-remote-api |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
These two cleanup lines will only be run when the test is successful, but not when it fails for some reason. This may not be as important when these are done in a CI environment that discards the entire CI container at the end of the run, but to avoid this for situations where that's not the case, I'd recommend removing these and adding to the beginning of the file:
cleanup () {
docker container kill saw-remote-api || true
docker container rm saw-remote-api || true
}
trap cleanup EXIT
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I guess you'd want to move the preceding echo
as well..
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah, good idea!
@@ -9,6 +9,7 @@ TAG=${1:-saw-remote-api} | |||
pushd $DIR/.. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I realize this wasn't changed in this particular PR, but in general I avoid the use of pushd/popd
and instead use the following pattern:
( cd newdir;
do_things_in_newdir;
more_things;
)
There are two advantages to using this pattern instead: 1) You don't inadvertently forget a popd
and a missing )
will be a bash
syntax error and more visible, and 2) the pushd/popd
aren't always available in all shells.
I'm not necessarily indicating this should be added to this PR, but since you're here, this might be a good time to make this change if you wanted it.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Another recommendation is to avoid using $DIR/..
if possible, since the ..
may move up to an unexpected location if there are links or mount points involved. While that's unlikely in this case, $DIR
was obtained from (effectively) ... dirname $0 ...
, so setting DIR from dirname $(dirname $0)
might be a better approach.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Also good suggestions. I can draft another PR to make some cleanups to Docker-related things. There are some other failures in that space that have been happening on the nightly builds, and this would fit well with those.
Oh, I didn't realize by approving mergebot would be going ahead with the merge. Whoops. |
No description provided.