From a9c5063145f3870393dc2dd75d0722ead1c5efd7 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Tue, 6 Feb 2018 19:46:04 -0800 Subject: [PATCH] Use separate shell script for common get-* script parts. (#1567) --- contrib/get-abc | 29 +++-------------------------- contrib/get-antlr-3.4 | 25 +------------------------ contrib/get-cryptominisat4 | 29 +++-------------------------- contrib/get-glpk-cut-log | 25 +------------------------ contrib/get-lfsc-checker | 15 +-------------- contrib/get-script-header.sh | 26 ++++++++++++++++++++++++++ 6 files changed, 35 insertions(+), 114 deletions(-) create mode 100644 contrib/get-script-header.sh diff --git a/contrib/get-abc b/contrib/get-abc index 7cf833e23..0a840fc84 100755 --- a/contrib/get-abc +++ b/contrib/get-abc @@ -1,37 +1,14 @@ #!/bin/bash # -set -e - -commit=53f39c11b58d - -cd "$(dirname "$0")/.." - -if ! [ -e src/parser/cvc/Cvc.g ]; then - echo "$(basename $0): I expect to be in the contrib/ of a CVC4 source tree," >&2 - echo "but apparently:" >&2 - echo >&2 - echo " $(pwd)" >&2 - echo >&2 - echo "is not a CVC4 source tree ?!" >&2 - exit 1 -fi - -function webget { - if which wget &>/dev/null; then - wget -c -O "$2" "$1" - elif which curl &>/dev/null; then - curl "$1" >"$2" - else - echo "Can't figure out how to download from web. Please install wget or curl." >&2 - exit 1 - fi -} +source "$(dirname "$0")/get-script-header.sh" if [ -e abc ]; then echo 'error: file or directory "abc" exists; please move it out of the way.' >&2 exit 1 fi +commit=53f39c11b58d + mkdir abc cd abc webget https://bitbucket.org/alanmi/abc/get/$commit.tar.gz abc-$commit.tar.gz diff --git a/contrib/get-antlr-3.4 b/contrib/get-antlr-3.4 index 87d6ea450..4ee23509a 100755 --- a/contrib/get-antlr-3.4 +++ b/contrib/get-antlr-3.4 @@ -1,34 +1,11 @@ #!/bin/bash # -set -e - -cd "$(dirname "$0")/.." +source "$(dirname "$0")/get-script-header.sh" if [ -z "${BUILD_TYPE}" ]; then BUILD_TYPE="--disable-shared --enable-static" fi -if ! [ -e src/parser/cvc/Cvc.g ]; then - echo "$(basename $0): I expect to be in the contrib/ of a CVC4 source tree," >&2 - echo "but apparently:" >&2 - echo >&2 - echo " $(pwd)" >&2 - echo >&2 - echo "is not a CVC4 source tree ?!" >&2 - exit 1 -fi - -function webget { - if which curl &>/dev/null; then - curl "$1" >"$2" - elif which wget &>/dev/null; then - wget -c -O "$2" "$1" - else - echo "Can't figure out how to download from web. Please install wget or curl." >&2 - exit 1 - fi -} - if [ -z "${MACHINE_TYPE}" ]; then if ! [ -e config/config.guess ]; then # Attempt to download once diff --git a/contrib/get-cryptominisat4 b/contrib/get-cryptominisat4 index c96bbe03d..c6f2a1ce8 100755 --- a/contrib/get-cryptominisat4 +++ b/contrib/get-cryptominisat4 @@ -1,37 +1,14 @@ #!/bin/bash # -set -e - -version="4.2.0" - -cd "$(dirname "$0")/.." - -if ! [ -e src/parser/cvc/Cvc.g ]; then - echo "$(basename $0): I expect to be in the contrib/ of a CVC4 source tree," >&2 - echo "but apparently:" >&2 - echo >&2 - echo " $(pwd)" >&2 - echo >&2 - echo "is not a CVC4 source tree ?!" >&2 - exit 1 -fi - -function webget { - if which wget &>/dev/null; then - wget -c -O "$2" "$1" - elif which curl &>/dev/null; then - curl "$1" >"$2" - else - echo "Can't figure out how to download from web. Please install wget or curl." >&2 - exit 1 - fi -} +source "$(dirname "$0")/get-script-header.sh" if [ -e cryptominisat4 ]; then echo 'error: file or directory "cryptominisat4" exists; please move it out of the way.' >&2 exit 1 fi +version="4.2.0" + mkdir cryptominisat4 cd cryptominisat4 CRYPTOMINISAT_PATH=`pwd` diff --git a/contrib/get-glpk-cut-log b/contrib/get-glpk-cut-log index 5ca18c66d..419fdba90 100755 --- a/contrib/get-glpk-cut-log +++ b/contrib/get-glpk-cut-log @@ -1,32 +1,9 @@ #!/bin/bash # -set -e +source "$(dirname "$0")/get-script-header.sh" commit=b420454e732f4b3d229c552ef7cd46fec75fe65c -cd "$(dirname "$0")/.." - -if ! [ -e src/parser/cvc/Cvc.g ]; then - echo "$(basename $0): I expect to be in the contrib/ of a CVC4 source tree," >&2 - echo "but apparently:" >&2 - echo >&2 - echo " $(pwd)" >&2 - echo >&2 - echo "is not a CVC4 source tree ?!" >&2 - exit 1 -fi - -function webget { - if which wget &>/dev/null; then - wget -c -O "$2" "$1" - elif which curl &>/dev/null; then - curl "$1" >"$2" - else - echo "Can't figure out how to download from web. Please install wget or curl." >&2 - exit 1 - fi -} - if [ -e glpk-cut-log ]; then echo 'error: file or directory "glpk-cut-log" exists; please move it out of the way.' >&2 exit 1 diff --git a/contrib/get-lfsc-checker b/contrib/get-lfsc-checker index 495082387..f4c79de2a 100755 --- a/contrib/get-lfsc-checker +++ b/contrib/get-lfsc-checker @@ -1,23 +1,10 @@ #!/bin/bash # -set -e +source "$(dirname "$0")/get-script-header.sh" lfscrepo="https://github.com/CVC4/LFSC.git" dirname="lfsc-checker" - -cd "$(dirname "$0")/.." - -if ! [ -e src/parser/cvc/Cvc.g ]; then - echo "$(basename $0): I expect to be in the contrib/ of a CVC4 source tree," >&2 - echo "but apparently:" >&2 - echo >&2 - echo " $(pwd)" >&2 - echo >&2 - echo "is not a CVC4 source tree ?!" >&2 - exit 1 -fi - function gitclone { if which git &> /dev/null then diff --git a/contrib/get-script-header.sh b/contrib/get-script-header.sh new file mode 100644 index 000000000..285d97b35 --- /dev/null +++ b/contrib/get-script-header.sh @@ -0,0 +1,26 @@ +#!/bin/bash +# +set -e + +cd "$(dirname "$0")/.." + +if ! [ -e src/parser/cvc/Cvc.g ]; then + echo "$(basename $0): I expect to be in the contrib/ of a CVC4 source tree," >&2 + echo "but apparently:" >&2 + echo >&2 + echo " $(pwd)" >&2 + echo >&2 + echo "is not a CVC4 source tree ?!" >&2 + exit 1 +fi + +function webget { + if which wget &>/dev/null; then + wget -c -O "$2" "$1" + elif which curl &>/dev/null; then + curl "$1" >"$2" + else + echo "Can't figure out how to download from web. Please install wget or curl." >&2 + exit 1 + fi +} -- 2.30.2