build

#!/usr/bin/env bash

# Settings/Utilities
# ------------------

set -e
set -u

top_dir="$(pwd)"
build_dir="$top_dir/.build"
include_dir="$build_dir/include"
lib_dir="$build_dir/lib"
contrib_dir="contrib"
tests_dir="tests"

cvc4_dir="ext/cvc4"
yices2_dir="ext/yices2"
pandoc_tangle_dir="$contrib_dir/pandoc-tangle"

export PATH="/usr/lib/ccache/bin:$PATH"
export PATH="/usr/lib/ccache:$PATH"

progress() { echo "===== " $@ ; }

# Functionality
# -------------

build_clean() {
    progress "Cleaning"
    rm -rf "$build_dir"
    make -s clean || true
    git clean -dfx
    rm -rf "$cvc4_dir" "$yices2_dir"
    git submodule update --init "$cvc4_dir" "$yices2_dir"
    (   cd "$contrib_dir"
        make clean
    )
}

build_deps() {
    progress "Updating submodules"
    git submodule update --init -- "$cvc4_dir" "$yices2_dir" "$pandoc_tangle_dir"
}

build_cvc4() {
    progress "Building CVC4"
    mkdir -p $build_dir
    (   cd "$cvc4_dir"
        ./autogen.sh
        ./contrib/get-antlr-3.4
        ./configure --prefix="$build_dir" \
                    --with-antlr-dir=./antlr-3.4 \
                    ANTLR=./antlr-3.4/bin/antlr3
        make -s -j4
        make -s install
    )
}

build_yices2() {
    progress "Building Yices2"
    mkdir -p $build_dir
    (   cd "$yices2_dir"
        autoconf
        ./configure --prefix="$build_dir"
        make -s -j4
        make -s install
    )
}

build_maude() {
    progress "Building Maude $@"
    aclocal
    autoconf
    autoheader
    automake --add-missing
    automake

    ./configure CXXFLAGS="-std=c++11 -I$include_dir -L$lib_dir" "$@"
    make -s -j4 \
        || ( git checkout -- src/Mixfix/{surface.cc,tokenizer.cc}
             make -s -j4
           )

    git checkout -- src/Mixfix/{surface.cc,tokenizer.cc}
}

build_maude_cvc4() {
    build_cvc4
    build_maude --with-cvc4 CVC4_LIB="-L$lib_dir -Wl,-R$lib_dir -lcvc4"
}

build_maude_yices2() {
    build_yices2
    build_maude --with-yices2 YICES2_LIB="-L$lib_dir -Wl,-R$lib_dir -lyices"
}

build_tangle() {
    progress "Tangling"
    (   cd "$contrib_dir"
        make all
    )
}

build_test() {
    local test_file_name test_name test_dir
    test_file_name="$1" && shift

    test_name="$(basename "$test_file_name")"
    test_dir="$(dirname "$test_file_name")"

    build_tangle

    (   cd "$test_dir"
        if ! make -s check TESTS=$test_name ; then
            git --no-pager diff --no-index $test_name.{expected,out}
            return 1
        fi
    )
}

build_test_load() {
    build_tangle
    (   cd "$contrib_dir"
        make test-load "$@"
    )
}

build_test_base() {
    build_clean
    build_deps
    build_maude
    build_tangle
    make -s check "$@"
}

build_test_smt() {
    build_clean
    build_deps
    build_maude_cvc4
    build_tangle
    build_test tests/Misc/smtTest

    build_clean
    build_deps
    build_maude_yices2
    build_tangle
    build_test tests/Misc/smtTest
}

build_test_all() {
    build_test_base "$@"
    build_test_smt
}

build_test_approve() {
    local test_prefix test_out test_expected

    test_prefix="${1:-$tests_dir/}"

    for test_out in $(find "$test_prefix" -iname "*.out"); do
        test_expected="${test_out%.out}.expected"
        cp $test_out $test_expected
    done
}

# Main
# ----

build_command="$1" ; shift
case "$build_command" in
    clean)          build_clean         "$@" ;;
    deps)           build_deps          "$@" ;;
    maude)          build_maude         "$@" ;;
    maude-cvc4)     build_maude_cvc4    "$@" ;;
    maude-yices2)   build_maude_yices2  "$@" ;;
    tangle)         build_tangle        "$@" ;;
    test)           build_test          "$@" ;;
    test-all)       build_test_all      "$@" ;;
    test-base)      build_test_base     "$@" ;;
    test-smt)       build_test_smt      "$@" ;;
    test-load)      build_test_load     "$@" ;;
    test-approve)   build_test_approve  "$@" ;;
    *)      echo "
    usage: $0 [clean|deps|tangle]
           $0 maude <options>
           $0 test  <test-name>

    $0 clean:            remove build directory '$build_dir', and call 'make clean'.
    $0 deps:             clone git submodules and build CVC4.
    $0 maude <options>:  build maude passing <options> to the ./configure step.
    $0 maude-cvc4 ...:   build maude using the cvc4 git submodule
    $0 maude-yices2 ...: build maude using the yices2 git submodule
    $0 tangle:           generate '*.maude' files from '*.md' files in '$contrib_dir'.

    developers: $0 test <test-path>
                $0 test-load
                $0 test-all
                $0 test-base
                $0 test-smt
                $0 test-approve [<test-prefix>]

    $0 test:         Run test at <test-path> (eg. tests/tools/fvp/numbers).
    $0 test-load:    Test that each tangled maude file loads correctly.
    $0 test-all:     Clean build and run all tests.
    $0 test-base:    Clean build and run non-smt tests.
    $0 test-smt:     Clean build and run smt tests.
    $0 test-approve: Copy test '.out' file to '.expected' under directory <test-prefix> (default: $tests_dir).
" ;;
esac