Skip to content

Conversation

@Kha
Copy link
Member

@Kha Kha commented Jan 16, 2026

No description provided.

@Kha
Copy link
Member Author

Kha commented Jan 16, 2026

!bench

@leanprover-radar
Copy link

leanprover-radar commented Jan 16, 2026

Benchmark results for 1a8b9c3 against 4af9cc0 are in! @Kha

Runs (2🟥)
  • 🟥 build exited with code 2
  • 🟥 other exited with code 2

@Kha Kha force-pushed the push-yvwnqyzozowp branch from 1a8b9c3 to a4030bc Compare January 16, 2026 09:51
@Kha
Copy link
Member Author

Kha commented Jan 16, 2026

!bench

@leanprover-radar
Copy link

leanprover-radar commented Jan 16, 2026

Benchmark results for a4030bc against 4af9cc0 are in! @Kha

Medium changes (1✅)
  • nat_repr//instructions: -552.6M (-12.2%)

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jan 16, 2026
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-01-16 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-01-16 10:56:07)

@leanprover-bot
Copy link
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-01-16 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-01-16 10:56:09)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants