diff options
Diffstat (limited to 'contrib/get-script-header.sh')
-rw-r--r-- | contrib/get-script-header.sh | 59 |
1 files changed, 58 insertions, 1 deletions
diff --git a/contrib/get-script-header.sh b/contrib/get-script-header.sh index 4e2a133b3..7a88b3be2 100644 --- a/contrib/get-script-header.sh +++ b/contrib/get-script-header.sh @@ -2,7 +2,15 @@ # set -e -o pipefail -cd "$(dirname "$0")/.." +[ ! -d contrib ] && echo "$0 not called from base directory" && exit 1 + +DEPS_DIR="$(pwd)/deps" +INSTALL_DIR="$DEPS_DIR/install" +INSTALL_LIB_DIR="$INSTALL_DIR/lib" +INSTALL_INCLUDE_DIR="$INSTALL_DIR/include" +INSTALL_BIN_DIR="$INSTALL_DIR/bin" + +mkdir -p "$DEPS_DIR" if ! [ -e src/parser/cvc/Cvc.g ]; then echo "$(basename $0): I expect to be in the contrib/ of a CVC4 source tree," >&2 @@ -36,3 +44,52 @@ if [ -z "$PYTHON" ]; then echo "Error: Couldn't find python, python2, or python3." >&2 exit 1 fi + +function setup_dep +{ + url="$1" + directory="$2" + echo "Setting up $directory ..." + mkdir -p "$directory" + cd "$directory" + webget "$url" archive + tar xf archive --strip 1 # Strip top-most directory + rm archive +} + +function check_dep_dir +{ + if [ -e "$1" ]; then + echo "error: file or directory '$1' exists; please move it out of the way." >&2 + exit 1 + fi +} + + +# Some of our dependencies do not provide a make install rule. Use the +# following helper functions to copy libraries/headers/binaries into the +# corresponding directories in deps/install. + +function install_lib +{ + echo "Copying $1 to $INSTALL_LIB_DIR" + [ ! -d "$INSTALL_LIB_DIR" ] && mkdir -p "$INSTALL_LIB_DIR" + cp "$1" "$INSTALL_LIB_DIR" +} + +function install_includes +{ + include="$1" + subdir="$2" + echo "Copying $1 to $INSTALL_INCLUDE_DIR/$subdir" + [ ! -d "$INSTALL_INCLUDE_DIR" ] && mkdir -p "$INSTALL_INCLUDE_DIR" + [ -n "$subdir" ] && [ ! -d "$INSTALL_INCLUDE_DIR/$subdir" ] && mkdir -p "$INSTALL_INCLUDE_DIR/$subdir" + cp -r "$include" "$INSTALL_INCLUDE_DIR/$subdir" +} + +function install_bin +{ + echo "Copying $1 to $INSTALL_BIN_DIR" + [ ! -d "$INSTALL_BIN_DIR" ] && mkdir -p "$INSTALL_BIN_DIR" + cp "$1" "$INSTALL_BIN_DIR" +} |