Skip to content

feat: precompiled tactic elaboration configurations (draft, for mathlib testing)#13650

Draft
kmill wants to merge 4 commits into
masterfrom
kmill_tactic_config_compile2
Draft

feat: precompiled tactic elaboration configurations (draft, for mathlib testing)#13650
kmill wants to merge 4 commits into
masterfrom
kmill_tactic_config_compile2

Conversation

@kmill
Copy link
Copy Markdown
Collaborator

@kmill kmill commented May 5, 2026 •
edited
Loading

This PR is a draft, to test out changes on nightly-with-mathlib that require a stage0 update. Corresponds to #13651.

@kmill kmill added the changelog-language Language features and metaprograms label May 5, 2026
@github-actions github-actions Bot added changes-stage0 Contains stage0 changes, merge manually using rebase toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN labels May 5, 2026
@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented May 5, 2026

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-05-04 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-05-05 19:35:57)

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

Reviewers

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

@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

@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

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

@kim-em kim-em Awaiting requested review from kim-em kim-em will be requested when the pull request is marked ready for review kim-em is a code owner

Assignees

No one assigned

Labels

changelog-language Language features and metaprograms changes-stage0 Contains stage0 changes, merge manually using rebase 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.

2 participants

@kmill @leanprover-bot