Skip to content

[#15027] perf: move ref into the Core.Context cold subobject - #46

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

[#15027] perf: move ref into the Core.Context cold subobject#46
downstream-lean4[bot] wants to merge 1 commit into
masterfrom
adaptation-15027

Conversation

@downstream-lean4

Copy link
Copy Markdown
Contributor

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

@downstream-lean4 downstream-lean4 Bot added adaptation This is an adaptation PR for a PR in the lean4 repository. toolchain-available labels Sep 4, 2026
@downstream-lean4

Copy link
Copy Markdown
Contributor Author

Build report for downstream: follow upstream PR

Stayed green
Repo Critical Build Test Lint
aesop ✅ in 17s ✅ in 4s ⏭️
batteries ✅ in 12s ✅ in 4s ✅ in 2s
import-graph ✅ in 3s ✅ in 4s ⏭️
lean4-cli ✅ in 3s ✅ in 0s ⏭️
mathlib4 ✅ in 1046s ✅ in 42s ✅ in 93s
plausible ✅ in 3s ✅ in 2s ⏭️
ProofWidgets4 ✅ in 5s ✅ in 1s ⏭️
quote4 ✅ in 6s ✅ in 1s ⏭️
reference-manual ✅ in 74s ⏭️ ⏭️
BibtexQuery ✅ in 3s ⏭️ ⏭️
comparator ✅ in 3s ⏭️ ⏭️
cslib ✅ in 34s ✅ in 8s ✅ in 3s
doc-gen4 ✅ in 16s ⏭️ ⏭️
illuminate ✅ in 8s ✅ in 11s ⏭️
lean4-unicode-basic ✅ in 4s ⏭️ ⏭️
lean4export ✅ in 3s ✅ in 8s ⏭️
LeanSearchClient ✅ in 2s ✅ in 0s ⏭️
leansqlite ✅ in 9s ✅ in 20s ⏭️
repl ✅ in 4s ✅ in 59s ⏭️
verso ✅ in 127s ✅ in 87s ⏭️
verso-slides ✅ in 19s ✅ in 6s ⏭️
verso-web-components ✅ in 36s ⏭️ ⏭️

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. cache-available toolchain-available

Projects

None yet

Development

Successfully merging this pull request may close these issues.

0 participants