ci

#!/usr/bin/env bash

########################################
#
# - WARNING WARNING WARNING WARNING -
#
#  DO NOT MAKE CHANGES ON THIS FILE!
#
#  IF YOU NEED TO MAKE CHANGES USE THE
#  NEW BUILD SCRIPT !!!
#
########################################

cat <<INFO
This is the Everest CI script.
... called as $0
... working directory is $(pwd)
... environment: $(uname -a)
INFO

# Sorry, everyone
if (( ${BASH_VERSION%%.*} < 4 )); then
  echo "This script requires Bash >= 4. On OSX, try: brew install bash"
  exit 1
fi

# CI runs [bash -c path/to/ci] without [--login]. This makes sure we have /bin
# and /usr/bin first...!
BUILD_DIR=$(pwd)
source /etc/profile
if [[ -f ~/.bash_profile ]]; then
  source ~/.bash_profile
fi
echo "... PATH is $PATH"
cd "$BUILD_DIR"

echo "... z3: $(which z3)"

# Any error is fatal.
set -e
set -o pipefail
# set -x # uncomment for debugging. This also will expose any github access tokens which will invalidate them so use wisely

# Some commands...
if [[ $(uname) = "Darwin" ]]; then
  DATE=gdate
  FIND=gfind
else
  DATE=date
  FIND=find
fi

# Self-update
echo "... trying to self-update"
if [[ ${0##*/} == $0 ]]; then
  pushd $(dirname $(which $0))
else
  pushd $(dirname $0)
fi
OLD_REVISION=$(git rev-parse HEAD)
git fetch
if ! git merge --ff origin/master; then
  echo "WARNING: script cannot self-update"
else
  if [[ $(git rev-parse HEAD) != $OLD_REVISION ]]; then
    echo "... new version of CI script available, updated"
    popd
    $0 "$@"
    exit 0
  else
    echo "... no new version available"
  fi
fi
EVEREST_CI_HOME=$(pwd)
popd

# The parallel option, either empty (by default), or -j n,
# as specified on the command line.
# WARNING: in the latter case, it MUST be interpreted as two words, so
# NEVER quote it as "$PARALLEL_OPT"
# Use $PARALLEL_OPT instead
unset PARALLEL_OPT

# Encode < > & and " in the given string
# The Slack syntax does not require escaping " or \ but JSON does in order to
# form a valid payload.
function quote() {
  local msg="$1"
  msg=${msg//&/&amp;}
  msg=${msg//</&lt;}
  msg=${msg//>/&gt;}
  msg=${msg//\\/\\\\}
  msg=${msg//\"/\\\"}
  echo $msg
}

# Once we have setup the environment, made errors fatal, and self-upgraded (all
# of which should never fail), we try to report any unexpected failure.
#  $1: channel
#  $2: message
function post_to_slack() {
  curl -X POST --data-urlencode "payload={\"channel\": \"$1\", \
    \"username\": \"dzomo\", \"text\": \"$2\", \
    \"icon_emoji\": \":water_buffalo:\"}" "$SLACK_FSTAR_WEBHOOK"
}
trap 'post_to_slack "#everest-build" ":heavy_exclamation_mark: \`$0 $@\` *failed* with error code: $?"' ERR

# Figure out the branch
if [[ $BUILD_SOURCEBRANCHNAME != "" ]]; then
  CI_BRANCH=${BUILD_SOURCEBRANCHNAME##refs/heads/}
  echo "... running in a VSTS environment, branch=$CI_BRANCH"
else
  echo "... trying to figure out the current branch"
  CI_BRANCH=$(git symbolic-ref HEAD) # fails if not on a branch
  CI_BRANCH=${CI_BRANCH##refs/heads/}
  tput setaf 1
  echo "... not running in a VSTS environment, $CI_BRANCH is the working directory's current branch"
  tput sgr0
fi

# Some environment variables we want
export OCAMLRUNPARAM=b
export OTHERFLAGS="--use_hints --query_stats"
export MAKEFLAGS="$MAKEFLAGS -Otarget"

function log_prelude() {
  # Some basic information
  echo "This is $0 $@"
  echo "Working directory: $(pwd)"
  echo "About to run: $build_command"
  echo "BUILD_SOURCEBRANCHNAME: $BUILD_SOURCEBRANCHNAME"
  echo "BUILD_DEFINITIONNAME: $BUILD_DEFINITIONNAME"
  echo "BUILD_BUILDID: $BUILD_BUILDID"
  echo "DEFINITIONNAME: $DEFINITIONNAME"
  echo "Z3 is $(which z3)"
}

# Global variable; if the file is non-empty, build is orange and the message is
# displayed along with the notification
ORANGE_FILE=$(mktemp)
function cleanup () {
  rm $ORANGE_FILE
}
trap cleanup EXIT

# Run a given command and commit & push the logs the the CI_LOGS repository.
# $1: the command to run
# $2: job description without space (e.g. everest-interop or fstar)
# $3: slack channel
# $4: github org/project
# $5: this is a build that uses F*, we can generate query stats for its log
function run_log_commit() {
  if [[ $CI_LOGS == "" ]]; then
    echo "Don't know where to checkout the logs"
    echo "Please specify the location via the CI_LOGS environment variable"
    exit 1
  fi

  local build_command="$1"
  local stem=$2
  local slack_channel=$3
  local github_project=$4
  local fstar_dir=$5

  local slack_commit=$(git rev-parse HEAD | cut -c 1-8)
  local slack_branch=$CI_BRANCH
  local slack_log=$(git log --pretty=format:"%s" -1)
  local slack_author=$(git log --pretty=format:"%cn" -1)

  # Determine where the logs are going
  local unique_id
  if [[ $BUILD_BUILDNUMBER == "" ]]; then
    echo "... probably running locally, generating a random build number"
    unique_id=$RANDOM
  else
    unique_id=$BUILD_BUILDNUMBER
  fi
  local log_all=$stem-$slack_commit-$unique_id.all
  local log_err=$stem-$slack_commit-$unique_id.err
  local log_no_replay=$stem-$slack_commit-$unique_id.no-replay
  local log_worst=$stem-$slack_commit-$unique_id.worst
  local raw_url=https://raw.githubusercontent.com/project-everest/ci-logs/master
  local rawgit_url=https://rawgit.com/project-everest/ci-logs/master

  # The actual CI
  SECONDS=0

  local success
  if ( log_prelude && $build_command ) \
    2> >( \
      while read -r line; do
        echo "$line" >> $CI_LOGS/$log_err;
        echo "$line" >> $CI_LOGS/$log_all
        echo STDERR: "$line" >&2
      done;
    ) \
    > >( \
      while read -r line; do
        echo "$line" >> $CI_LOGS/$log_all
        echo "$line"
      done
    )
  then
    success=true
  else
    echo "ERROR: PIPESTATUS=${PIPESTATUS[@]}"
    success=false
  fi

  # We are not logging things anymore... this is a last resort debugging info
  # that should show up via VSTS
  set -x

  # Generate query-stats if the version of F* is recent enough.
  local failed_hints
  local query_stats_min_html=f1552cbb
  local query_stats_min_csv=704c7a0f
  if [[ $fstar_dir != "" ]]; then
    log_no_replay=$log_no_replay.html
    log_worst=$log_worst.html
    # List the hints that fail to replay.
    $fstar_dir/.scripts/query-stats.py -f $CI_LOGS/$log_all -F html \
      -o $CI_LOGS/$log_no_replay -n all '--filter=fstar_usedhints=+' \
      '--filter=fstar_tag=-' -g
    # Get the number of replay failures.
    local n_failed_hints=$(cat $CI_LOGS/$log_no_replay | grep "# failed (with " | cut -d ">" -f 5 | cut -d "<" -f 1)
    failed_hints="      *A total of $n_failed_hints hints failed to replay* (<$rawgit_url/$log_no_replay|not replayable>, <$rawgit_url/$log_worst|worst offenders>)\n"
    # Worst offenders (longest times)
    $fstar_dir/.scripts/query-stats.py -f $CI_LOGS/$log_all -F html \
                                       -o $CI_LOGS/$log_worst -c -g -n 10
  fi

  # Commit & push the logs. This does not prevent interleaving from concurrent
  # build jobs.
  pushd $CI_LOGS
  export GIT_MERGE_AUTOEDIT=no
  git fetch && git reset --hard origin/master
  for f in "$log_all" "$log_err" "$log_no_replay" "$log_worst"; do
    [[ -f "$f" ]] && git add "$f"
  done
  if $success; then
    git commit -am "[CI] $stem logs (success)"
  else
    git commit -am "[CI] $stem logs (failure)"
  fi
  local pull_success=true
  until git push
  do
    git pull --no-edit || {
      pull_success=false
      break
    }
  done
  $pull_success
  popd

  if [[ $SLACK_FSTAR_WEBHOOK != "" ]]; then
    local slack_time=$(if (( $SECONDS >= 3600 )); then $DATE -d@$SECONDS -u +%Hh%Mm%Ss; else $DATE -d@$SECONDS -u +%Mm%Ss; fi)
    local slack_msg="<$raw_url/$log_err|stderr> <$raw_url/$log_all|stdout+stderr>"
    local slack_name=$(git remote get-url origin)
    slack_name=${slack_name##*/}
    slack_name=${slack_name%.git}
    local slack_os=$(uname)
    local slack_emoji=""
    local slack_type=""
    local slack_breakage=""

    if $success; then
      # Main F* build succeeded
      local orange=$(cat $ORANGE_FILE | xargs echo -n)
      if [[ $orange == "" ]]; then
        # Perfect build, no breakage
        slack_emoji=":white_check_mark:"
        slack_type="success :smile_cat:"
      else
        # Build with breakage, display where the breakage is
        slack_emoji=":fire:"
        slack_type="success with breakage :scream_cat:"
        slack_breakage="      *Breakage:* $orange\n"
      fi
    else
      # Build failure, display the list of modules that failed to verify
      slack_emoji=":no_entry:"
      slack_type="failure :crying_cat_face:"

      # Get all the lines of the form: path\to\foo.fst(111,11-111,11) : (Error...
      # something. Erase the path while at it, keeping the filename only.
      local failed_modules=$(sed -n 's/\(.*[\\\/]\)\?\([^(]*\)[^:]*: (Error.*/\2/p' $CI_LOGS/$log_err | \
        sort | \
        uniq | \
        tr '\r\n' ' ')
      if [[ $failed_modules != "" ]]; then
        slack_breakage="      *There were errors :rage: in:* "$(quote "$failed_modules")"\n"
      fi
    fi

    # The branch *may* be of the form user_foobar
    local maybe_slack_user="${slack_branch%%_*}"

    # Check if the branch has c_ to send to the appropriate channel - otherwise
    # check if the tentative user name is a match using slack-users file
    if [[ ${slack_branch##c_} != $slack_branch ]]; then
      slack_channel=${slack_branch##c_}
      slack_channel="#${slack_channel%%_*}"
    elif egrep ^$maybe_slack_user$ $EVEREST_CI_HOME/slack-users >/dev/null 2>&1; then
      slack_channel="@$maybe_slack_user"
    fi

    # Set up payload. If branch is not c_ or a valid slack name_ then just leave payload as default
    local payload="$slack_emoji \`$build_command\` on <https://github.com/$github_project/commit/$slack_commit|$slack_commit> ($slack_branch) is a *$slack_type*\n\
      *Project:* $slack_name\n\
      *Message:* $(quote "$slack_log")\n\
      *Author:* $slack_author\n\
      *Duration:* $slack_time\n\
      *OS:* $slack_os\n\
      *Logs:* $slack_msg\n$failed_hints$slack_breakage\
      *VSTS Build definition:* $BUILD_DEFINITIONNAME"

    post_to_slack "$slack_channel" "$payload" || echo "Slack notification NOT sent"
  fi

  if ! $success; then
    exit 255
  fi

  set +x
}

# Note: this performs an _approximate_ refresh of the hints, in the sense that
# since the hint refreshing job takes about 80 minutes, it's very likely someone
# merged to $CI_BRANCH in the meanwhile, which would invalidate some hints. So, we
# 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
}

function refresh_fstar_hints() {
  if [ -f ".scripts/git_rm_stale_hints.sh" ]; then
    ./.scripts/git_rm_stale_hints.sh
  fi
  refresh_hints "git@github.com:FStarLang/FStar.git" "git ls-files src/ocaml-output/ | xargs git add" "regenerate hints + ocaml snapshot" "."
}

function refresh_mitls_hints() {
  refresh_hints "git@github.com:mitls/mitls-fstar.git" "true" "regenerate hints" "src"
}

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

function everest_rebuild() {
  if [[ -x /usr/bin/time ]]; then
    gnutime=/usr/bin/time
  else
    gnutime=""
  fi
  git clean -ffdx
  $gnutime ./everest --yes $PARALLEL_OPT $1 check reset make &&
  echo done with check reset make, timing above &&
  $gnutime ./everest --yes $PARALLEL_OPT $1 test &&
  echo done with test, timing above &&
  $gnutime ./everest --yes $PARALLEL_OPT $1 verify &&
  echo done with verify, timing above
}

function everest_move() {
  # This function is called from a test... so it needs to fast-fail because "set
  # -e" does not apply within subshells.

  # VSTS does not clean things properly... no point in fighting that, let's just
  # do it ourselves
  git clean -ffdx
  # Sanity check that will fail if something is off the rails
  ./everest --yes $PARALLEL_OPT check reset || return 1
  # Update every project to its know good version and branch, then for each
  # project run git pull
  source hashes.sh
  source repositories.sh
  local fresh=false
  local versions=""
  local url=""
  for r in ${!hashes[@]}; do
    cd $r
    git pull
    if [[ $(git rev-parse HEAD) != ${hashes[$r]} ]]; then
      fresh=true
      url=${repositories[$r]#git@github.com:}
      url="https://www.github.com/${url%.git}/compare/${hashes[$r]}...$(git rev-parse HEAD)"
      versions="$versions\n    *$r* <$url|moves to $(git rev-parse HEAD | cut -c 1-8)> on branch ${branches[$r]}"
    else
      versions="$versions\n    *$r* stays at $(git rev-parse HEAD | cut -c 1-8) on branch ${branches[$r]}"
    fi
    cd ..
  done
  versions="$versions\n"
  local msg=""
  if ! $fresh; then
    # Bail out early if there's nothing to do
    post_to_slack "#everest-build" ":information_source: *Nightly Everest Upgrade ($CI_BRANCH):* nothing to upgrade"
  elif ! ./everest --yes $PARALLEL_OPT -windows make test verify drop qbuild; then
    # Provide a meaningful summary of what we tried
    msg=":no_entry: *Nightly Everest Upgrade ($CI_BRANCH):* upgrading each project to its latest version breaks the build\n$versions"
    post_to_slack "#everest-build" "$msg"
    return 255
  else
    # Life is good, record new revisions and commit.
    msg=":white_check_mark: *Nightly Everest Upgrade ($CI_BRANCH):* upgrading each project to its latest version works!\n$versions"
    post_to_slack "#everest-build" "$msg"
    git checkout $CI_BRANCH && \
    git pull && \
    ./everest --yes snapshot && \
    git commit -am "[CI] automatic upgrade" && \
    git push git@github.com:project-everest/everest.git $CI_BRANCH || \
    post_to_slack "#everest-build" ":no_entry: *Nightly Everest Upgrade:* could not push fresh commit on branch $CI_BRANCH"

    # Import Vale assemblies into HACL*
    cd hacl-star
    # Ignore other changes (e.g. submodules)
    if ! git diff --exit-code secure_api/vale/asm ; then
      echo "New assemblies from Vale, committing"
      git add -u secure_api/vale/asm
      git commit -m "[CI] New assemblies coming from Vale"
      local commit=$(git rev-parse HEAD)
      local branch=${branches[hacl-star]}
      git fetch
      git reset --hard origin/$branch
      git merge -Xours $commit
      git push
    fi
    cd ..
  fi
}

# Remove unused images left over after the build
# TODO: replace with 'docker image prune' once we upgrade to Docker 1.13
function docker_image_prune () {
  while docker images --quiet --filter dangling=true | xargs docker rmi
  do
    true
  done
}

# Build a Docker image where everything will be built and verified,
# then push it to the Docker Hub as projecteverest/everest
# Requires credentials to access the Docker Hub servers:
# - user name in the DOCKER_HUB_USERNAME environment variable
# - password in the DOCKER_HUB_PASSWORD environment variable
function docker_from_scratch() {
  # First check if the image really needs to be rebuilt
  # Use the commit hash as Docker image metadata
  # and check whether it has changed,
  # or if DOCKER_FORCE_BUILD is nonempty
  current_commit_hash=`git rev-parse HEAD`
  old_commit_hash=`docker inspect --format '{{index .Config.Labels "commit_hash"}}' projecteverest/everest`
  if
    [[ -z ${DOCKER_FORCE_BUILD+x} ]] &&
    [[ "x$current_commit_hash" = "x$old_commit_hash" ]]
  then
    echo Docker image does not need to be rebuilt
    return 0
  fi
  # Then, log into the Docker Hub server
  if [ -z ${DOCKER_HUB_USERNAME+x} ] || [ -z ${DOCKER_HUB_PASSWORD+x} ]
  then
    echo Please specify Docker Hub username and password
    echo using the DOCKER_HUB_USERNAME and DOCKER_HUB_PASSWORD environment variables
    exit 1
  fi
  docker login --username="$DOCKER_HUB_USERNAME" --password="$DOCKER_HUB_PASSWORD" &&
  # Build the Docker image
  docker build --pull --no-cache --rm --tag=projecteverest/everest --build-arg "PARALLEL_OPT=$PARALLEL_OPT" --label "commit_hash=$current_commit_hash" .docker/everest/ &&
  # Push the image onto the Docker Hub
  echo "PIPESTATUS=${PIPESTATUS[@]}" &&
  echo Pushing projecteverest/everest to Docker Hub &&
  {
    # Retrying $retry times
    local retry=5
    until [ $retry -eq 0 ] || docker push projecteverest/everest
    do
      retry=$(($retry - 1))
      echo "Push failed. Number of remaining attempts: $retry"
    done
    [ $retry -ne 0 ]
  } &&
  # Cleanup: log out from Docker Hub and remove intermediate images
  docker logout &&
  docker_image_prune
}

function export_home() {
  if command -v cygpath >/dev/null 2>&1; then
    export $1_HOME=$(cygpath -m "$2")
  else
    export $1_HOME="$2"
  fi
}

# Since many projects may depend on F*, we provide a function to just clone F*
# (by default, the stable branch), unless otherwise specified via the
# .fstar_version file.
function fetch_fstar() {
  if [ ! -d fstar ]; then
    git clone https://github.com/FStarLang/FStar/ fstar
  fi
  cd fstar
  git fetch origin
  local ref=$( if [ -f ../.fstar_version ]; then cat ../.fstar_version | tr -d '\r\n'; else echo origin/stable; fi )
  echo Switching to F* $ref
  git reset --hard $ref
  cd ..
  export_home FSTAR "$(pwd)/fstar"
}

function fetch_and_make_fstar() {
  fetch_fstar
  make -C fstar/src/ocaml-output $PARALLEL_OPT || \
    (git clean -fdx && make -C src/ocaml-output $PARALLEL_OPT) || \
    exit 255
  make -C fstar/ulib/ml $PARALLEL_OPT
  OTHERFLAGS='--admit_smt_queries true' make -C fstar/ulib $PARALLEL_OPT
}

# 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"
}

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

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"
}

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

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

# 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"
}

function fetch_vale() {
  vale_dir="$1"
  if [ -z "$vale_dir" ] ; then
    vale_dir=vale
  fi
  if [ ! -d "$vale_dir" ]; then
    git clone https://github.com/project-everest/vale "$vale_dir"
  fi
  cd "$vale_dir"
  git fetch origin
  echo Switching to vale to fstar_ci
  git clean -fdx .
  git reset --hard origin/fstar_ci
  nuget.exe restore tools/Vale/src/packages.config -PackagesDirectory tools/FsLexYacc
  cd ..
  export_home VALE "$(pwd)/$vale_dir"
}

function build_pki_if() {
  if [[ -d src/pki ]]; then
    make -C src/pki $PARALLEL_OPT
  fi
}

function mitls_verify() {
  export_home MITLS "$(pwd)"
  # Only building a subset of HACL* for now
  fetch_and_make_fstar && fetch_and_make_kremlin all && fetch_hacl && \
    fetch_and_make_mlcrypto && \
    make -C hacl-star/code extract-c $PARALLEL_OPT && \
    OTHERFLAGS="--admit_smt_queries true $OTHERFLAGS" make -C hacl-star/providers $PARALLEL_OPT && \
    make -C hacl-star/secure_api $PARALLEL_OPT && \
    make -C libs/ffi $PARALLEL_OPT && \
    build_pki_if && \
    VERIFY_LOWPARSE=1 make -C src/tls $PARALLEL_OPT all -k && \
    make -C src/tls $PARALLEL_OPT test -k
}

function mitls_verify_and_hints() {
  mitls_verify && refresh_mitls_hints
}

function hacl_test() {
  fetch_and_make_fstar
  fetch_and_make_kremlin
  fetch_and_make_mlcrypto
  fetch_mitls # for mitlsffi.h, sigh
  fetch_vale valebin
  export_home OPENSSL "$(pwd)/mlcrypto/openssl"
  export_home HACL "$(pwd)"
  export VALE_SCONS_PARALLEL_OPT="$PARALLEL_OPT"
  # Build Vale first
  pushd valebin && ./run_scons.sh $PARALLEL_OPT --FSTAR-MY-VERSION && popd &&
  # then build HACL*
  env make $PARALLEL_OPT ci -k
}

function hacl_test_and_hints() {
  hacl_test && refresh_hacl_hints
}

# Parse options. All options should come first, before the operation.
# Currently, only "-j n" is supported.
while true
do
  case "$1" in
    -j)
      # The -j option is in two parts: -j n, where n is the parallel factor
      # (max number of parallel jobs)
      shift
      PARALLEL_OPT="-j $1"
      ;;
    *)
      break
      ;;
  esac
  shift
done

# Runs F* along with some representative tests from other projects. Writes into
# $ORANGE_FILE (since it's called from within a sub-shell).
fstar_and_friends () {
  local target=$1

  # Communication from sub-process shells.
  local out_file=$(mktemp)

  # Warm-up: bootstrap F* and fetch other repositories
  echo -n false > $out_file
  if [[ -x /usr/bin/time ]]; then
    gnutime=/usr/bin/time
  else
    gnutime=""
  fi
  { $gnutime make -C src $PARALLEL_OPT -k utest-prelude && echo -n true > $out_file; } &
  fetch_vale &
  fetch_hacl &
  fetch_and_make_kremlin &
  fetch_mitls &
  wait
  if [[ $(cat $out_file) != "true" ]]; then
    echo "warm-up failed" && rm $out_file && return 1
  fi

  # The commands above were executed in sub-shells and their EXPORTs are not
  # propagated to the current shell. Re-do.
  export_home HACL "$(pwd)/hacl-star"
  export_home KREMLIN "$(pwd)/kremlin"
  export_home FSTAR "$(pwd)"

  # Once F* is built, run its main regression suite, along with more relevant
  # tests.
  echo -n false > $out_file
  { $gnutime make -C src $PARALLEL_OPT -k $target && echo -n true > $out_file; } &

  { cd vale
    if [[ "$OS" == "Windows_NT" ]]; then
        ## This hack for determining the success of a vale run is needed
        ## because somehow scons is not returning the error code properly
        timeout 480 ./scons_cygwin.sh -j 4 --FSTAR-MY-VERSION --MIN_TEST |& tee vale_output
        ## adds "min-test (Vale)" to the ORANGE_FILE
        ##      if this string vvvv is present in vale_output
        ! grep -qi 'scons: building terminated because of errors.' vale_output || echo "min-test (Vale)" >> $ORANGE_FILE
    else
        timeout 480 scons -j 4 --FSTAR-MY-VERSION --MIN_TEST || echo "min-test (Vale)" >> $ORANGE_FILE
    fi
    cd ..
  } &

  { OTHERFLAGS='--warn_error -276 --use_hint_hashes' timeout 480 make -C hacl-star/code/hash/ -j 4 Hacl.Impl.SHA2_256.fst-verify || \
    echo "Hacl.Impl.Hash.SHA2_256.fst-verify (HACL*)" >> $ORANGE_FILE; } &

  { OTHERFLAGS='--use_hint_hashes' timeout 480 make -C hacl-star/secure_api -f Makefile.old -j 4 aead/Crypto.AEAD.Encrypt.fst-ver || \
    echo "Crypto.AEAD.Encrypt.fst-ver (HACL*)" >> $ORANGE_FILE; } &

  # 2018.05.29: removed the hacl-star-old clone, we were using HACL_HOME=$(pwd)/hacl-star-old
  # We now run all (hardcoded) tests in mitls-fstar@master
  { OTHERFLAGS=--use_hint_hashes timeout 480 make -C mitls-fstar/src/tls -j 4 StreamAE.fst-ver || \
    echo "StreamAE.fst-ver (mitls)" >> $ORANGE_FILE;
    OTHERFLAGS=--use_hint_hashes timeout 240 make -C mitls-fstar/src/tls -j 4 Pkg.fst-ver || \
    echo "Pkg.fst-ver (mitls verify)" >> $ORANGE_FILE;
    OTHERFLAGS="--use_hint_hashes --use_extracted_interfaces true" timeout 240 make -C mitls-fstar/src/tls -j 4 Pkg.fst-ver || \
    echo "Pkg.fst-ver with --use_extracted_interfaces true (mitls verify)" >> $ORANGE_FILE;
  } &

  # JP: doesn't work because it leads to uint128 being verified in the wrong Z3
  # context (?) meaning that some proof obligations fail
  # { cd kremlin/test && timeout 480 ../krml -warn-error @4 -static-header FStar -no-prefix \
  #     Test128 Test128.fst -verify -verbose -fnouint128 -tmpdir .output/Test128.out || \
  #   echo "test/Test128.test (KreMLin)" >> $ORANGE_FILE; } &

  # { cd kremlin/test && timeout 480 ../krml -warn-error @4 -add-include '"kremstr.h"' \
  #     main-Server.c -tmpdir .output/Server.out -no-prefix Server -verify \
  #     Server.fst -verbose || \
  #   echo "test/Server.test (KreMLin)" >> $ORANGE_FILE; } &
  wait

  # Make it an orange if there's a git diff. Note: FStar_Version.ml is in the
  # .gitignore.
  echo "Searching for a diff in src/ocaml-output"
  if ! git diff --exit-code --name-only src/ocaml-output; then
    echo "GIT DIFF: the files in the list above have a git diff"
    echo "snapshot-diff (F*)" >> $ORANGE_FILE
  fi

  if [[ $(cat $out_file) != "true" ]]; then
    echo "F* regression failed" && rm $out_file && return 1
  fi

  rm $out_file
}

# Main commands.
case "$1" in
  fstar-ci)
    if [ ! -d ulib ]; then
      echo "I don't seem to be in the right directory, bailing"
      exit 1
    fi
    fetch_kremlin
    run_log_commit "fstar_and_friends uregressions" "fstar-ci" "#fstar-build" "FStarLang/FStar" "."
    ;;

  fstar-nightly)
    # Same as above, except with a different label and hint regeneration.
    if [ ! -d ulib ]; then
      echo "I don't seem to be in the right directory, bailing"
      exit 1
    fi
    export OTHERFLAGS="--record_hints $OTHERFLAGS"
    fetch_kremlin
    run_log_commit "fstar_and_friends uregressions-ulong" "fstar-nightly" "#fstar-build" "FStarLang/FStar" "."
    refresh_fstar_hints
    ;;

  fstar-docs-nightly)
    # Create the docs associated with FStar
    if [ ! -d ulib ]; then
      echo "I don't seem to be in the right directory, bailing"
      exit 1
    fi

    # First - get fstar built
    make -C src/ocaml-output clean
    make -C src/ocaml-output $PARALLEL_OPT

    # Second - run fstar with the --doc flag
    run_log_commit ".ci/fsdoc.sh" "fstar-docs-nightly" "#fstar-build" "FStarLang/FStar"
    ;;

  fstar-binary-build)
    # Builds the binaries for fstar project
    if [ ! -d ulib ]; then
      echo "I don't seem to be in the right directory, bailing"
      exit 1
    fi
    fetch_kremlin
    run_log_commit "./.scripts/process_build.sh" "fstar-binarybuild" "#fstar-build" "FStarLang/FStar"
    ;;

  mitls-ci)
    if [ ! -f miTLS_icla.txt ]; then
      echo "I don't seem to be in the right directory, bailing"
      exit 1
    fi

    run_log_commit "mitls_verify" "mitls-ci" "#mitls-build" "mitls/mitls-fstar" "./fstar"
    ;;

  mitls-nightly)
    if [ ! -f miTLS_icla.txt ]; then
      echo "I don't seem to be in the right directory, bailing"
      exit 1
    fi

    export OTHERFLAGS="--record_hints $OTHERFLAGS"
    run_log_commit "mitls_verify_and_hints" "mitls-ci" "#mitls-build" "mitls/mitls-fstar" "./fstar"
    ;;


  hacl-ci)
    if [ ! -d "secure_api" ]; then
      echo "I don't seem to be in the right directory, bailing"
      exit 1
    fi

    run_log_commit "hacl_test" "hacl-ci" "#hacl-build" "mitls/hacl-star" "./fstar"
    ;;

  hacl-nightly)
    if [ ! -d "secure_api" ]; then
      echo "I don't seem to be in the right directory, bailing"
      exit 1
    fi

    export OTHERFLAGS="--record_hints $OTHERFLAGS --z3rlimit_factor 2"
    run_log_commit "hacl_test_and_hints" "hacl-ci" "#hacl-build" "mitls/hacl-star" "./fstar"
    ;;

  everest-ci)
    # Clone all projects together and make sure they test and build together
    if ! [ -x everest ]; then
      echo "Not in the right directory"
      exit 1
    fi
    run_log_commit "everest_rebuild" "everest-build" "#everest-build" "project-everest/everest"
    ;;

  everest-ci-windows)
    # Clone all projects together and make sure they test and build together
    if ! [ -x everest ]; then
      echo "Not in the right directory"
      exit 1
    fi
    run_log_commit "everest_rebuild -windows" "everest-build-windows" "#everest-build" "project-everest/everest"
    # collect sources and build with MSVC
    run_log_commit "./everest drop qbuild" "everest-qbuild-windows" "#everest-build" "project-everest/everest"
    ;;

  everest-nightly-check)
    # Start a fresh docker container that sets up everything, checks that
    # everything builds and runs on a fresh Ubuntu setup
    if ! [ -x everest ]; then
      echo "Not in the right directory"
      exit 1
    fi
    run_log_commit "docker_from_scratch" "everest-ubuntu" "#everest-docker" "project-everest/everest-ci"
    ;;

  everest-nightly-move)
    # Try to move the package to their last revision
    if ! [ -x everest ]; then
      echo "Not in the right directory"
      exit 1
    fi
    run_log_commit "everest_move" "everest-upgrade" "#everest-build" "project-everest/everest" "./FStar"
    ;;

  vale-ci)
    # Run vale ci - start in everest
    if ! [ -d tools/Vale ]; then
      echo "Not in the right directory"
      exit 1
    fi

    fetch_kremlin

    # Build F* if needed
    if [ -d .fstar_version ]; then
      fetch_fstar
    fi

    # Set up build environment
    nuget restore tools/Vale/src/packages.config -PackagesDirectory tools/FsLexYacc

    #since each build verifies x86, x64 and ARM, only verify on one build as takes quite a bit longer to verify
    if [[ "$OS" == "Windows_NT" ]]; then
      if [[ "$Platform" == "X64" ]]; then
        run_log_commit "scons.bat $PARALLEL_OPT --NOVERIFY" "vale-build" "#vale-build" "project-everest/vale"
      else
        run_log_commit "scons.bat $PARALLEL_OPT" "vale-build" "#vale-build" "project-everest/vale"
      fi
    else
      run_log_commit "scons $PARALLEL_OPT --NOVERIFY" "vale-build" "#vale-build" "project-everest/vale"
    fi
    ;;

  *)
    cat <<USAGE
USAGE: $0 [OPTIONS] ACTION

OPTIONS:
  -j n    Set the max number of parallel jobs to n (default 1)

ACTIONS:
  fstar-ci
  fstar-nightly
  fstar-docs-nightly
  fstar-binary-build
  mitls-ci
  everest-ci
  everest-nightly-check
  everest-nightly-move
  vale-ci

REMARKS:
  Read this script's source code for more explanations. It has comments.
USAGE
    ;;
esac