You are viewing a plain text version of this content. The canonical link for it is here.
Posted to commits@tvm.apache.org by GitBox <gi...@apache.org> on 2021/05/26 22:19:44 UTC
[GitHub] [tvm] mehrdadh opened a new pull request #8144: [Docker] Add external directory mount
mehrdadh opened a new pull request #8144:
URL: https://github.com/apache/tvm/pull/8144
This PR:
- Adds external directory mount option to `docker/bash.sh`
--
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
For queries about this service, please contact Infrastructure at:
users@infra.apache.org
[GitHub] [tvm] mehrdadh commented on a change in pull request #8144: [Docker] Add external directory mount
Posted by GitBox <gi...@apache.org>.
mehrdadh commented on a change in pull request #8144:
URL: https://github.com/apache/tvm/pull/8144#discussion_r644145200
##########
File path: docker/bash.sh
##########
@@ -46,6 +46,16 @@ if [[ "$1" == "--net=host" ]]; then
shift 1
fi
+# Mount external directory to the docker
+CI_DOCKER_MOUNT_DIR=( )
+CI_DOCKER_MOUNT_CMD=""
+if [[ "$1" == "--mount" ]]; then
+ shift 1
+ CI_DOCKER_MOUNT_DIR+="$1"
+ shift 1
+ CI_DOCKER_MOUNT_CMD="--mount type=bind,source=${CI_DOCKER_MOUNT_DIR},target=${CI_DOCKER_MOUNT_DIR}"
Review comment:
changed the `CI_DOCKER_MOUNT_CMD `.
Regarding to -v vs mound, docker website recommends using mount option since it has a better readable syntax and easier to use. But I don't have a preference.
--
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
For queries about this service, please contact Infrastructure at:
users@infra.apache.org
[GitHub] [tvm] mehrdadh commented on a change in pull request #8144: [Docker] Add external directory mount
Posted by GitBox <gi...@apache.org>.
mehrdadh commented on a change in pull request #8144:
URL: https://github.com/apache/tvm/pull/8144#discussion_r644224296
##########
File path: docker/bash.sh
##########
@@ -46,6 +46,16 @@ if [[ "$1" == "--net=host" ]]; then
shift 1
fi
+# Mount external directory to the docker
+CI_DOCKER_MOUNT_DIR=( )
+CI_DOCKER_MOUNT_CMD=""
+if [[ "$1" == "--mount" ]]; then
+ shift 1
+ CI_DOCKER_MOUNT_DIR+="$1"
+ shift 1
+ CI_DOCKER_MOUNT_CMD="--mount type=bind,source=${CI_DOCKER_MOUNT_DIR},target=${CI_DOCKER_MOUNT_DIR}"
Review comment:
makes sense. Changed it to -v.
thanks!
--
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
For queries about this service, please contact Infrastructure at:
users@infra.apache.org
[GitHub] [tvm] mherkazandjian commented on pull request #8144: [Docker] Add external directory mount
Posted by GitBox <gi...@apache.org>.
mherkazandjian commented on pull request #8144:
URL: https://github.com/apache/tvm/pull/8144#issuecomment-852190462
@leandron
The variable ``EXTRA_MOUNTS`` is set as an empty list here
https://github.com/apache/tvm/blob/cc7307d2eca52cafe0aabdc9c4cebb5497097540/docker/bash.sh#L151
and hence does not inhert (or append) values from the environment. The change by @mehrdadh is quite useful. I was
planning to work on this myself, i think this will be quite handy since many people use the ci containers for development too.
--
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
For queries about this service, please contact Infrastructure at:
users@infra.apache.org
[GitHub] [tvm] mehrdadh commented on pull request #8144: [Docker] Add external directory mount
Posted by GitBox <gi...@apache.org>.
mehrdadh commented on pull request #8144:
URL: https://github.com/apache/tvm/pull/8144#issuecomment-849159158
cc @areusch
--
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
For queries about this service, please contact Infrastructure at:
users@infra.apache.org
[GitHub] [tvm] areusch commented on a change in pull request #8144: [Docker] Add external directory mount
Posted by GitBox <gi...@apache.org>.
areusch commented on a change in pull request #8144:
URL: https://github.com/apache/tvm/pull/8144#discussion_r643222899
##########
File path: docker/bash.sh
##########
@@ -46,6 +46,16 @@ if [[ "$1" == "--net=host" ]]; then
shift 1
fi
+# Mount external directory to the docker
+CI_DOCKER_MOUNT_DIR=( )
+CI_DOCKER_MOUNT_CMD=""
+if [[ "$1" == "--mount" ]]; then
+ shift 1
+ CI_DOCKER_MOUNT_DIR+="$1"
+ shift 1
+ CI_DOCKER_MOUNT_CMD="--mount type=bind,source=${CI_DOCKER_MOUNT_DIR},target=${CI_DOCKER_MOUNT_DIR}"
Review comment:
i guess this is the same as `-v`, but wondering if we should be consistent everywhere and use `-v` here in case there are differences in the way those two options are handled with past versions of docker?
also, can you use array syntax and quote, in case CI_DOCKER_MOUNT_DIR contains spaces?
`CI_DOCKER_MOUNT_CMD=( "--mount" "type=bind,source=${CI_DOCKER_MOUNT_DIR},target=${CI_DOCKER_MOUNT_DIR}" )`
and later:
`"${CI_DOCKER_MOUNT_CMD[@]}"`
--
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
For queries about this service, please contact Infrastructure at:
users@infra.apache.org
[GitHub] [tvm] mehrdadh commented on pull request #8144: [Docker] Add external directory mount
Posted by GitBox <gi...@apache.org>.
mehrdadh commented on pull request #8144:
URL: https://github.com/apache/tvm/pull/8144#issuecomment-849776217
@leandron Thanks for point that out, I just notice this feature.
Not sure if EXTRA_MOUNTS works as intended. My understanding is that when you run the `docker/bash.sh` from another git repository, EXTRA_MOUNTS should mount the external repository? I printed EXTRA_MOUNTS and it's empty.
--
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
For queries about this service, please contact Infrastructure at:
users@infra.apache.org
[GitHub] [tvm] mehrdadh commented on a change in pull request #8144: [Docker] Add external directory mount
Posted by GitBox <gi...@apache.org>.
mehrdadh commented on a change in pull request #8144:
URL: https://github.com/apache/tvm/pull/8144#discussion_r645850302
##########
File path: docker/bash.sh
##########
@@ -154,6 +162,7 @@ ${DOCKER_BINARY} run --rm --pid=host\
${WORKSPACE_VOLUMES}\
-v ${WORKSPACE}:/workspace \
-v ${SCRIPT_DIR}:/docker \
+ -v ${CI_DOCKER_MOUNT_DIR}:${CI_DOCKER_MOUNT_DIR} \
Review comment:
thanks for pointing out. I changed the command to be empty when --mount is not available.
--
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
For queries about this service, please contact Infrastructure at:
users@infra.apache.org
[GitHub] [tvm] areusch commented on pull request #8144: [Docker] Add external directory mount
Posted by GitBox <gi...@apache.org>.
areusch commented on pull request #8144:
URL: https://github.com/apache/tvm/pull/8144#issuecomment-857156340
thanks @mehrdadh , the PR is now merged!
--
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
For queries about this service, please contact Infrastructure at:
users@infra.apache.org
[GitHub] [tvm] areusch merged pull request #8144: [Docker] Add external directory mount
Posted by GitBox <gi...@apache.org>.
areusch merged pull request #8144:
URL: https://github.com/apache/tvm/pull/8144
--
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
For queries about this service, please contact Infrastructure at:
users@infra.apache.org
[GitHub] [tvm] mehrdadh edited a comment on pull request #8144: [Docker] Add external directory mount
Posted by GitBox <gi...@apache.org>.
mehrdadh edited a comment on pull request #8144:
URL: https://github.com/apache/tvm/pull/8144#issuecomment-849776217
@leandron Thanks for pointing that out, I just notice this feature.
Not sure if EXTRA_MOUNTS works as intended. My understanding is that when you run the `docker/bash.sh` from another git repository, EXTRA_MOUNTS should mount the external repository? I printed EXTRA_MOUNTS and it's empty.
--
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
For queries about this service, please contact Infrastructure at:
users@infra.apache.org
[GitHub] [tvm] areusch commented on a change in pull request #8144: [Docker] Add external directory mount
Posted by GitBox <gi...@apache.org>.
areusch commented on a change in pull request #8144:
URL: https://github.com/apache/tvm/pull/8144#discussion_r645833765
##########
File path: docker/bash.sh
##########
@@ -154,6 +162,7 @@ ${DOCKER_BINARY} run --rm --pid=host\
${WORKSPACE_VOLUMES}\
-v ${WORKSPACE}:/workspace \
-v ${SCRIPT_DIR}:/docker \
+ -v ${CI_DOCKER_MOUNT_DIR}:${CI_DOCKER_MOUNT_DIR} \
Review comment:
i think you need to handle the case where --mount is not given
--
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
For queries about this service, please contact Infrastructure at:
users@infra.apache.org
[GitHub] [tvm] areusch commented on a change in pull request #8144: [Docker] Add external directory mount
Posted by GitBox <gi...@apache.org>.
areusch commented on a change in pull request #8144:
URL: https://github.com/apache/tvm/pull/8144#discussion_r644147330
##########
File path: docker/bash.sh
##########
@@ -46,6 +46,16 @@ if [[ "$1" == "--net=host" ]]; then
shift 1
fi
+# Mount external directory to the docker
+CI_DOCKER_MOUNT_DIR=( )
+CI_DOCKER_MOUNT_CMD=""
+if [[ "$1" == "--mount" ]]; then
+ shift 1
+ CI_DOCKER_MOUNT_DIR+="$1"
+ shift 1
+ CI_DOCKER_MOUNT_CMD="--mount type=bind,source=${CI_DOCKER_MOUNT_DIR},target=${CI_DOCKER_MOUNT_DIR}"
Review comment:
i think we should maintain one convention for this file. since we are bind-mounting, it's probably fine to just keep using `-v`. but if you want to change the others for readability, you can too.
--
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
For queries about this service, please contact Infrastructure at:
users@infra.apache.org