diff --git a/tests/playground/newcompile.sh b/tests/playground/newcompile.sh new file mode 100755 index 0000000000..b7ee89a4a8 --- /dev/null +++ b/tests/playground/newcompile.sh @@ -0,0 +1,28 @@ +#!/usr/bin/env bash +if [ $# -eq 0 ]; then + echo "Usage: compile.sh [file]" + exit 1 +fi +ulimit -s 8192 +BIN_DIR=../../bin +LEAN=$BIN_DIR/lean +export LEAN_PATH=../../library:. +ff=$1 + +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 --newcpp="$ff".cpp "$ff" +if [ $? -ne 0 ]; then + echo "Failed to compile $ff into C++ file" + exit 1 +fi + +$BIN_DIR/leanc -O3 -o "$ff.out" $ff.cpp +if [ $? -ne 0 ]; then + echo "Failed to compile C++ file $ff.cpp" + exit 1 +fi diff --git a/tests/playground/newrun.sh b/tests/playground/newrun.sh new file mode 100755 index 0000000000..0e0fd65cb1 --- /dev/null +++ b/tests/playground/newrun.sh @@ -0,0 +1,9 @@ +#!/usr/bin/env bash +if [ $# -eq 0 ]; then + echo "Usage: run.sh [file] [args]*" + exit 1 +fi +ff=$1 +./newcompile.sh $ff +shift 1 +time "./$ff.out" $*