Skip to content

feat: bundle leantar with Lean#12822

Merged
tydeu merged 6 commits intoleanprover:masterfrom
tydeu:add-leantar
Mar 9, 2026
Merged

feat: bundle leantar with Lean#12822
tydeu merged 6 commits intoleanprover:masterfrom
tydeu:add-leantar

Conversation

@tydeu
Copy link
Copy Markdown
Member

@tydeu tydeu commented Mar 6, 2026

This PR downloads a prebuilt release of leantar and bundles it with Lean as part of the core build.

@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 Mar 6, 2026
@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Mar 6, 2026 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-05 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-03-06 02:53:53)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-09 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-03-09 17:56:47)

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Mar 6, 2026
Update lean-toolchain for testing leanprover/lean4#12822
b880b94
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 6, 2026
Update lean-toolchain for testing leanprover/lean4#12822
6864d52
@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 Mar 6, 2026
@tydeu tydeu added the release-ci Enable all CI checks for a PR, like is done for releases label Mar 6, 2026
@mathlib-lean-pr-testing mathlib-lean-pr-testing bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Mar 6, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Mar 6, 2026 •
edited
Loading

Mathlib CI status (docs):

  • ✅ Mathlib branch lean-pr-testing-12822 has successfully built against this PR. (2026-03-06 03:50:28) View Log
  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-03-09 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-03-09 17:56:44)

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Mar 6, 2026
Update lean-toolchain for leanprover/lean4#12822
7ce7f9d
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 6, 2026
Update lean-toolchain for leanprover/lean4#12822
e1afbff
@tydeu tydeu requested a review from Kha March 6, 2026 05:01
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Mar 6, 2026

Mathlib CI status (docs):

@tydeu tydeu requested review from Garmelon and digama0 March 6, 2026 17:15
Garmelon
Garmelon reviewed Mar 6, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@Garmelon Garmelon left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

On systems like NixOS, downloading random binaries from the internet won't result in runnable binaries. Will leantar be part of the build process itself in the future?

Comment thread CMakeLists.txt
mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Mar 6, 2026
Update lean-toolchain for leanprover/lean4#12822
608726e
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 6, 2026
Update lean-toolchain for leanprover/lean4#12822
7563a2f
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Mar 6, 2026

Mathlib CI status (docs):

@tydeu tydeu added this pull request to the merge queue Mar 9, 2026
Merged via the queue into leanprover:master with commit 007e082 Mar 9, 2026
23 checks passed
@tydeu tydeu deleted the add-leantar branch March 10, 2026 16:29
@mattrobball mattrobball mentioned this pull request Apr 7, 2026
Open
3 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@digama0 digama0 digama0 approved these changes

@Garmelon Garmelon Garmelon approved these changes

@Kha Kha Awaiting requested review from Kha

Assignees

No one assigned

Labels

builds-mathlib CI has verified that Mathlib builds against this PR changelog-other mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN release-ci Enable all CI checks for a PR, like is done for releases 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.

4 participants

@tydeu @leanprover-bot @digama0 @Garmelon