Skip to content

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

Draft
downstream-lean4[bot] wants to merge 1 commit into
masterfrom
adaptation-14536
Draft

[#14536] [downstream PR] Julia's instance check#16
downstream-lean4[bot] wants to merge 1 commit into
masterfrom
adaptation-14536

Conversation

@downstream-lean4

Copy link
Copy Markdown
Contributor

This is the adaptation PR for leanprover/lean4#14536.

@downstream-lean4 downstream-lean4 Bot added the adaptation This is an adaptation PR for a PR in the lean4 repository. label Jul 24, 2026
@downstream-lean4

Copy link
Copy Markdown
Contributor Author

Build report for downstream: follow upstream PR

Recently turned red:

Repo Critical Build Test Lint
batteries ✅ in 0m 🟥 in 0m ✅ in 0m
mathlib4 🟥 in 1m ⏭️ ⏭️
reference-manual ⏭️ ⏭️ ⏭️
cslib ⏭️ ⏭️ ⏭️
illuminate ✅ in 0m 🟥 in 0m ⏭️
verso 🟥 in 1m ⏭️ ⏭️
verso-web-components ⏭️ ⏭️ ⏭️
Unchanged
Repo Critical Build Test Lint
aesop ✅ in 0m ✅ in 0m ⏭️
import-graph ✅ in 0m ✅ in 0m ⏭️
lean4-cli ✅ in 0m ✅ in 0m ⏭️
plausible ✅ in 0m ✅ in 0m ⏭️
ProofWidgets4 ✅ in 0m ✅ in 0m ⏭️
quote4 ✅ in 0m ✅ in 0m ⏭️
BibtexQuery ✅ in 0m ⏭️ ⏭️
comparator ✅ in 0m ⏭️ ⏭️
doc-gen4 ✅ in 0m ⏭️ ⏭️
lean4-unicode-basic ✅ in 0m ✅ in 0m ⏭️
lean4export ✅ in 0m ✅ in 0m ⏭️
LeanSearchClient ✅ in 0m ✅ in 0m ⏭️
leansqlite ✅ in 0m ✅ in 0m ⏭️
repl ✅ in 0m ✅ in 0m ⏭️
verso-slides ⏭️ ⏭️ ⏭️

View run

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

Labels

adaptation This is an adaptation PR for a PR in the lean4 repository. toolchain-available

Projects

None yet

Development

Successfully merging this pull request may close these issues.

0 participants