BE-AD test script for checking solutions of tasks in Agda

agda.sh

AGDA_STDLIB=/usr/share/agda-stdlib

# build()
#
# Available:
# - submission: the text of submission (file)
# - tests: test cases (file)
# - SANDBOX_PATH: root of the directory where run() will be invoked
build() {
  name=$(cat tests | grep -m 1 -oP "(?<=module ).*(?= where)")

  cat submission > "$SANDBOX_PATH/$name.agda"
  cat tests > "$SANDBOX_PATH/original.agda"
}

# run()
#
# Available:
# - tests: test cases (file, the same as at build())
run() {
  name=$(cat tests | grep -m 1 -oP "(?<=module ).*(?= where)")

  taskRegEx="{- TASK START -}.*{- TASK END -}"

  grep -Pzo "(?s)$taskRegEx" "$name.agda" > solution.agda
  perl -0pe "s/$taskRegEx/{- TASK REMOVED -}/gs" "$name.agda" > filtered.agda
  perl -0pe "s/$taskRegEx/{- TASK REMOVED -}/gs" original.agda > benchmark.agda

  if ! diff -bwB benchmark.agda filtered.agda > difference.txt 2>&1
  then
    say "Please only edit the lines belonging to the task! ಠ_ಠ"
    say "Details:"
    say ""
    say "$(cat difference.txt)"
    return 1
  fi

  if ! agda -i ${AGDA_STDLIB} "$name.agda" > output.txt 2>&1
  then
    say "The submission has errors. (╯°□°）╯︵ ┻━┻"
    say "Details:"
    say ""
    say "$(agda --version)"
    say ""
    say "$(cat output.txt)"
    return 1
  fi

  if grep "postulate" solution.agda > /dev/null
  then
    say "Your solution contains postulate, which is not allowed. ¯\_(ツ)_/¯"
    return 1
  fi

  say "Your submission is accepted. \(ᵔᵕᵔ)/"
}