max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test(tests/playground/run.sh): split out compile.sh

Browse source
This commit is contained in:
Sebastian Ullrich 2019-02-26 19:23:04 +01:00
parent 6f73f19d19
commit c4bc783ef4
2 changed files with 41 additions and 36 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

40
tests/playground/compile.sh Normal file
View file

@ -0,0 +1,40 @@
#!/usr/bin/env bash
if [ $# -eq 0 ]; then
echo "Usage: compile.sh [file]"
exit 1
fi
ulimit -s 8192
source ../compiler/test_flags.sh
BIN_DIR=../../bin
LEAN=$BIN_DIR/lean
INCLUDE_DIR=../../src
export LEAN_PATH=../../library:.
ff=$1
# Hack for converting a list of libraries such as `/usr/lib/gmp.so;dl` into valid liker parameters.
LINKER_LIBS=""
for lib in ${LIBS//;/ }; do
if [[ $lib == *".so" || $lib == *".dll" || $lib == *".dylib" ]]; then
LINKER_LIBS="$LINKER_LIBS $lib"
else
LINKER_LIBS="$LINKER_LIBS -l$lib"
fi
done
if [[ "$OSTYPE" == "msys" ]]; then
# Windows running MSYS2
# Replace /c/ with c:, and / with \\
ff=$(echo $ff | sed 's|^/\([a-z]\)/|\1:/|' | sed 's|/|\\\\|g')
fi
$LEAN --cpp="$ff".cpp "$ff"
if [ $? -ne 0 ]; then
echo "Failed to compile $ff into C++ file"
exit 1
fi
$CXX -o "$ff.out" -I $INCLUDE_DIR $CXX_FLAGS $ff.cpp $BIN_DIR/libleanstatic.a $LINKER_FLAGS $LINKER_LIBS
if [ $? -ne 0 ]; then
echo "Failed to compile C++ file $ff.cpp"
exit 1
fi

37
tests/playground/run.sh
View file

@ -3,41 +3,6 @@ if [ $# -eq 0 ]; then
echo "Usage: run.sh [file] [args]*"
exit 1
fi
ulimit -s 8192
source ../compiler/test_flags.sh
BIN_DIR=../../bin
LEAN=$BIN_DIR/lean
INCLUDE_DIR=../../src
export LEAN_PATH=../../library:.
ff=$1
# Hack for converting a list of libraries such as `/usr/lib/gmp.so;dl` into valid liker parameters.
LINKER_LIBS=""
for lib in ${LIBS//;/ }; do
if [[ $lib == *".so" || $lib == *".dll" || $lib == *".dylib" ]]; then
LINKER_LIBS="$LINKER_LIBS $lib"
else
LINKER_LIBS="$LINKER_LIBS -l$lib"
fi
done
if [[ "$OSTYPE" == "msys" ]]; then
# Windows running MSYS2
# Replace /c/ with c:, and / with \\
ff=$(echo $ff | sed 's|^/\([a-z]\)/|\1:/|' | sed 's|/|\\\\|g')
fi
$LEAN --cpp="$ff".cpp "$ff"
if [ $? -ne 0 ]; then
echo "Failed to compile $ff into C++ file"
exit 1
fi
$CXX -o "$ff.out" -I $INCLUDE_DIR $CXX_FLAGS $ff.cpp $BIN_DIR/libleanstatic.a $LINKER_FLAGS $LINKER_LIBS
if [ $? -ne 0 ]; then
echo "Failed to compile C++ file $ff.cpp"
exit 1
fi
./compile.sh $1
shift 1
"./$ff.out" $*