70 Pull requests merged by 16 people

• [Backport releases/v4.13.0] fix: lake: make package extraDep intransitive

  #5777 merged Oct 19, 2024

• [Backport releases/v4.13.0] refactor: lake: restrict cache fetch to leanprover*

  #5776 merged Oct 19, 2024

• feat: #version command

  #5768 merged Oct 18, 2024

• fix: structural nested recursion confused when nested type appears first

  #5766 merged Oct 18, 2024

• fix: include references in attributes in call hierarchy

  #5650 merged Oct 18, 2024

• chore: @hargoniX Std.Sat codeowner, fix Kim's user name

  #5765 merged Oct 18, 2024

• chore: check-prelude also for Std

  #5764 merged Oct 18, 2024

• fix: duplicate info trees from IO.processCommandsIncrementally

  #5763 merged Oct 18, 2024

• chore: deprecation for Array.data

  #5687 merged Oct 18, 2024

• feat: Lean.Expr.name?

  #5760 merged Oct 18, 2024

• fix: app unexpander for sorryAx

  #5759 merged Oct 18, 2024

• chore: upstream Array.reduceOption

  #5758 merged Oct 18, 2024

• chore: deprecate Nat.sum

  #5746 merged Oct 18, 2024

• feat: add Hashable instance for Char

  #5747 merged Oct 17, 2024

• fix: do not force snapshot tree too early

  #5752 merged Oct 17, 2024

• fix: some goal state issues

  #5677 merged Oct 17, 2024

• perf: do not lint unused variables defined in tactics by default

  #5338 merged Oct 17, 2024

• doc: remove docstring from implicitDefEqProofs

  #5751 merged Oct 17, 2024

• chore: remove SplitIf.ext cache

  #5571 merged Oct 17, 2024

• chore: move Array.mapIdx lemmas to new file

  #5748 merged Oct 17, 2024

• doc: point out that OfScientific is called with raw literals

  #5725 merged Oct 17, 2024

• chore: upstream List.foldxM_map

  #5697 merged Oct 17, 2024

• feat: change lake new math to use autoImplicit false

  #5715 merged Oct 17, 2024

• [Backport releases/v4.13.0] fix: don't block on snapshot tree if tracing is not enabled

  #5738 merged Oct 17, 2024

• fix: change String.dropPrefix? signature

  #5745 merged Oct 17, 2024

• chore: cleanup in Array/Lemmas

  #5744 merged Oct 17, 2024

• chore: move Antisymm to Std.Antisymm

  #5740 merged Oct 17, 2024

• chore: upstream basic material on Sum

  #5741 merged Oct 17, 2024

• chore: upstream ne_of_apply_ne

  #5743 merged Oct 17, 2024

• chore: upstream ne_of_mem_of_not_mem

  #5742 merged Oct 17, 2024

• chore: upstream material on Prod

  #5739 merged Oct 16, 2024

• chore: rename List.pure to List.singleton

  #5732 merged Oct 16, 2024

• fix: don't block on snapshot tree if tracing is not enabled

  #5736 merged Oct 16, 2024

• feat: UIntX.[val_ofNat, toBitVec_ofNat]

  #5735 merged Oct 16, 2024

• feat: add BitVec.(getMSbD, msb)_(add, sub) and BitVec.getLsbD_sub

  #5691 merged Oct 16, 2024

• chore: rename List.bind and Array.concatMap to flatMap

  #5731 merged Oct 16, 2024

• feat: DiscrTree: index the domain of ∀

  #5686 merged Oct 16, 2024

• fix: ac_nf0, simp_arith: don't tempt the kernel to reduce atoms

  #5708 merged Oct 16, 2024

• fix: make applyEdit optional in WorkspaceClientCapabilities of LSP

  #5224 merged Oct 16, 2024

• refactor: redefine unsigned fixed width integers in terms of BitVec

  #5323 merged Oct 16, 2024

• chore: remove instBEqNat, which is redundant with instBEqOfDecidableEq but not defeq

  #5694 merged Oct 16, 2024

• feat: push/pop tactic API

  #5720 merged Oct 16, 2024

• chore: upstream classical tactic

  #5730 merged Oct 16, 2024

• feat: Expr helper functions

  #5729 merged Oct 16, 2024

• chore: upstream String.dropPrefix?

  #5728 merged Oct 16, 2024

• chore: make getIntrosize public

  #5727 merged Oct 16, 2024

• fix: simpproc to reduce Fin literals consistently

  #5632 merged Oct 15, 2024

• refactor: remove mkRecursorInfoForKernelRec

  #5681 merged Oct 15, 2024

• fix: List.drop_drop addition order

  #5716 merged Oct 15, 2024

• feat: add BitVec.sdiv_[zero|one|self] theorems

  #5718 merged Oct 15, 2024

• chore: rename instDecidableEqQuotientOfDecidableEquiv to Quotient.decidableEq

  #5722 merged Oct 15, 2024

• feat: bv_decide inequality regression tests

  #5714 merged Oct 15, 2024

• chore: upstream List.sum, planning to later deprecate Nat.sum

  #5703 merged Oct 15, 2024

• chore: better default value for Array.swapAt!

  #5705 merged Oct 15, 2024

• feat: let dot notation see through CoeFun instances

  #5692 merged Oct 14, 2024

• feat: options pp.mvars.anonymous and pp.mvars.levels

  #5711 merged Oct 14, 2024

• chore: disable ac_nf by default

  #5673 merged Oct 14, 2024

• feat: add BitVec.[udiv|umod]_[zero|one|self] theorems

  #5712 merged Oct 14, 2024

• fix: the ⋯ elaboration warning did not mention pp.maxSteps

  #5710 merged Oct 14, 2024

• feat: use libuv for tempfiles

  #5135 merged Oct 14, 2024

• feat: denote deprecations in completion items

  #5707 merged Oct 14, 2024

• chore: remove @[simp] from Option.isSome_eq_isSome

  #5704 merged Oct 14, 2024

• chore: mark prefix_append_right_inj as simp lemma

  #5706 merged Oct 14, 2024

• chore: rename List.join to List.flatten

  #5701 merged Oct 14, 2024

• feat: lemmas about BitVector arithmetic inequalities

  #5646 merged Oct 14, 2024

• feat: upstream List.mapIdx, and add lemmas

  #5696 merged Oct 14, 2024

• chore: import orphaned Lean.Replay

  #5693 merged Oct 14, 2024

• chore: move BitVec.udiv/umod/sdiv/smod after add/sub/mul/lt

  #5623 merged Oct 13, 2024

• feat: complete BitVec.[getMsbD|getLsbD|msb] for shifts

  #5604 merged Oct 13, 2024

• feat: expand relationship with BitVec and toFin

  #5680 merged Oct 13, 2024

15 Pull requests opened by 7 people

• fix: have `Lake` not create core aliases into `Lake` namespace

  #5688 opened Oct 13, 2024

• fix: when pretty printing constant names, do not use aliases from "non-API `export`s"

  #5689 opened Oct 13, 2024

• feat: simp local confluence testing

  #5717 opened Oct 14, 2024

• feat: improved `calc` error messages

  #5719 opened Oct 15, 2024

• feat: add `BitVec.(msb, getMsbD, getLsbD)_(neg, abs)`

  #5721 opened Oct 15, 2024

• chore: simplify signature of Array.mapIdx

  #5749 opened Oct 17, 2024

• feat: compile against Windows SDK headers under Windows

  #5753 opened Oct 17, 2024

• feat: add Nat.log2_two_pow

  #5756 opened Oct 17, 2024

• feat: unique sorries

  #5757 opened Oct 17, 2024

• chore: pull `intMin` and `intMax` up

  #5762 opened Oct 18, 2024

• chore: mention `#version` in bug report template

  #5769 opened Oct 18, 2024

• feat: resolve generalized field notation using all parents

  #5770 opened Oct 19, 2024

• feat: add BitVec.toInt_sub, simplify BitVec.toInt_neg

  #5772 opened Oct 19, 2024

• feat: prove that `intMin` is indeed the smallest signed bitvector

  #5778 opened Oct 19, 2024

• feat: make `MessageData.ofConstName` be the default coercion from `Name` to `MessageData`

  #5779 opened Oct 19, 2024

12 Issues closed by 5 people

• `PANIC at outOfBounds` on theorem involving a nested inductive

  #5726 closed Oct 18, 2024

• Duplicate instances introduced through inheritance gives confusing errors

  #2952 closed Oct 18, 2024

• RFC: Provide a `leanpkg` binary to help confused new users

  #2872 closed Oct 18, 2024

• `show_term` and `by?` change order of elaboration

  #5713 closed Oct 18, 2024

• can't see goal state after case tactic

  #2881 closed Oct 17, 2024

• unwanted reduction when checking simp_arith proof objects

  #5384 closed Oct 16, 2024

• kernel hangs on ac_nf expression

  #5699 closed Oct 16, 2024

• Consider making WorkspaceClientCapabilities.applyEdit field Optionable

  #4541 closed Oct 16, 2024

• simp usually reduces `Fin n` literals, but not `n` itself

  #5630 closed Oct 15, 2024

• Dot notation and `CoeFun`

  #1910 closed Oct 14, 2024

• Unable to figure the term when destructing an inductive proposition

  #5700 closed Oct 14, 2024

• RFC: decide! tactic variant

  #5629 closed Oct 13, 2024

14 Issues opened by 12 people

• Kernel: infinite loop on nested inductive type

  #5775 opened Oct 19, 2024

• INTERNAL PANIC: unreachable code has been reached

  #5774 opened Oct 19, 2024

• Return types not inferred in presence of implicit variables of unknown type

  #5773 opened Oct 19, 2024

• Nat.repr slow for very large literals, quadratic algorithm

  #5771 opened Oct 19, 2024

• Cannot derive functional induction principle

  #5767 opened Oct 18, 2024

• `dsimp` simplifies too much

  #5755 opened Oct 17, 2024

• No docstring is show on `·` terms

  #5737 opened Oct 16, 2024

• clear does not work in `conv` mode

  #5734 opened Oct 16, 2024

• omega does not look through abbreviations in types

  #5733 opened Oct 16, 2024

• Deep kernel reduction detected after `simp`

  #5724 opened Oct 15, 2024

• rcases doesn't complain about unsynthesized placeholder

  #5723 opened Oct 15, 2024

• Application type mismatch in simp involving dsimp theorem

  #5702 opened Oct 14, 2024

• Universe level normalization has associativity of `max` backwards from parsing associativity

  #5695 opened Oct 14, 2024

• Recursive theorems with `cases` vs `match`

  #5690 opened Oct 13, 2024

46 Unresolved conversations

Sometimes conversations happen on old items that aren’t yet closed. Here is a list of all the Issues and Pull Requests with unresolved conversations.

• feat: add date and time functionality

  #4904 commented on Oct 18, 2024 • 60 new comments

• feat: Strict Ackermannization tactic (bv_ac_eager) for QF_UFBV

  #5657 commented on Oct 19, 2024 • 4 new comments

• RFC: make constructor tactic fail in ambiguous cases

  #3129 commented on Oct 18, 2024 • 0 new comments

• RFC: better UX around `throw`?

  #3128 commented on Oct 18, 2024 • 0 new comments

• RFC: A better error message for uncapitalized package name

  #3108 commented on Oct 18, 2024 • 0 new comments

• RFC: Make `IO` universe polymorphic

  #3011 commented on Oct 18, 2024 • 0 new comments

• Misleading import error message when imports are duplicated with different casing

  #2768 commented on Oct 18, 2024 • 0 new comments

• No progress indicator for a long time when downloading a project in VSCode

  #5615 commented on Oct 19, 2024 • 0 new comments

• Make `Decidable` a subtype of `Bool`

  #2038 commented on Oct 18, 2024 • 0 new comments

• feat: `opaque_repr` attribute to suppress "trivial structure" opt

  #2292 commented on Oct 16, 2024 • 0 new comments

• fix: don't write padding bits to olean files

  #2908 commented on Oct 18, 2024 • 0 new comments

• feat: allow `EStateM` to be used universe-polymorphically

  #3010 commented on Oct 19, 2024 • 0 new comments

• feat: error on non-rfl dsimp args

  #3087 commented on Oct 18, 2024 • 0 new comments

• fix: remove `Option.lt` and related components

  #3102 commented on Oct 18, 2024 • 0 new comments

• feat: `Simp.Config.implicitDefEqProofs`

  #4595 commented on Oct 17, 2024 • 0 new comments

• feat: `debug.proofAsSorry`

  #5140 commented on Oct 13, 2024 • 0 new comments

• chore: CI: build 64-bit platforms consistently with GMP

  #5144 commented on Oct 18, 2024 • 0 new comments

• Git conflict experiment

  #5500 commented on Oct 18, 2024 • 0 new comments

• chore: add LNSym omega benchmarks with large problems that take multiple seconds to solve

  #5622 commented on Oct 18, 2024 • 0 new comments

• test: add two benchmarks that are slow to parse or elaborate

  #5656 commented on Oct 18, 2024 • 0 new comments

• chore: add example where omega never terminates / runs out of heartbeats

  #5662 commented on Oct 18, 2024 • 0 new comments

• fix: RecursorVal.getInduct to return name of major argument’s type

  #5679 commented on Oct 15, 2024 • 0 new comments

• feat: update toolchain on `lake update`

  #5684 commented on Oct 20, 2024 • 0 new comments

• Delaboration of re-exported names

  #2524 commented on Oct 15, 2024 • 0 new comments

• Metavariable instantiation seems to slow down non-linearly in the size of the proof

  #5610 commented on Oct 17, 2024 • 0 new comments

• Slow elaboration of `List Nat` literals

  #5683 commented on Oct 18, 2024 • 0 new comments

• Instance creates defs regardless of whether the typeclass is Prop- or Type-valued

  #5672 commented on Oct 18, 2024 • 0 new comments

• `<|>` notation is not pretty-printed

  #5668 commented on Oct 18, 2024 • 0 new comments

• "failed to generate equational theorem" when matching on not only recursive call

  #5667 commented on Oct 18, 2024 • 0 new comments

• Structure eta doesn't work for nested inductives

  #5661 commented on Oct 18, 2024 • 0 new comments

• Meta.check does not check projections

  #5660 commented on Oct 18, 2024 • 0 new comments

• `rintro` error message is in the wrong place

  #5659 commented on Oct 18, 2024 • 0 new comments

• Namespace completion inserts full name rather than remainder

  #5654 commented on Oct 18, 2024 • 0 new comments

• "(kernel) unknown constant" when specializing a mutually recursive function

  #5651 commented on Oct 18, 2024 • 0 new comments

• macOS clang fails to link against dylib generated by Lean

  #5649 commented on Oct 18, 2024 • 0 new comments

• by? generates sorryAX instead of reporting proof

  #5625 commented on Oct 18, 2024 • 0 new comments

• Unexpected "invalid universe level" error using implicit variables

  #5621 commented on Oct 18, 2024 • 0 new comments

• "failed to generate unfold theorem" for recursive nested match

  #2962 commented on Oct 18, 2024 • 0 new comments

• Syntax pattern $foo:with_type fails unhelpfully

  #2957 commented on Oct 18, 2024 • 0 new comments

• `conv`-mode `congr` tactic fails with "over-applied" functions

  #2942 commented on Oct 18, 2024 • 0 new comments

• Renaming does not correctly deal with namespaces

  #2936 commented on Oct 18, 2024 • 0 new comments

• `linter.unusedVariables` false positive when used in `decreasing_by`

  #2920 commented on Oct 18, 2024 • 0 new comments

• MonadControlT is not the transitive closure of MonadControl

  #2894 commented on Oct 18, 2024 • 0 new comments

• Conv changing goals to metavariables with `pattern`.

  #2877 commented on Oct 18, 2024 • 0 new comments

• cases/induction does not connect reverted variables in info tree

  #2873 commented on Oct 18, 2024 • 0 new comments

• RFC: Overlapping matches and termination proofs

  #3136 commented on Oct 18, 2024 • 0 new comments