Repository navigation
fix: port to Lean v4.33.1 (toolchain, manifest, tactic adaptations) - #3
Merged
Merged
Conversation
- lean-toolchain + lake-manifest.json: v4.31.0 -> v4.33.1, same pins as consumer formal_logic_lean (mathlib 0df444a3, Foundation 81810b9f, batteries 4488d40d) - AdjunctiveSet: explicit Subset field value (v4.33 rejects the self-referential synthesized instance) - Logic/Semantics:219: explicit application in the reverse iff direction - Modal/LogicSymbol:347,430: dsimp -> simp (dsimp no longer fires closing simp lemmas) - Neighborhood/Semantics/Completeness:264: term-mode .trans proof (rw/unfold fragile on abbrev+lambda under implicit transparency) - Neighborhood/Semantics/Filtration: open Finset membership by lemma application (Finset.mem_filter) instead of rcases whnf - Neighborhood/Semantics/AxiomN: direct ContainsUnit instance on the abbrev head (v4.33 instance search no longer unfolds intermediateRelativeMaximalCanonicalModel to match the general relativeBasicCanonicalModel instance) lake build: SUCCESS (1230 jobs) under v4.33.1 lake build ModalLogicArchive.Modal.Kripke.Logic.S5: SUCCESS (1081 jobs) Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Grain: DEEP/lean — lane myia-po-2024:CoursIA-2 — prev: MED/guard #18970
Port to Lean v4.33.1 (toolchain, manifest, tactic adaptations)
Moves the fork to the same toolchain as its consumer
formal_logic_lean(CoursIA #17522, option 1, coordinator arbitration 2026-10-04 10:08Z), so the CI of this fork proves the build under the toolchain the consumer actually pins.lean-toolchain:v4.31.0->v4.33.1lake-manifest.json: same pins as the consumer (mathlib0df444a3, Foundation81810b9f, batteries4488d40d)Lean v4.33 breaking changes addressed (all measured on this port)
Vorspiel/AdjunctiveSet.leanSubsetfield value — v4.33 rejects the self-referential synthesized instance (inferInstanceloops back into the instance being defined)Logic/Semantics.lean:219iffdirectionModal/LogicSymbol.lean:347,430dsimp->simp—dsimpno longer fires closing simp lemmasNeighborhood/Semantics/Completeness.lean:264.trans ⟨...⟩proof —rw/unfoldare fragile on abbrev+lambda under implicit transparency (the lambda elaborates to the unfolded→ Propform, defeq but not canonical)Neighborhood/Semantics/Filtration.lean(5 sites)Finset.mem_filter.mp) —rintro/rcasescannot whnf throughQuot.lifton a Finset filter, andsimp/rwwithFinset.mem_filtermake no progress on the non-canonical formNeighborhood/Semantics/AxiomN.leanContainsUnitinstance on the abbrev head — v4.33 instance search no longer unfoldsintermediateRelativeMaximalCanonicalModel(an abbrev ofrelativeBasicCanonicalModel) to match the general instanceBuild proofs (under v4.33.1, at the consumer pins)
lake build(default targets: Fin74 + Neighborhood): SUCCESS, 1230 jobslake build ModalLogicArchive.Modal.Kripke.Logic.S5: SUCCESS, 1081 jobssorrycount on all touched files: 0Relation to other work
coursia-archive-tableau-4.33.1): zero file overlap — fix(Archive): build the whole ModalLogicArchive under Lean 4.33.1 #1 coversModalLogicArchive/{Modal/Kripke,Modal/Tableau,Propositional}, this PR coverslean-toolchain,lake-manifest.json,Vorspiel,Logic,Modal/LogicSymbol,Neighborhood/*.formal_logic_leanmanifest) follows in a separate CoursIA PR after this one merges: See ModalLogic@71968137 : ModalLogicArchive.Modal.Tableau ne compile pas sous Lean 4.33.1 — Kripke/Logic/* inutilisable jsboige/CoursIA#17522.Merge criterion (coordinator): the CI build job of this PR must run under
v4.33.1— that is the point of the toolchain bump.See jsboige/CoursIA#17522
🤖 Generated with Claude Code