#!/bin/sh
#--------------------------------------------------------------------------#
# Run './configure' to produce a 'makefile' in the 'build' sub-directory or
# in any immediate sub-directory different from the 'src', 'scripts' and
# 'test' directories.
#--------------------------------------------------------------------------#
rm -f configure.log
#--------------------------------------------------------------------------#
# Common default options.
all=no
debug=no
libs=""
logging=no
check=no
competition=no
coverage=no
flexible=yes
profile=no
contracts=yes
tracing=yes
unlocked=yes
pedantic=no
options=""
quiet=no
m32=no
contrib=yes
ipasir=yes
#--------------------------------------------------------------------------#
if [ -f ./scripts/colors.sh ]
then
. ./scripts/colors.sh
elif [ -f ../scripts/colors.sh ]
then
. ../scripts/colors.sh
else
BAD=""
HILITE=""
BOLD=""
NORMAL=""
fi
die () {
if [ -f configure.log ]
then
checklog=" (check also 'configure.log')"
else
checklog=""
fi
cecho "${BOLD}configure:${NORMAL} ${BAD}error:${NORMAL} $*${checklog}"
exit 1
}
rm -f configure.log
msg () {
cecho "${BOLD}configure:${NORMAL} $*"
}
# if we can find the 'color.sh' script source it and overwrite color codes
for dir in . ..
do
[ -f $dir/scripts/colors.sh ] || continue
. $dir/scripts/colors.sh || exit 1
break
done
#--------------------------------------------------------------------------#
# Parse and handle command line options.
usage () {
cat << EOF
usage: configure [ ... ]
where ' ' is one of the following
-h|--help print this command line summary
-g|--debug compile with debugging information
-c|--check compile with assertion checking (default for '-g')
-l|--log[ging] include logging code (but disabled by default)
-a|--all short cut for all above, e.g., '-g -l' (thus also '-c')
-q|--quiet exclude message and profiling code (logging too)
-p|--pedantic add '--pedantic' and '-Werror' compilation flag
-s|--symbols add '-ggdb3' (even for optimized compilation)
--coverage compile with '-ftest-coverage -fprofile-arcs' for 'gcov'
--profile compile with '-pg' to profile with 'gprof'
--no-contracts compile without API contract checking code
--no-tracing compile without API call tracing code
--no-contrib compile without contributed code
--no-ipasir compile without ipasir interface
--competition configure for the competition
('--quiet', '--no-contracts', '--no-tracing')
-f... pass '-f [=]' options to the makefile
-W... pass '-W' options to the makefile
-m32 pass '-m32' to the compiler (compile for 32 bit)
-ggdb3 pass '-ggdb3' to makefile (like '-s')
-O|-O[123] pass '-O' or '-O[123]' to the makefile
-static... pass '-static...' option to makefile
The environment variable CXX can be used to set a different C++
compiler than the default 'g++'. Similarly you can add additional
compilation options by setting CXXFLAGS. For example
CXX=clang++ CXXFLAGS=-fPIC ./configure
will enforce to use 'clang++' as C++ compiler and also produce
position independent code. In order to be shell independent we also
allow to have the following form. Thus for instance
./configure CXX="g++-8" CXXFLAGS="-fPIC -fsanitize=address"
will have the same effect as
CXX="g++-8" ./configure -fPIC -fsanitize=address
The following configuration options might be usefull during porting the
code to a new platform and are usually not necessary to change.
--no-flexible do not use flexible array members
--no-unlocked force compilation without unlocked IO
EOF
exit 0
}
#--------------------------------------------------------------------------#
while [ $# -gt 0 ]
do
case $1 in
-h|--help) usage;;
-a|--all) all=yes;;
-g|--debug) debug=yes;;
-c|--check) check=yes;;
-l|--log|--logging) logging=yes;;
-l*) libs="$libs $1";;
-p|--pedantic) pedantic=yes;;
-q|--quiet) quiet=yes;;
--no-contracts | --no-contract) contracts=no;;
--no-tracing | --no-trace) tracing=no;;
--no-contrib) contrib=no;;
--no-ipasir) ipasir=no;;
--coverage) coverage=yes;;
--profile) profile=yes;;
--competition) competition=yes;;
--no-flexible) flexible=no;;
--no-unlocked) unlocked=no;;
-m32) options="$options $1";m32=yes;;
-f*|-W*|-ggdb3|-O|-O1|-O2|-O3) options="$options $1";;
-s|--symbols) options="$options -ggdb3";;
-static*) options="$options $1";;
CXX=*)
CXX="`expr \"$1\" : 'CXX=\(.*\)'`"
;;
CXXFLAGS=*)
CXXFLAGS="`expr \"$1\" : 'CXXFLAGS=\(.*\)'`"
;;
*) die "invalid option '$1' (try '-h')";;
esac
shift
done
#--------------------------------------------------------------------------#
if [ $quiet = yes ]
then
[ $logging = yes ] && die "can not combine '-q' with '-l'"
fi
if [ $all = yes ]
then
[ $check = yes ] && die "'-a' subsumes '-c'"
[ $debug = yes ] && die "'-a' subsumes '-g'"
[ $logging = yes ] && die "'-a' subsumes '-l'"
check=yes
debug=yes
logging=yes
elif [ $debug = yes ]
then
[ $check = yes ] && die "'-g' subsumes '-c'"
check=yes
fi
#--------------------------------------------------------------------------#
# Generate and enter 'build' directory if not already in sub-directory.
build_in_default_build_sub_directory () {
if [ -d build ]
then
msg "reusing default 'build' directory"
else
mkdir build 2>/dev/null || \
die "failed to generate 'build' directory"
msg "making default 'build' directory"
fi
cd build
msg "building in default ${HILITE}'`pwd`'${NORMAL}"
build=build
}
if [ -f configure -a -f makefile.in -a -d src ]
then
root="`pwd`"
build_in_default_build_sub_directory
elif [ -f ../configure -a -f ../makefile.in -a -d ../src ]
then
cwd="`pwd`"
build=`basename "$cwd"`
root=`dirname "$cwd"`
case x"$build" in
xsrc|xtest|xscripts)
cd ..
build_in_default_build_sub_directory
;;
*)
msg "building in ${HILITE}'$build'${NORMAL} sub-directory"
;;
esac
else
die "call 'configure' from root of CaDiCaL source or a sub-directory"
fi
msg "root directory '$root'"
#--------------------------------------------------------------------------#
src="$root/src"
if [ -d "$src" ]
then
msg "source directory '$src'"
else
die "could not find source director '$src'"
fi
#--------------------------------------------------------------------------#
# Prepare '@CXX@' and '@CXXFLAGS@' parameters for 'makefile.in'
[ x"$CXX" = x ] && CXX=g++
[ x"$CXXFLAGS" = x ] || CXXFLAGS="$CXXFLAGS "
case x"$CXX" in
x*g++*|x*clang++*) CXXFLAGS="${CXXFLAGS}-Wall -Wextra";;
*) CXXFLAGS="${CXXFLAGS}-W";;
esac
if [ $debug = yes ]
then
CXXFLAGS="$CXXFLAGS -g"
else
case x"$CXX" in
x*g++*|x*clang++*) CXXFLAGS="$CXXFLAGS -O3";;
*) CXXFLAGS="$CXXFLAGS -O";;
esac
fi
if [ $m32 = yes ]
then
case x"$CXX" in
x*g++*)
options="$options -mpc64"
msg "forcing portable 64-bit FPU mode ('-mpc64') for '$CXX'"
;;
esac
fi
if [ $competition = yes ]
then
quiet=yes
contracts=no
tracing=no
contrib=no
fi
[ $check = no ] && CXXFLAGS="$CXXFLAGS -DNDEBUG"
[ $logging = yes ] && CXXFLAGS="$CXXFLAGS -DLOGGING"
[ $quiet = yes ] && CXXFLAGS="$CXXFLAGS -DQUIET"
[ $profile = yes ] && CXXFLAGS="$CXXFLAGS -pg"
[ $coverage = yes ] && CXXFLAGS="$CXXFLAGS -ftest-coverage -fprofile-arcs"
if [ $pedantic = yes ]
then
CXXFLAGS="$CXXFLAGS --pedantic -Werror -std=c++11"
case x"$CXX" in
x*g++*|x*clang++*) CXXFLAGS="${CXXFLAGS} -Wp,-D_GLIBCXX_ASSERTIONS"
;;
esac
fi
[ $contracts = no ] && CXXFLAGS="$CXXFLAGS -DNCONTRACTS"
[ $tracing = no ] && CXXFLAGS="$CXXFLAGS -DNTRACING"
[ $contrib = no ] && CXXFLAGS="$CXXFLAGS -DNCONTRIB"
[ $ipasir = no ] && CXXFLAGS="$CXXFLAGS -DNIPASIR"
CXXFLAGS="$CXXFLAGS$options"
#--------------------------------------------------------------------------#
case x"$CXX" in
x*g++* | x*clang++*) WERROR="-Werror -pedantic";;
*) WERROR="";;
esac
# Check that compilation flags work.
feature=./configure-hello-world
cat < $feature.cpp
#include
int main () { std::cout << "hello world" << std::endl; }
EOF
if $CXX $CXXFLAGS $WERROR -o $feature.exe $feature.cpp 2>>configure.log
then
if [ ! "`$feature.exe 2>>configure.log|tr -d '\r'`" = "hello world" ]
then
die "execution of '$feature.exe' failed"
fi
else
die "test compilation '$feature.cpp'"
fi
#--------------------------------------------------------------------------#
# Since C99/C++11 is becoming the standard newer versions of 'g++' (7.3 for
# instance) discourage certain GCC extensions, particularly the GCC version
# of variadic macros, if the same concept exists in the standard. This
# forced us to replace all GCC style 'ARGS...' macros with '...' and
# '__VA_ARGS__'. Otherwise compiling the library with '--pedantic -Werror'
# would fail (configuration flag '-p'). However, older versions of 'gcc'
# (such as 4.8) would disallow these new forms of macros unless we
# explicitly enforce the new standard with '-std=c++11'. Here we try to
# figure out whether we need that flag. In earlier versions we used
# '-std=c++0x' but due to issues with older MacOS builds we switched to
# '-std=c++11' instead.
feature=./configure-requires-c++11
cat < $feature.cpp
#include
#include
// old variadic macro usage 'ARGS...' / '#ARGS' discouraged in g++-7...
// new variadic macro usage '...' / '__VA_ARGS__' available in C99/C++11
//
#define MACRO(FMT, ...) printf (FMT "\n", __VA_ARGS__)
// we use ranged for loops which became available in gcc 4.6 and for
// the gcc 4.6 as well as 4.8 requires '-std=c++11' too.
//
unsigned f (const std::vector & a) {
unsigned res = 0;
for (auto i : a) res += i;
return res;
}
int main () { MACRO ("%d", 42); return 0; }
EOF
if $CXX $CXXFLAGS $WERROR -o $feature.exe $feature.cpp 2>>configure.log
then
if [ "`$feature.exe 2>>configure.log|tr -d '\r'`" = 42 ]
then
msg "compiler supports all required C99/C++11 extensions"
else
die "checking compilation without '-std=c++11' failed"
fi
else
CXXFLAGS="$CXXFLAGS -std=c++11"
if $CXX $CXXFLAGS -o $feature.exe $feature.cpp 2>>configure.log
then
if [ "`$feature.exe 2>>configure.log|tr -d '\r'`" = 42 ]
then
msg "using '-std=c++11' for all required C99/C++11 extensions"
else
die "checking compilation with '-std=c++11' failed"
fi
else
die "compiler does not support C99/C++11 even with '-std=c++11'"
fi
fi
#--------------------------------------------------------------------------#
# Flexible array members are in C99 but not in C++11 but essential. Thus
# with pedantic compilation we have to fake them which in turn might produce
# warnings. To control those build variances with respect to warnings
# we check the support of flexible array members explicitly.
if [ $flexible = yes ]
then
feature=./configure-have-flexible-array-members
cat < $feature.cpp
#include
struct S {
int size;
int flexible_array_member[];
};
int main () {
struct S * s = (struct S*) malloc (12);
s->size = 2;
s->flexible_array_member[0] = 1;
s->flexible_array_member[1] = -1;
int res = 0;
for (int i = 0; i != s->size; i++)
res += s->flexible_array_member[i];
return res;
}
EOF
if $CXX $CXXFLAGS -o $feature.exe $feature.cpp 2>>configure.log
then
if $feature.exe
then
msg "compiler configuration supports flexible array members"
else
msg "no support for flexible array members (non zero exit code)"
flexible=no
fi
else
msg "no support for flexible array members (compilation failed)"
flexible=no
fi
else
msg "not using flexible array members (since '--no-flexible' specified)"
fi
[ $flexible = no ] && CXXFLAGS="$CXXFLAGS -DNFLEXIBLE"
#--------------------------------------------------------------------------#
# Unlocked IO is much faster but not necessarily supported.
if [ $unlocked = yes ]
then
feature=./configure-have-unlocked-io
cat < $feature.cpp
#include
int main () {
const char * path = "$feature.log";
FILE * file = fopen (path, "w");
if (!file) return 1;
if (putc_unlocked (42, file) != 42) return 1;
if (fclose (file)) return 1;
file = fopen (path, "r");
if (!file) return 1;
if (getc_unlocked (file) != 42) return 1;
if (fclose (file)) return 1;
return 0;
}
EOF
if $CXX $CXXFLAGS -o $feature.exe $feature.cpp 2>>configure.log
then
if $feature.exe
then
msg "unlocked IO with '{putc,getc}_unlocked' seems to work"
else
msg "not using unlocked IO (running '$feature.exe' failed)"
unlocked=no
fi
else
msg "not using unlocked IO (failed to compile '$feature.cpp')"
unlocked=no
fi
else
msg "not using unlocked IO (since '--no-unlocked' specified)"
fi
[ $unlocked = no ] && CXXFLAGS="$CXXFLAGS -DNUNLOCKED"
#--------------------------------------------------------------------------#
# Instantiate '../makefile.in' template to produce 'makefile' in 'build'.
msg "compiling with ${HILITE}'$CXX $CXXFLAGS'${NORMAL}"
rm -f makefile
sed \
-e "2c\\
# This 'makefile' is generated from '../makefile.in'." \
-e "s,@CXX@,$CXX," \
-e "s#@CXXFLAGS@#$CXXFLAGS#" \
-e "s#@LIBS@#$libs#" \
-e "s#@CONTRIB@#$contrib#" \
-e "s#@IPASIR@#$ipasir#" \
-e "s#@ROOT@#$root#" \
../makefile.in > makefile
msg "generated '$build/makefile' from '../makefile.in'"
#--------------------------------------------------------------------------#
build="`pwd`"
makefile="`dirname "$build"`/makefile"
cat < "$makefile"
CADICALBUILD=$build
all:
\$(MAKE) -C "\$(CADICALBUILD)"
clean:
@if [ -d "\$(CADICALBUILD)" ]; \\
then \\
if [ -f "\$(CADICALBUILD)"/makefile ]; \\
then \\
touch "\$(CADICALBUILD)"/build.hpp; \\
\$(MAKE) -C "\$(CADICALBUILD)" clean; \\
fi; \\
rm -rf "\$(CADICALBUILD)"; \\
fi
rm -f "$src/makefile"
rm -f "$makefile"
test:
\$(MAKE) -C "\$(CADICALBUILD)" test
cadical:
\$(MAKE) -C "\$(CADICALBUILD)" cadical
mobical:
\$(MAKE) -C "\$(CADICALBUILD)" mobical
update:
\$(MAKE) -C "\$(CADICALBUILD)" update
format:
\$(MAKE) -C "\$(CADICALBUILD)" format
.PHONY: all cadical clean mobical test format
EOF
msg "generated '../makefile' as proxy to ..."
msg "... '$build/makefile'"
#--------------------------------------------------------------------------#
if [ -f $src/makefile ]
then
msg "removing '$src/makefile'"
rm -f $src/makefile
fi
msg "linking '$root/makefile'"
ln -s $root/makefile $src/makefile
#--------------------------------------------------------------------------#
msg "now run ${HILITE}'make'${NORMAL} to compile CaDiCaL"
msg "optionally run 'make test'"