Skip to content

[Merged by Bors] - fix(CI): run leanchecker in mathlib4 repo for both master and nightly#34480

Closed
kim-em wants to merge 1 commit intomasterfrom
fix-daily-leanchecker
Closed

[Merged by Bors] - fix(CI): run leanchecker in mathlib4 repo for both master and nightly#34480
kim-em wants to merge 1 commit intomasterfrom
fix-daily-leanchecker

Conversation

@kim-em
Copy link
Contributor

@kim-em kim-em commented Jan 27, 2026

This PR fixes the daily CI workflow for leanchecker.

The check-leanchecker job was configured to run only in mathlib4-nightly-testing, but the notify-leanchecker job runs in mathlib4 and tries to query the job status from the current workflow run. Since the job was skipped in mathlib4, the notification produced broken Zulip messages with empty URLs (see https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/leanchecker.20failure/near/570212817).

This PR:

  • Moves check-leanchecker to run in mathlib4 (matching check-nanoda and check-mathlib_test_executable)
  • Enables both master and nightly branches for leanchecker (the TODO comment indicated this was waiting for leanchecker to land on master)

🤖 Prepared with Claude Code

The leanchecker job was configured to run in mathlib4-nightly-testing
but the notification job runs in mathlib4, causing the notification to
fail to find the job and produce broken Zulip messages with empty URLs.

This PR:
- Moves check-leanchecker to run in mathlib4 (like the other check jobs)
- Enables both master and nightly branches for leanchecker

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <noreply@anthropic.com>
@github-actions
Copy link

PR summary 0e16bffea0

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 script/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).

@github-actions github-actions bot added the CI Modifies the continuous integration setup or other automation label Jan 27, 2026
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+

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Jan 27, 2026
mathlib-bors bot pushed a commit that referenced this pull request Jan 27, 2026
…#34480)

This PR fixes the daily CI workflow for leanchecker.

The `check-leanchecker` job was configured to run only in `mathlib4-nightly-testing`, but the `notify-leanchecker` job runs in `mathlib4` and tries to query the job status from the current workflow run. Since the job was skipped in `mathlib4`, the notification produced broken Zulip messages with empty URLs (see https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/leanchecker.20failure/near/570212817).

This PR:
- Moves `check-leanchecker` to run in `mathlib4` (matching `check-nanoda` and `check-mathlib_test_executable`)
- Enables both `master` and `nightly` branches for leanchecker (the TODO comment indicated this was waiting for leanchecker to land on master)

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

mathlib-bors bot commented Jan 27, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title fix(CI): run leanchecker in mathlib4 repo for both master and nightly [Merged by Bors] - fix(CI): run leanchecker in mathlib4 repo for both master and nightly Jan 27, 2026
@mathlib-bors mathlib-bors bot closed this Jan 27, 2026
@mathlib-bors mathlib-bors bot deleted the fix-daily-leanchecker branch January 27, 2026 10:08
YellPika pushed a commit to YellPika/mathlib4 that referenced this pull request Feb 3, 2026
…leanprover-community#34480)

This PR fixes the daily CI workflow for leanchecker.

The `check-leanchecker` job was configured to run only in `mathlib4-nightly-testing`, but the `notify-leanchecker` job runs in `mathlib4` and tries to query the job status from the current workflow run. Since the job was skipped in `mathlib4`, the notification produced broken Zulip messages with empty URLs (see https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/leanchecker.20failure/near/570212817).

This PR:
- Moves `check-leanchecker` to run in `mathlib4` (matching `check-nanoda` and `check-mathlib_test_executable`)
- Enables both `master` and `nightly` branches for leanchecker (the TODO comment indicated this was waiting for leanchecker to land on master)

🤖 Prepared with Claude Code
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