nightly-2025-01-17

Changes since nightly-2025-01-16:

Full commit log

• e3fd954 chore: update stage0
• b7815b5 feat: add lcAny constant to Prelude (#6665)
• 7f0ae22 fix: don't filter out local instances in LCNF toMono pass (#6664)
• 35a4da2 feat: add simp-like parameters to grind (#6675)
• 60142c9 chore: remove unneeded instance (#6671)
• 17c0187 fix: add workaround for MessageData limitations (#6669)
• e42f7d9 feat: equality resolution for grind (#6663)
• 906aa1b feat: add Nat.[shiftLeft_or_distrib, shiftLeft_xor_distrib, shiftLeft_and_distrib, testBit_mul_two_pow, bitwise_mul_two_pow, shiftLeft_bitwise_distrib] (#6630)
• f015271 feat: align List.replicate/Array.mkArray/Vector.mkVector lemmas (#6667)

nightly-2025-01-16

Changes since nightly-2025-01-15:

Full commit log

• f4c9934 feat: Vector.getElem_flatMap (#6661)
• 80ddbf4 feat: align List/Array/Vector.flatMap (#6660)
• 3a6c5cf feat: canonicalizer diagnostics (#6662)
• af4a7d7 fix: grind term preprocessor (#6659)
• 6259b47 feat: improve case-split heuristic used in grind (#6658)
• 0050e93 refactor: lake: use StateRefT for BuildStore (#6290)
• 64cf5e5 feat: improve grind search procedure (#6657)
• 127b3f9 feat: more grind tests (#6650)
• 65175dc feat: improvegrind diagnostic information (#6656)
• 54f06cc feat: better support for partial applications in the E-matching procedure (#6654)
• b3f8fef fix: improve E-matching pattern selection heuristics (#6653)
• 6665837 feat: verify insertMany method for adding lists to HashMaps (#6211)
• c7fd873 feat: tag lemmas
• a10ce94 chore: update stage0
• 838ad28 feat: add the int_toBitVec simpset
• a1ef26b perf: improve bv_decide preprocessing based on Bitwuzla optimisations (#6641)

nightly-2025-01-15

Changes since nightly-2025-01-14:

Full commit log

• a955708 fix: grind canonicalizer state management (#6649)
• 0f7f80a fix: indicate dependency on pkgconf in ubuntu docs (#6646)
• 8d69909 feat: literals, lower and upper bounds in the offset constraint module within grind (#6648)
• f95d810 chore: fib_correct monadic reasoning example as a test (#6647)
• 5d6bf75 feat: align List/Array/Vector flatten lemmas (#6640)
• 563d5e8 feat: offset equalities in grind (#6645)
• 3da7f70 fix: indicate dependency on pkgconf in macOS docs (#6643)
• 8e5a3e4 chore: remove duplicate branch in LCNF.toMonoType (#6644)
• 9dbe5e6 refactor: bv_normalize simp set and implementation (#6639)
• c12b1d0 chore: fix docstring in Bitvec.toNat_add_of_lt (#6638)
• 85294b8 chore: update release checklist (#6637)
• 821c9b7 feat: faster, linear HashMap.alter and modify (#6573)

nightly-2025-01-14

Changes since nightly-2025-01-10:

Full commit log

• e9bd980 fix: Windows stage0 linking (#6622)
• 05aa256 feat: model construction for offset constraints (#6636)
• d6f0c32 chore: display E-matching theorems in goalToMessageData (#6635)
• f57745e feat: improve grind failure message (#6633)
• 749a82a fix: lake: set MACOSX_DEPLOYMENT_TARGET for shared libs (#6631)
• 85560da chore: remove functions for compiling decls from Environment (#6600)
• e6a6437 feat: implement basic async IO with timers (#6505)
• 30ba383 feat: lean --src-deps (#6427)
• 734fca7 feat: UIntX.toBitVec lemmas (#6625)
• a6eea4b fix: lake: v4.16.0-rc1 trace issues (#6627)
• 8483ac7 fix: adjustments to the datetime library (#6431)
• 5f41cc7 fix: trace indentation in info view (#6597)
• 2421f7f feat: exhaustive offset constraint propagation in the grind tactic (#6618)
• 40efbb9 doc: commit conventions and Mathlib CI (#6605)
• 603108e feat: finish alignment of List/Array/Vector.append lemmas (#6617)
• aa95a1c chore: cleaunp grind tests (#6616)
• af8f3d1 feat: avoid some redundant proof terms in grind (#6615)
• c7939cf feat: offset constraints support for the grind tactic (#6603)
• 0da3624 fix: allow dot idents to resolve to local names (#6602)
• 349da6c feat: improve [grind =] attribute (#6614)
• 5419025 feat: improve case split heuristic used in grind (#6613)
• 8b1aabb feat: lemmas about Array.append (#6612)
• ce1ff03 fix: checkParents in grind (#6611)
• c5c1278 fix: bug in the grind propagator (#6610)
• 5119528 feat: improve case-split heuristic used in grind (#6609)
• 4636091 fix: simp_arith (#6608)
• 7ea5504 feat: add support for splitting on <-> to grind (#6607)
• acad587 fix: pattern selection for local lemmas (#6606)
• 8791a9c chore: add lean4-cli to release checklist (#6596)
• 03081a5 doc: update FFI description for Int and signed fixed-width ints (#6599)
• 918924c feat: BitVec.{toFin, toInt, msb}_umod (#6404)
• 58cd011 chore: update stage0
• 0b5d977 feat: BitVec.toNat theorems for rotateLeft and rotateRight (#6347)
• ed309dc feat: add decidable instances for comparison operation of time offset types (#6587)

nightly-2025-01-10

Changes since nightly-2025-01-09:

Full commit log

• d2c4471 feat: BitVec.{toInt, toFin, msb}_udiv (#6402)
• c07948a feat: add simp? and dsimp? in conversion mode (#6593)
• d369976 feat: improve inequality offset support theorems for grind (#6595)
• a6789a7 feat: Std.Net.Addr (#6563)
• 1b42728 feat: add UInt32.{lt, le} (#6591)

nightly-2025-01-09

Changes since nightly-2025-01-08:

Full commit log

• dd64455 feat: improve grind canonicalizer diagnostics (#6588)
• 827c667 feat: align List/Array lemmas for filter/filterMap (#6589)
• 623dec1 feat: aligning List/Array/Vector lemmas for map (#6586)
• cb9f198 fix: grind canonicalizer (#6585)
• c5314da feat: add helper theorems for handling offsets in grind (#6584)
• 0afa1d1 feat: apply E-matching for local lemmas in grind (#6582)
• ddd454c feat: add grind configuration options to control case-splitting (#6581)
• 5be241c fix: forall propagation in grind (#6578)
• 034bc26 feat: make classical tactic incremental (#6575)
• 680ede7 fix: set LLVM sysroot consistently (#6574)
• 48eb308 perf: speed up JSON serialisation (#6479)
• f01471f fix: proper "excess binders" error locations for rintro and intro (#6565)

nightly-2025-01-08

Changes since nightly-2025-01-07:

Full commit log

• 00ef231 feat: split on match-expressions in the grind tactic (#6569)
• 9040108 feat: add BitVec.[toNat|toInt|toFin|getLsbD|getMsbD|getElem|msb]_fill (#6177)
• 91cbd7c feat: BitVec.toInt_shiftLeft theorem (#6346)
• 18b183f feat: let induction take zero alteratives (#6486)
• 78ed072 feat: add Int.emod_sub_emod and Int.sub_emod_emod (#6507)
• 22a7995 feat: add support for cast, Eq.rec, Eq.ndrec to grind (#6568)
• 5decd2c feat: trace messages for working and closing goals in the grind tactic (#6567)
• 0da5be1 feat: add support for erasing the [grind] attribute (#6566)
• 83098cd chore: typos / improvements to grind messages (#6561)
• a2a525f fix: set absolute linker path (#6547)

nightly-2025-01-07

Changes since nightly-2025-01-06:

Full commit log

• 97d07a5 feat: basic case-split for grind (#6559)
• a424029 feat: Array lemma alignment; fold and map (#6546)
• db3ab39 feat: propagate implication in the grind tactic (#6556)
• 8dec579 feat: grind tests for basic category theory (#6543)
• 3ca3f84 fix: avoid new tokens _=_ and =_ (#6554)
• 2c9641f doc: modify aesop usage example of omegaDefault (#6549)

nightly-2025-01-06

Changes since nightly-2025-01-05:

Full commit log

• 78ddee9 feat: release checklist script (#6542)
• 2ed77f3 feat: attribute [grind] (#6545)
• 76f883b fix: remove unused -static-libgcc MinGW linker arg (#6535)
• 675244d feat: [grind_eq] attribute for the grind tactic (#6539)
• fd091d1 feat: pattern normalization in the grind tactic (#6538)
• 7b29f48 fix: E-matching thresholds in the grind tactic (#6536)
• fb506b9 fix: allow projections in E-matching patterns (#6534)

nightly-2025-01-05

Changes since nightly-2025-01-04:

Full commit log

• dc5c809 feat: add term offset support to the grind E-matching modulo (#6533)
• 9dcbc33 chore: fix signature of perm_insertIdx (#6532)
• d22233f fix: let_fun support in grind (#6531)
• a5b1ed9 fix: nondeterministic failure in grind (#6530)
• ad2c16d feat: add support for let-declarations to grind (#6529)
• 37127ea fix: missing propagation in grind (#6528)
• 31435e9 doc: fix broken code blocks in RELEASES.md (#6527)