diff --git a/docker/Jenkinsfile b/docker/Jenkinsfile index 4eb8d1f0a601610ce1a3d6df9542758d2ca005e0..a165256948305d205b6802a963203b82494f9a16 100644 --- a/docker/Jenkinsfile +++ b/docker/Jenkinsfile @@ -8,7 +8,7 @@ pipeline { DOCKER_TAG='finn_ci:$BUILD_ID' DOCKER_INST_NAME='finn_ci_$BUILD_ID' BUILD_PATH='/tmp/finn_ci_$BUILD_ID' - DOCKER_CMD="python setup.py test --addopts '-k test_compilation_trafo'" + DOCKER_CMD="python setup.py test" } stages { stage("Clone") { diff --git a/docker/launch-jenkins.sh b/docker/launch-jenkins.sh index 72a3758dc0fb206e5e156075cb7f461741607502..0a366df65dcf2d5dba05dc6dac4a51cf7f53642f 100644 --- a/docker/launch-jenkins.sh +++ b/docker/launch-jenkins.sh @@ -1,11 +1,19 @@ #!/bin/bash -: ${JUPYTER_PORT=8888} -: ${JENKINS_USER=jenkins} -: ${JENKINS_PORT=8080} -: ${JENKINS_HOME=$(pwd)/jenkins_home} +# defaults, can be overriden by environment variables +# user to run Jenkins as -- see NOTE below regarding Docker access permissions +JENKINS_USER ?= jenkins +# port for Jenkins on host machine +JENKINS_PORT ?= 8080 +# make Jenkins config persistent by mounting into this folder +JENKINS_HOME ?= $(pwd)/jenkins_home mkdir -p $JENKINS_HOME +# build a Jenkins Docker image that also has the Docker CLI installed docker build -t finn_jenkins -f Dockerfile.jenkins . + +# launch Docker container mounted to local Docker socket +# NOTE: we allow customizing the user (e.g. as root) to work around permission +# issues, may not al docker run -u $JENKINS_USER -p $JENKINS_PORT:8080 -v /var/run/docker.sock:/var/run/docker.sock -v $JENKINS_HOME:/var/jenkins_home finn_jenkins