Skip to content

[Merged by Bors] - chore: use authenticated gh api in nightly bump workflow#35427

Closed
kim-em wants to merge 1 commit intomasterfrom
ci/use-gh-api-for-nightly-bump
Closed

[Merged by Bors] - chore: use authenticated gh api in nightly bump workflow#35427
kim-em wants to merge 1 commit intomasterfrom
ci/use-gh-api-for-nightly-bump

Conversation

@kim-em
Copy link
Contributor

@kim-em kim-em commented Feb 17, 2026

This PR replaces unauthenticated curl calls to the GitHub API with gh api in the nightly bump workflow. The gh api command automatically uses the app token already generated in the workflow, avoiding transient failures from the unauthenticated rate limit (60 req/hour).

The first attempt of this run failed because the API returned a rate-limit error object instead of the expected array, and jq crashed trying to index it.

Corresponding PRs:

🤖 Prepared with Claude Code

Replace unauthenticated `curl` calls to GitHub API with `gh api`,
which uses the app token already generated in the workflow. This
avoids transient failures from hitting the unauthenticated rate
limit (60 requests/hour).

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@kim-em kim-em added the CI Modifies the continuous integration setup or other automation label Feb 17, 2026
@github-actions
Copy link

github-actions bot commented Feb 17, 2026

PR summary 32fe3f9354

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for scripts/declarations_diff.sh contains some details about this script.


No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@kim-em kim-em force-pushed the ci/use-gh-api-for-nightly-bump branch from 5a6a262 to b135547 Compare February 17, 2026 03:39
github-merge-queue bot pushed a commit to leanprover/cslib that referenced this pull request Feb 17, 2026
This PR replaces unauthenticated `curl` calls to the GitHub API with `gh
api` in the nightly bump workflow. The `gh api` command automatically
uses the app token already generated in the workflow, avoiding transient
failures from the unauthenticated rate limit (60 req/hour).

See [this mathlib4-nightly-testing
failure](https://github.com/leanprover-community/mathlib4-nightly-testing/actions/runs/22084056453/job/63814863096)
for an example of the problem: the API returned a rate-limit error
object instead of the expected array, and `jq` crashed trying to index
it.

Corresponding PRs:
- leanprover-community/mathlib4#35427
- leanprover-community/batteries#1678

🤖 Prepared with Claude Code

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
github-merge-queue bot pushed a commit to leanprover/cslib that referenced this pull request Feb 17, 2026
This PR replaces unauthenticated `curl` calls to the GitHub API with `gh
api` in the nightly bump workflow. The `gh api` command automatically
uses the app token already generated in the workflow, avoiding transient
failures from the unauthenticated rate limit (60 req/hour).

See [this mathlib4-nightly-testing
failure](https://github.com/leanprover-community/mathlib4-nightly-testing/actions/runs/22084056453/job/63814863096)
for an example of the problem: the API returned a rate-limit error
object instead of the expected array, and `jq` crashed trying to index
it.

Corresponding PRs:
- leanprover-community/mathlib4#35427
- leanprover-community/batteries#1678

🤖 Prepared with Claude Code

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
Copy link
Contributor

@bryangingechen bryangingechen left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!
bors r+

@mathlib-triage mathlib-triage bot added the ready-to-merge This PR has been sent to bors. label Feb 17, 2026
mathlib-bors bot pushed a commit that referenced this pull request Feb 17, 2026
This PR replaces unauthenticated `curl` calls to the GitHub API with `gh api` in the nightly bump workflow. The `gh api` command automatically uses the app token already generated in the workflow, avoiding transient failures from the unauthenticated rate limit (60 req/hour).

The [first attempt of this run](https://github.com/leanprover-community/mathlib4-nightly-testing/actions/runs/22084056453/job/63814863096) failed because the API returned a rate-limit error object instead of the expected array, and `jq` crashed trying to index it.

Corresponding PRs:
- leanprover-community/batteries#1678
- leanprover/cslib#341

🤖 Prepared with Claude Code
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Feb 17, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: use authenticated gh api in nightly bump workflow [Merged by Bors] - chore: use authenticated gh api in nightly bump workflow Feb 17, 2026
@mathlib-bors mathlib-bors bot closed this Feb 17, 2026
@mathlib-bors mathlib-bors bot deleted the ci/use-gh-api-for-nightly-bump branch February 17, 2026 14:17
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

CI Modifies the continuous integration setup or other automation ready-to-merge This PR has been sent to bors.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants

Comments