#!/usr/bin/env bash

set -e
set -o pipefail
set -x

# We need two FSTAR_HOMEs in this script: one for the host (from where
# we build F*) and one for the package (from where we test the
# obtained binary). FSTAR_HOST_HOME is the former.
if [[ -z "$FSTAR_HOST_HOME" ]] ; then
  FSTAR_HOST_HOME=$(cd `dirname $0`/.. && pwd)
fi
pushd "$FSTAR_HOST_HOME"

# Constants for showing color in output window
RED='\033[0;31m'
YELLOW='\033[0;33m'
GREEN='\033[0;32m'
NC='\033[0m' # No Color

diag () {
	echo -e "${YELLOW}$1${NC}"
}

diag "*** Check that the package was created  ***"
if [[ -z $OS ]] ; then
    OS=$(uname)
fi
if echo $OS | grep -i '^cygwin' ; then
    OS=Windows_NT
fi
if [[ $OS = Windows_NT ]] ; then
    ext=.zip
else
    ext=.tar.gz
fi
BUILD_PACKAGE="$FSTAR_HOST_HOME/src/ocaml-output/fstar$ext"
if ! [[ -f $BUILD_PACKAGE ]] ; then
  echo -e "src/ocaml-output/make package did not create ${BUILD_PACKAGE_FILENAME}"
  echo -e "* ${RED}FAIL!${NC}"
  exit 1
fi

diag "*** Unzip the binary package ***"
rm -rf /tmp/fstar_package
mkdir /tmp/fstar_package
popd
pushd /tmp/fstar_package
if [[ $ext = .zip ]] ; then
    unzip -o $BUILD_PACKAGE
else
    tar xf $BUILD_PACKAGE
fi
pushd fstar

diag "-- Version --"
bin/fstar.exe --version

diag "*** Test the binary package"
# We need two FSTAR_HOMEs in this script: one for the host (from where
# we build F*) and one for the package (from where we test the
# obtained binary). FSTAR_HOME is the latter.
export FSTAR_HOME="$PWD"
export FSTAR_ROOT="$PWD"/share/fstar

# We need to add the bin subdirectory to the PATH,
# to make z3 reachable
export PATH="$PWD/bin:$PATH"

# Move doc and examples to the tmp directory.
# We move them elsewhere since we
# don't want to rely on relative paths in their Makefiles.
rm -rf /tmp/fstar_examples /tmp/fstar_doc
mv share/fstar/examples /tmp/fstar_examples
mv share/fstar/doc /tmp/fstar_doc

diag "-- Verify all examples --"
if [[ -z "$CI_THREADS" ]] ; then
    CI_THREADS=1
fi

# NB: This relies on FSTAR_ROOT being set (to the share directory of the package)
# in order to find the relevant Makefiles.
make -j "$CI_THREADS" -C /tmp/fstar_examples HAS_OCAML= && make -j "$CI_THREADS" -C /tmp/fstar_doc/old/tutorial HAS_OCAMLFIND= regressions
if [ $? -ne 0 ]; then
    echo -e "* ${RED}FAIL!${NC} for all examples - make returned $?"
    exit 1
else
    echo -e "* ${GREEN}PASSED!${NC} for all examples"
fi

popd
popd
pushd $FSTAR_HOST_HOME

# Cleanup
rm -rf /tmp/fstar_examples /tmp/fstar_doc

# From this point on, we should no longer need FSTAR_HOME.
export FSTAR_HOME=
popd
