diff --git a/reply-coqbot-error.sh b/reply-coqbot-error.sh index d12c937..01466b0 100644 --- a/reply-coqbot-error.sh +++ b/reply-coqbot-error.sh @@ -8,7 +8,7 @@ DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" set -x id="$1" -comment_contents="Error: Could not minimize file $2 (full log [on GitHub Actions](${GITHUB_WORKFLOW_URL}))" +comment_contents="Error: Could not minimize file $2 (full log [on GitHub Actions](${GITHUB_WORKFLOW_URL}), cc @JasonGross)" comment_contents+="$(print_file tail "$(( 2 * ${GITHUB_MAX_CHAR_COUNT} / 5 ))" "build log" "" "${start_code}" "$3" "${end_code}")" comment_contents+="$(print_file tail "$(( 2 * ${GITHUB_MAX_CHAR_COUNT} / 5 ))" "minimizer log" "" "${start_code}" "$4" "${end_code}")" comment_contents+="${nl}${nl}$(cat "$DIR/feedback.md")" diff --git a/reply-coqbot.sh b/reply-coqbot.sh index ecd65db..bdce7b2 100644 --- a/reply-coqbot.sh +++ b/reply-coqbot.sh @@ -11,11 +11,20 @@ comment_contents="Minimized File $2 (full log [on GitHub Actions](${GITHUB_WORKF if [ ! -z "${SURVEY_URL}" ] && [ ! -z "${SURVEY_PR_URL_PARAMETER}" ] && [ ! -z "${ISSUE_NUMBER}" ] && [ ! -z "$DIR/early-feedback.md" ] && [ ! -f "${TIMEDOUT_STAMP_FILE}" ]; then comment_contents+="${nl}${nl}$(cat "$DIR/early-feedback.md" | sed "s>@SURVEY_URL@>${SURVEY_URL}?${SURVEY_PR_URL_PARAMETER}=${ISSUE_NUMBER}>g")" fi -comment_contents+="$(print_file head "$(( ${GITHUB_MAX_CHAR_COUNT} / 2 ))" "Minimized Coq File" " (consider adding this file to the test-suite)" "${start_coq_code}" "$3" "${end_code}")" +uninlinable_modules="$(grep '^\s*Modules that could not be inlined:' "$3" | sed 's/^\s*Modules that could not be inlined:\s*/g')" +if [ ! -z "${uninlinable_modules}" ]; then + min_descr="Partially Minimized Coq File (could not inline ${uninlinable_modules})" +else + min_descr="Minimized Coq File" +fi +comment_contents+="$(print_file head "$(( ${GITHUB_MAX_CHAR_COUNT} / 2 ))" "${min_descr}" " (consider adding this file to the test-suite)" "${start_coq_code}" "$3" "${end_code}")" comment_contents+="$(print_file head "$(( ${GITHUB_MAX_CHAR_COUNT} / 8 ))" "Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)" "" "${start_coq_code}" "$4" "${end_code}")" comment_contents+="$(print_file tail "$(( ${GITHUB_MAX_CHAR_COUNT} / 8 ))" "Build Log (contains the Coq error message)" "" "${start_code}" "$5" "${end_code}")" comment_contents+="$(print_file tail "$(( ${GITHUB_MAX_CHAR_COUNT} / 8 ))" "Minimization Log" "" "${start_code}" "$6" "${end_code}")" comment_contents+="${nl}${nl}$(cat "$DIR/feedback.md")" +if [ ! -z "${uninlinable_modules}" ]; then + comment_contents+="${nl}${nl}cc @JasonGross" +fi file="$(mktemp)" cat > "$file" <