Skip to content

Bump con-leche and con-ron - #260

Merged
nomeata merged 1 commit into
masterfrom
joachim/bump-con-leche-67f0463
Oct 6, 2026
Merged

nomeata merged 1 commit into
masterfrom
joachim/bump-con-leche-67f0463

Conversation

@nomeata

@nomeata nomeata commented Oct 6, 2026 •

Copy link
Copy Markdown
Collaborator

Bumps con-leche to 67f0463 and con-ron to 328307e (con-ron's pin of con-leche is 67f0463, so the two stay in sync).

  • Both checkers move from Lean v4.33.0 to v4.35.0-rc3 (sources, built-in prelude and pin dump; the nightly pin set matches v4.35.0-rc3's Init).
  • con-leche: the consistency proof now covers nested inductives (proof side only), plus the whitepaper.
  • con-ron: tracks con-leche; removes the whnf_core memo cache cap (it limited magma-list-deep-n36) and moves its proofs to vcgen and Std.WP.

🤖 Generated with Claude Code

con-leche 67f0463 and con-ron 328307e: both on Lean v4.35.0-rc3; con-leche
extends the consistency proof to nested inductives, con-ron drops its cache
cap.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@nomeata
nomeata enabled auto-merge (squash) October 6, 2026 19:45
@nomeata
nomeata merged commit b83254d into master Oct 6, 2026
7 checks passed
@nomeata
nomeata deleted the joachim/bump-con-leche-67f0463 branch October 6, 2026 20:02
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant