Skip to content

[downstream PR] Julia's instance check - #14536

Draft
datokrat wants to merge 10 commits into
leanprover:masterfrom
datokrat:julias-instance-check
Draft

[downstream PR] Julia's instance check#14536
datokrat wants to merge 10 commits into
leanprover:masterfrom
datokrat:julias-instance-check

Conversation

@datokrat

@datokrat datokrat commented Jul 24, 2026

Copy link
Copy Markdown
Contributor

No description provided.

@datokrat datokrat added the downstream Request a downstream-lean4 adaptation PR. label Jul 24, 2026
@downstream-lean4

downstream-lean4 Bot commented Jul 24, 2026 •
edited
Loading

Copy link
Copy Markdown

The adaptation PR for this PR is leanprover/downstream-lean4#16.

@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 Jul 24, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Jul 24, 2026 •
edited
Loading

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-07-22 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-07-24 14:33:12)
  • 💥 Mathlib branch lean-pr-testing-14536 build failed against this PR. (2026-08-14 16:10:50) View Log
  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-08-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-08-18 09:53:40)

@leanprover-bot

leanprover-bot commented Jul 24, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-07-22 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-07-24 14:33:13)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-08-14 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-08-14 16:01:19)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-08-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-08-18 09:53:42)

@downstream-lean4 downstream-lean4 Bot mentioned this pull request Jul 24, 2026
Draft
@datokrat
datokrat force-pushed the julias-instance-check branch 2 times, most recently from 3801f8b to bb2ac20 Compare August 14, 2026 15:34
@datokrat

datokrat commented Aug 14, 2026

Copy link
Copy Markdown
Contributor Author

Note to self: No longer on downstream-green. Generally, I should migrate this to nightly-with-mathlib, so that I can get benchmarks.

@github-actions github-actions Bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Aug 14, 2026
@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Aug 14, 2026
@datokrat datokrat removed the downstream Request a downstream-lean4 adaptation PR. label Aug 18, 2026
@datokrat
datokrat force-pushed the julias-instance-check branch from bb2ac20 to cc7922e Compare August 18, 2026 09:22
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@hargoniX hargoniX Awaiting requested review from hargoniX hargoniX will be requested when the pull request is marked ready for review hargoniX is a code owner
@TwoFX TwoFX Awaiting requested review from TwoFX TwoFX will be requested when the pull request is marked ready for review TwoFX is a code owner
@digama0 digama0 Awaiting requested review from digama0 digama0 will be requested when the pull request is marked ready for review digama0 is a code owner

Assignees

No one assigned

Labels

breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@datokrat @leanprover-bot @TwoFX