Skip to content

Commit

Permalink
Fix docker file
Browse files Browse the repository at this point in the history
  • Loading branch information
@gugavaro
gugavaro committed Sep 4, 2018
1 parent 4c7a736 commit 339c871
Show file tree
Hide file tree
Showing 3 changed files with 143 additions and 96 deletions.
211 changes: 119 additions & 92 deletions .docker/build/build.sh
View file
Expand Up @@ -5,6 +5,7 @@
target=$1
out_file=$2
threads=$3
branchname=$4

function export_home() {
if command -v cygpath >/dev/null 2>&1; then
Expand All @@ -15,82 +16,103 @@ function export_home() {
}

function hacl_test() {
fetch_and_make_kremlin && \
fetch_and_make_mlcrypto && \
fetch_mitls && \
export_home OPENSSL "$(pwd)/mlcrypto/openssl" && \
make -j $threads ci -k
fetch_and_make_kremlin &&
fetch_and_make_mlcrypto &&
fetch_mitls &&
fetch_and_make_vale &&
export_home OPENSSL "$(pwd)/mlcrypto/openssl" &&
env VALE_SCONS_PARALLEL_OPT="-j $threads" make -j $threads ci -k
}

function hacl_test_and_hints() {
hacl_test && refresh_hacl_hints
hacl_test && refresh_hacl_hints
}

function fetch_and_make_kremlin() {
fetch_kremlin
# Default build target is minimal, unless specified otherwise
local localTarget
if [[ $1 == "" ]]; then
localTarget="minimal"
else
localTarget="$1"
fi
make -C kremlin -j $threads $localTarget || \
(cd kremlin && git clean -fdx && make -j $threads $localTarget)
OTHERFLAGS='--admit_smt_queries true' make -C kremlin/kremlib -j $threads
export PATH="$(pwd)/kremlin:$PATH"
fetch_kremlin
# Default build target is minimal, unless specified otherwise
local localTarget
if [[ $1 == "" ]]; then
localTarget="minimal"
else
localTarget="$1"
fi
make -C kremlin -j $threads $localTarget ||
(cd kremlin && git clean -fdx && make -j $threads $localTarget)
OTHERFLAGS='--admit_smt_queries true' make -C kremlin/kremlib -j $threads
export PATH="$(pwd)/kremlin:$PATH"
}

# By default, kremlin master works against F* stable. Can also be overridden.
function fetch_kremlin() {
if [ ! -d kremlin ]; then
git clone https://github.com/FStarLang/kremlin kremlin
fi
cd kremlin
git fetch origin
local ref=$( if [ -f ../.kremlin_version ]; then cat ../.kremlin_version | tr -d '\r\n'; else echo origin/master; fi )
echo Switching to KreMLin $ref
git reset --hard $ref
cd ..
export_home KREMLIN "$(pwd)/kremlin"
if [ ! -d kremlin ]; then
git clone https://github.com/FStarLang/kremlin kremlin
fi
cd kremlin
git fetch origin
local ref=$(if [ -f ../.kremlin_version ]; then cat ../.kremlin_version | tr -d '\r\n'; else echo origin/master; fi)
echo Switching to KreMLin $ref
git reset --hard $ref
cd ..
export_home KREMLIN "$(pwd)/kremlin"
}

function fetch_and_make_mlcrypto() {
fetch_mlcrypto
make -C mlcrypto -j $threads
fetch_mlcrypto
make -C mlcrypto -j $threads
}

function fetch_mlcrypto() {
if [ ! -d mlcrypto ]; then
git clone https://github.com/project-everest/MLCrypto mlcrypto
fi
cd mlcrypto
git fetch origin
local ref=$( if [ -f ../.mlcrypto_version ]; then cat ../.mlcrypto_version | tr -d '\r\n'; else echo origin/master; fi )
echo Switching to MLCrypto $ref
git reset --hard $ref
git submodule update
cd ..
export_home MLCRYPTO "$(pwd)/mlcrypto"
if [ ! -d mlcrypto ]; then
git clone https://github.com/project-everest/MLCrypto mlcrypto
fi
cd mlcrypto
git fetch origin
local ref=$(if [ -f ../.mlcrypto_version ]; then cat ../.mlcrypto_version | tr -d '\r\n'; else echo origin/master; fi)
echo Switching to MLCrypto $ref
git reset --hard $ref
git submodule update
cd ..
export_home MLCRYPTO "$(pwd)/mlcrypto"
}

# By default, mitls-fstar master works against F* stable. Can also be overridden.
function fetch_mitls() {
if [ ! -d mitls-fstar ]; then
git clone https://github.com/mitls/mitls-fstar mitls-fstar
fi
cd mitls-fstar
git fetch origin
local ref=$( if [ -f ../.mitls_version ]; then cat ../.mitls_version | tr -d '\r\n'; else echo origin/master; fi )
echo Switching to mitls-fstar $ref
git reset --hard $ref
git clean -fdx
cd ..
export_home MITLS "$(pwd)/mitls-fstar"
if [ ! -d mitls-fstar ]; then
git clone https://github.com/mitls/mitls-fstar mitls-fstar
fi
cd mitls-fstar
git fetch origin
local ref=$(if [ -f ../.mitls_version ]; then cat ../.mitls_version | tr -d '\r\n'; else echo origin/master; fi)
echo Switching to mitls-fstar $ref
git reset --hard $ref
git clean -fdx
cd ..
export_home MITLS "$(pwd)/mitls-fstar"
}

function fetch_vale() {
# NOTE: the name of the directory where Vale is downloaded MUST NOT be vale, because the latter already exists
# so let's call it valebin
if [ ! -d valebin ]; then
git clone https://github.com/project-everest/vale valebin
fi
cd valebin
git fetch origin
local ref=$(if [ -f ../.vale_version ]; then cat ../.vale_version | tr -d '\r\n'; else echo origin/master; fi)
echo Switching to Vale $ref
git reset --hard $ref
cd ..
export_home VALE "$(pwd)/valebin"
}

function fetch_and_make_vale() {
fetch_vale
python3.6 $(which scons) -C valebin -j $threads
}

function refresh_hacl_hints() {
refresh_hints "git@github.com:mitls/hacl-star.git" "true" "regenerate hints" "."
refresh_hints "git@github.com:mitls/hacl-star.git" "true" "regenerate hints" "."
}

# Note: this performs an _approximate_ refresh of the hints, in the sense that
Expand All @@ -99,73 +121,78 @@ function refresh_hacl_hints() {
# reset to origin/$CI_BRANCH, take in our hints, and push. This is short enough that
# the chances of someone merging in-between fetch and push are low.
function refresh_hints() {
local remote=$1
local extra="$2"
local msg="$3"
local hints_dir="$4"

# Add all the hints, even those not under version control
find $hints_dir -iname '*.hints' -and -not -path '*/.*' -and -not -path '*/dependencies/*' | xargs git add

# Without the eval, this was doing weird stuff such as,
# when $2 = "git ls-files src/ocaml-output/ | xargs git add",
# outputting the list of files to stdout
eval "$extra"

git commit --allow-empty -m "[CI] $msg"
# Memorize that commit
commit=$(git rev-parse HEAD)
# Drop any other files that were modified as part of the build (e.g.
# parse.fsi)
git reset --hard HEAD
# Move to whatever is the most recent master (that most likely changed in the
# meantime)
git fetch
git checkout $CI_BRANCH
git reset --hard origin/$CI_BRANCH
# Silent, always-successful merge
export GIT_MERGE_AUTOEDIT=no
git merge $commit -Xtheirs
# Push.
git push $remote $CI_BRANCH
local remote=$1
local extra="$2"
local msg="$3"
local hints_dir="$4"

# Figure out the branch
CI_BRANCH=$branchname
echo "Current branch_name=$CI_BRANCH"

# Add all the hints, even those not under version control
find $hints_dir -iname '*.hints' -and -not -path '*/.*' -and -not -path '*/dependencies/*' | xargs git add

# Without the eval, this was doing weird stuff such as,
# when $2 = "git ls-files src/ocaml-output/ | xargs git add",
# outputting the list of files to stdout
eval "$extra"

git commit --allow-empty -m "[CI] $msg"
# Memorize that commit
commit=$(git rev-parse HEAD)
# Drop any other files that were modified as part of the build (e.g.
# parse.fsi)
git reset --hard HEAD
# Move to whatever is the most recent master (that most likely changed in the
# meantime)
git fetch
git checkout $CI_BRANCH
git reset --hard origin/$CI_BRANCH
# Silent, always-successful merge
export GIT_MERGE_AUTOEDIT=no
git merge $commit -Xtheirs
# Push.
git push $remote $CI_BRANCH
}

function exec_build () {
function exec_build() {
cd hacl-star

export_home FSTAR "$(pwd)/../"
result_file="../result.txt"
local status_file="../status.txt"
echo -n false > $status_file
echo -n false >$status_file

if [ ! -d "secure_api" ]; then
echo "I don't seem to be in the right directory, bailing"
echo Failure > $result_file
echo Failure >$result_file
return
fi

export_home HACL "$(pwd)"
export_home EVERCRYPT "$(pwd)/providers"

if [[ $target == "hacl-ci" ]]; then
echo target -> hacl-ci
hacl_test && echo -n true > $status_file;
echo target - >hacl-ci
hacl_test &&
echo -n true >$status_file
elif [[ $target == "hacl-nightly" ]]; then
echo target -> hacl-nightly
echo target - >hacl-nightly
export OTHERFLAGS="--record_hints $OTHERFLAGS --z3rlimit_factor 2"
hacl_test_and_hints && echo -n true > $status_file;
hacl_test_and_hints && echo -n true >$status_file
else
echo "Invalid target"
echo Failure > $result_file
echo Failure >$result_file
return
fi

if [[ $(cat $status_file) != "true" ]]; then
echo "Build failed"
echo Failure > $result_file
echo Failure >$result_file
else
echo "Build succeeded"
echo Success > $result_file
echo Success >$result_file
fi

cd ..
Expand Down
1 change: 1 addition & 0 deletions .docker/build/build_helper.sh
View file
Expand Up @@ -3,6 +3,7 @@
target=$1
out_file=$2
threads=$3
branchname=$4

tail -f $out_file &
tail_pd=$!
Expand Down
27 changes: 23 additions & 4 deletions .docker/build/linux/Dockerfile
View file
Expand Up @@ -13,9 +13,13 @@ FROM fstar-linux:${COMMITID}
ARG BUILDLOGFILE
ARG MAXTHREADS
ARG TARGET
ARG BRANCHNAME
ARG COMMITID

RUN export FSTAR_HOME=${MYHOME}/FStar

WORKDIR ${MYHOME}/FStar

# Do some cleanup
RUN rm -rf hacl-star
RUN rm -rf hacl-star-old
Expand All @@ -37,17 +41,29 @@ RUN rm -f commitinfofilename.json
RUN mkdir ${MYHOME}/FStar/hacl-star
COPY --chown=everest / ${MYHOME}/FStar/hacl-star/

# Hacl make calls git clean, which will delete buildlogfile.txt
# Because of that we will first output on the parent folder
WORKDIR ${MYHOME}/FStar
# Do another cleanup
RUN rm ${MYHOME}/FStar/hacl-star/Dockerfile
RUN rm ${MYHOME}/FStar/hacl-star/build_helper.sh
RUN rm ${MYHOME}/FStar/hacl-star/build.sh
RUN rm ${MYHOME}/FStar/hacl-star/id_rsa
RUN rm ${MYHOME}/FStar/hacl-star/commitinfofilename.json

# ADD SSH KEY
RUN mkdir -p ${MYHOME}/.ssh
RUN chown everest ${MYHOME}/.ssh
RUN chmod 700 ${MYHOME}/.ssh
COPY --chown=everest id_rsa ${MYHOME}/.ssh/id_rsa
RUN chmod 600 ${MYHOME}/.ssh/id_rsa
RUN eval $(ssh-agent)

COPY --chown=everest build.sh ${MYHOME}/FStar/build.sh
RUN chmod +x build.sh
COPY --chown=everest build_helper.sh ${MYHOME}/FStar/build_helper.sh
RUN chmod +x build_helper.sh

RUN echo $(date -u '+%Y-%m-%d %H:%M:%S') >> ${BUILDLOGFILE}
RUN ./build_helper.sh ${TARGET} ${BUILDLOGFILE} ${MAXTHREADS} || true
RUN echo "FStar version => ${COMMITID}" >> ${BUILDLOGFILE}
RUN ./build_helper.sh ${TARGET} ${BUILDLOGFILE} ${MAXTHREADS} ${BRANCHNAME} || true
RUN echo $(date -u '+%Y-%m-%d %H:%M:%S') >> ${BUILDLOGFILE}

# Generate query-stats.
Expand All @@ -57,3 +73,6 @@ RUN bash -c ".scripts/query-stats.py -f ${BUILDLOGFILE} -F html -o log_no_replay
# Worst offenders (longest times)
RUN bash -c ".scripts/query-stats.py -f ${BUILDLOGFILE} -F html -o log_worst.html -c -g -n 10"

# Remove ssh identities.
RUN rm ${MYHOME}/.ssh/id_rsa
RUN eval $(ssh-agent) && ssh-add -D

0 comments on commit 339c871

Please sign in to comment.