diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-12-06 06:48:04 -0800 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-06 08:48:04 -0600 |
commit | 008d6b51baec353f45324e1d9407d898866cf688 (patch) | |
tree | 136e5c1dcbfb32f1fed99b853b79c2f7ecc6b5d2 /contrib/get-script-header.sh | |
parent | 46bae5d2a8b22867f917c6f644e46e29884049f9 (diff) |
contrib: Setup all dependencies in deps/ directory. (#3534)
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" +} |