Tag me on failures

Fixes #8
coq-community · Feb 10, 2022 · c309417 · c309417 · Zimmi48 · Feb 10, 2022
1 parent cf62925
commit c309417
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 2 deletions.
diff --git 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
@@ -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" <<EOF