Skip to content

Commit

Permalink
Generalize process_files and use it to check Coq extraction
Browse files Browse the repository at this point in the history
  • Loading branch information
scuellar committed Jul 10, 2024
1 parent b0b7ead commit 6fce7fa
Showing 1 changed file with 11 additions and 8 deletions.
19 changes: 11 additions & 8 deletions src/example-archive/check.sh
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
#!/usr/bin/env bash
set -x

if [ -n "$1" ]
then
Expand All @@ -9,13 +8,11 @@ else
CN=cn
fi



process_files() {
local dir=$1
local pattern=$2
local action=$3
local expected_exit_code=$4
local action_argument=$4

if [ -d "$dir" ]; then
# Array to hold files matching the pattern
Expand All @@ -26,7 +23,7 @@ process_files() {
for file in "${files[@]}"; do
# Ensure the file variable is not empty
if [[ -n "$file" ]]; then
"$action" "$file" "$expected_exit_code"
"$action" "$file" "$action_argument"
fi
done
else
Expand All @@ -39,6 +36,10 @@ process_files() {

failures=0

# ====================
# Check CN verification
# ====================

check_file() {
local file=$1
local expected_exit_code=$2
Expand Down Expand Up @@ -82,7 +83,7 @@ check_coq_exports_end() {
local FAILED=$1
local MESSAGE=$2

if [[FAILED]]; then
if [[ $FAILED -ne 0 ]]; then
printf "\033[31mFAIL\033[0m (${MESSAGE})\n"
failures=$(( $failures + 1 ))
else
Expand Down Expand Up @@ -158,8 +159,10 @@ check_coq_exports() {
}

printf "=========\nChecking Coq builds\n\n"
check_coq_exports "coq/working/trivial-001.c" ${SUCCESS}
check_coq_exports "coq/broken-export/recursive-001.c" ${FAIL_EXPORT}

process_files "coq/working" "*.c" check_coq_exports $SUCCESS
process_files "coq/broken-build" "*.c" check_coq_exports $FAIL_COQ_BUILD
process_files "coq/broken-export" "*.c" check_coq_exports $FAIL_EXPORT


if [[ "$failures" = 0 ]]
Expand Down

0 comments on commit 6fce7fa

Please sign in to comment.