Skip to content

Commit

Permalink
Add CI mode for test script
Browse files Browse the repository at this point in the history
  • Loading branch information
marcusrossel committed Feb 28, 2024
1 parent 541c57d commit a505de1
Show file tree
Hide file tree
Showing 2 changed files with 28 additions and 19 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -30,4 +30,4 @@ jobs:
- name: Run Tests
run: |
cd Lean/Egg/Tests && ./run_tests.sh
./Lean/Egg/Tests/run_tests.sh --ci
45 changes: 27 additions & 18 deletions Lean/Egg/Tests/run_tests.sh
Original file line number Diff line number Diff line change
Expand Up @@ -3,19 +3,38 @@
tests_dir="$(realpath -s "$(dirname "$0")")"
pkg_dir="${tests_dir}/../../.."
module_prefix="Egg.Tests."
expected_fail="WIP"
skip_prefix="WIP"

cd "$pkg_dir"
ci_mode=false
for arg in "$@"
do
if [ "$arg" == "--ci" ]
then
ci_mode=true
break
fi
done

status=0
cd "$pkg_dir"
exit_code=0

for file in "$tests_dir"/*; do
if [[ -f "$file" ]]; then
if [[ "$file" == *".lean" ]]; then
file_name=$(basename "$file" ".lean")

if [[ "$file_name" == "$skip_prefix"* ]]; then
continue
fi

module_name="${module_prefix}${file_name}"

if [[ "$ci_mode" == true ]]; then
:
else
echo -n "Testing ${file_name} ..."
fi

echo -n "Testing ${file_name} ..."
lake build $module_name >/dev/null 2>&1

if [[ $? -eq 0 ]]; then
Expand All @@ -25,21 +44,11 @@ for file in "$tests_dir"/*; do
echo -e "\r✅ ${file_name} "
fi
else
expected=0
for name in $expected_fail; do
if [ "$name" = "$file_name" ]; then
expected=1
echo -e "\r❌ ${file_name} (expected)"
break
fi
done
if [[ $expected -eq 0 ]]; then
echo -e "\r❌ ${file_name} "
status=1
fi
fi
exit_code=1
echo -e "\r❌ ${file_name} "
fi
fi
fi
done

exit $status
exit $exit_code

0 comments on commit a505de1

Please sign in to comment.