COUNTEREXAMPLES_OUTCOME: unbound variable

Stream: nightly-testing

[Joachim Breitner]

Did the pr-testing-comment script break? Is anyone already having a look?

Run scripts/lean-pr-testing-comments.sh lean
This is a 'lean-pr-testing-5991' branch, so we need to adjust labels and write a comment.
Removing label awaiting-mathlib
{
  "message": "Label does not exist",
  "documentation_url": "https://docs.github.com/rest/issues/labels#remove-a-label-from-an-issue",
  "status": "404"
}
Removing label breaks-mathlib
{
  "message": "Label does not exist",
  "documentation_url": "https://docs.github.com/rest/issues/labels#remove-a-label-from-an-issue",
  "status": "404"
}
Adding label builds-mathlib
[
  {
    "id": 5906552834,
    "node_id": "LA_kwDOB7kabM8AAAABYA7YAg",
    "url": "https://api.github.com/repos/leanprover/lean4/labels/builds-mathlib",
    "name": "builds-mathlib",
    "color": "81C3A1",
    "default": false,
    "description": "CI has verified that Mathlib builds against this PR"
  },
  {
    "id": 5906657964,
    "node_id": "LA_kwDOB7kabM8AAAABYBByrA",
    "url": "https://api.github.com/repos/leanprover/lean4/labels/toolchain-available",
    "name": "toolchain-available",
    "color": "366329",
    "default": false,
    "description": "A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN"
  }
]
scripts/lean-pr-testing-comments.sh: line 105: COUNTEREXAMPLES_OUTCOME: unbound variable

https://github.com/leanprover-community/mathlib4/actions/runs/11722398054/job/32651847816

[Bryan Gin-ge Chen]

Fallout from #15996 perhaps? @Michael Rothgang

[Michael Rothgang]

Sounds like it could be! This is a script erroring because it doesn't know any variable COUNTEREXAMPLES_OUTCOME. I see a short and a long-term fix.

Short-term fix: use a default value for the variable, as described here, i.e. write ${COUNTEREXAMPLES_OUTCOME:-} instead. This could work here... but reading the doc-string before, it looks like that's not a good fix.

Better fix: find out why that variable was not set when this script was called. By line 27 on that file, it should be set --- this this is merely exposing a pre-existing error.

(Worst fix: remove the set -u from that file. That's at best a band-aid, in my opinion.)

[Damiano Testa]

There was a recent similar issue: is it the difference between counterexample and counterexamples?

[Damiano Testa]

Maybe #18617?

[Damiano Testa]

And this discussion seems to report the same error.

[Bryan Gin-ge Chen]

If no one beats me to it I'll make a PR in a few hours.

[Bryan Gin-ge Chen]

Ah, actually, I just noticed that this testing branch doesn't contain #18617, so if you merge master into it, it might fix it?