Skip to content

feat: add cslib package template - #12679

Draft
Shreyas4991 wants to merge 5 commits into
leanprover:masterfrom
Shreyas4991:cslib_template
Draft

feat: add cslib package template#12679
Shreyas4991 wants to merge 5 commits into
leanprover:masterfrom
Shreyas4991:cslib_template

Conversation

@Shreyas4991

@Shreyas4991 Shreyas4991 commented Feb 24, 2026

Copy link
Copy Markdown

Context : Zulip Thread 1 and Zulip Thread 2
RFC : #12592

TODO : This PR <short changelog summary for feat/fix, see above>.

Closes #12592

@Shreyas4991 Shreyas4991 changed the title Add cslib package template feat: add cslib package template Feb 24, 2026
@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 Feb 24, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Feb 24, 2026

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f31f50836d032d6c237272a3b2e733a92a3ee619 --onto ed0fd1e933239beaa7aaa12598f961c260062ab6. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-24 20:31:10)
  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-09-01 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-09-01 13:22:38)

@leanprover-bot

leanprover-bot commented Feb 24, 2026

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase f31f50836d032d6c237272a3b2e733a92a3ee619 --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-02-24 20:31:12)
  • ✅ Reference manual branch lean-pr-testing-12679 has successfully built against this PR. (2026-09-01 13:29:02) View Log
  • 🟡 Reference manual branch lean-pr-testing-12679 build against this PR didn't complete normally. (2026-09-01 13:30:31) View Log
  • 💥 Reference manual branch lean-pr-testing-12679 build failed against this PR. (2026-09-01 14:06:59) View Log
  • 🟡 Reference manual branch lean-pr-testing-12679 build against this PR didn't complete normally. (2026-09-01 14:09:15) View Log

@leanprover-bot leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Sep 1, 2026
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Sep 1, 2026
@leanprover-bot leanprover-bot added breaks-manual This is not necessarily a blocker for merging, but there needs to be a plan. and removed builds-manual CI has verified that the Lean Language Reference builds against this PR labels Sep 1, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

breaks-manual This is not necessarily a blocker for merging, but there needs to be a plan. toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

RFC: Add CSLib template for lake

2 participants