From e786a577048b050839072ce2963eeaf6ab2d2a17 Mon Sep 17 00:00:00 2001
From: Yaman Umuroglu <maltanar@gmail.com>
Date: Tue, 21 Apr 2020 17:24:34 +0100
Subject: [PATCH] [Jenkins] add comments in launch-jenkins, run entire test
suite
---
docker/Jenkinsfile | 2 +-
docker/launch-jenkins.sh | 16 ++++++++++++----
2 files changed, 13 insertions(+), 5 deletions(-)
diff --git a/docker/Jenkinsfile b/docker/Jenkinsfile
index 4eb8d1f0a..a16525694 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 72a3758dc..0a366df65 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
--
GitLab