-
Notifications
You must be signed in to change notification settings - Fork 607
Insights: leanprover/lean4
Overview
Could not load contribution data
Please try again later
99 Pull requests merged by 18 people
-
feat: add
BitVec.msb_(smod, srem)#8974 merged
Jun 25, 2025 -
feat: refactor of Lean.Grind.ToInt and remaining instances
#8996 merged
Jun 25, 2025 -
feat: PULift
#8992 merged
Jun 25, 2025 -
refactor: linearNoConfusionType: use PULift, not
PUnit →#8973 merged
Jun 25, 2025 -
fix: add isDefEq check in the recursive call case of
solveMonoStepinsidemonotonicitytactic#8978 merged
Jun 25, 2025 -
feat: add ToInt typeclasses for grind
#8991 merged
Jun 25, 2025 -
feat: doc-strings for grind algebra classes
#8990 merged
Jun 25, 2025 -
chore: cleanup of grind in BitVec/Lemmas
#8989 merged
Jun 25, 2025 -
chore: updates to (failing) grind algebra tests
#8987 merged
Jun 25, 2025 -
feat: lake: avoid use of Lean root directories
#8981 merged
Jun 25, 2025 -
fix: congruence proof for over-applied terms
#8983 merged
Jun 24, 2025 -
fix: pass Lean CMake CI options to the Lake build
#8823 merged
Jun 24, 2025 -
feat: use
grindin BitVec/Lemmas#8967 merged
Jun 24, 2025 -
fix: linter.simpUnusedSimpArgs to check syntax kind
#8971 merged
Jun 24, 2025 -
chore: remove use of deprecated API
#8970 merged
Jun 24, 2025 -
feat: add
BitVec.(getElem, getLsbD, getMsbD)_(smod, sdiv, srem)#8941 merged
Jun 24, 2025 -
chore: cleanup after stage0 update
#8966 merged
Jun 24, 2025 -
feat: embed a NatModule in its IntModule completion
#8963 merged
Jun 24, 2025 -
feat: revise grind annotations for bitwise operations
#8965 merged
Jun 24, 2025 -
chore: add @[expose] in Grind/Ring/Poly.lean
#8964 merged
Jun 24, 2025 -
chore: adds (failing) grind algebra tests
#8961 merged
Jun 24, 2025 -
feat: move lean-pr-testing-NNNN branches to a fork
#8933 merged
Jun 24, 2025 -
feat: the grothendieck envelope of an ordered semiring is an ordered ring
#8959 merged
Jun 24, 2025 -
fix: better case-split for match-conditions in
grind#8958 merged
Jun 24, 2025 -
feat: add configuration for
let/havetactics#8957 merged
Jun 24, 2025 -
fix: avoid caching uses of
never_extractconstants in toLCNF#8956 merged
Jun 24, 2025 -
fix:
Lean.MVarId.deltaLocalDecl#8955 merged
Jun 24, 2025 -
feat: add
Meta.letToHaveand thelet_to_havetactic#8954 merged
Jun 24, 2025 -
feat: semiring normalizer in
grind#8953 merged
Jun 24, 2025 -
refactor: simplify semiring normalization helper theorems
#8946 merged
Jun 23, 2025 -
fix: correctly handle never_extract attribute in LCNF CSE
#8952 merged
Jun 23, 2025 -
chore: share leading prefix between then/else branches
#8951 merged
Jun 23, 2025 -
feat: server support for new module setup
#8699 merged
Jun 23, 2025 -
feat: ignore
lean -Rif module name is in setup#8874 merged
Jun 23, 2025 -
feat: add initial error explanations
#8934 merged
Jun 23, 2025 -
feat: make math Lake template follow Mathlib standards
#8866 merged
Jun 23, 2025 -
feat: semiring normalization theorems
#8943 merged
Jun 23, 2025 -
feat: add antitonicity lemmas for (co)inductive predicates
#8940 merged
Jun 23, 2025 -
fix: correct universe used in
below/brecOnfor non-reflexive inductive types#8937 merged
Jun 23, 2025 -
feat: linter.loopingSimpArgs
#8865 merged
Jun 23, 2025 -
chore: fix indentation
#8936 merged
Jun 23, 2025 -
feat:
let +generalize#8935 merged
Jun 23, 2025 -
chore: cleanup of grind's order typeclasses
#8913 merged
Jun 22, 2025 -
chore: for #8914 after stage0 update, part 2
#8931 merged
Jun 22, 2025 -
feat: use
nondepflag inExpr.letEandLocalContext.ldecl#8804 merged
Jun 22, 2025 -
fix: update
Parser.Term.letIdDeclNoBindersto use newletIdDeclformat#8929 merged
Jun 22, 2025 -
feat:
IO.FS.Stream.readToEnd#8886 merged
Jun 22, 2025 -
feat:
IO.FS.Stream.lines&IO.FS.Handle.lines#8887 merged
Jun 22, 2025 -
refactor: SimpM.run
#8843 merged
Jun 22, 2025 -
feat: linter.unusedSimpArgs
#8901 merged
Jun 22, 2025 -
chore: Revert "feat: Upstream
MPL.SPred.*frommpl"#8927 merged
Jun 22, 2025 -
chore: for #8914 after stage0 update
#8925 merged
Jun 22, 2025 -
chore: remove unused impure LCNF Phase
#8924 merged
Jun 22, 2025 -
feat: support casesOn for Thunk and Task
#8923 merged
Jun 22, 2025 -
feat: make
letandhaveterm syntaxes be consistent#8914 merged
Jun 22, 2025 -
feat: (commutative) semiring support in
grind#8921 merged
Jun 21, 2025 -
chore: remove more unused simp args
#8920 merged
Jun 21, 2025 -
perf: check simp cache in simpLoop
#8880 merged
Jun 21, 2025 -
refactor: simp arg elaboration
#8815 merged
Jun 21, 2025 -
fix: check guard_msgs.diff using .get rather than Options.getBool
#8918 merged
Jun 21, 2025 -
chore: add test for #4278, which was fixed by the new compiler
#8916 merged
Jun 21, 2025 -
fix: make sure local instance detection sees through reductions
#8903 merged
Jun 21, 2025 -
feat: refactor grind's typeclasses for ordered algebra
#8855 merged
Jun 21, 2025 -
feat:
NoNatZeroDivisorsforSemiringenvelope#8910 merged
Jun 21, 2025 -
refactor:
NoNatZeroDivisors#8909 merged
Jun 21, 2025 -
chore: allow
modulein tests#8881 merged
Jun 21, 2025 -
chore: remove staging workarounds
#8908 merged
Jun 21, 2025 -
feat: fix pretty printing of grind attributes
#8892 merged
Jun 21, 2025 -
chore: add a test for #4716, which is fixed by the new compiler
#8907 merged
Jun 21, 2025 -
chore: a few missing grind typeclass docstrings
#8906 merged
Jun 20, 2025 -
chore: remove unused simp args
#8905 merged
Jun 20, 2025 -
fix: make
mkHCongrWithArityForConst?compatible with parallelism#8899 merged
Jun 20, 2025 -
chore: add a test for #6957, fixed by the new compiler
#8904 merged
Jun 20, 2025 -
chore: add a test for #2602, which was fixed by the new compiler
#8902 merged
Jun 20, 2025 -
feat:
where ... finallysection to assign leftover goals#8723 merged
Jun 20, 2025 -
feat: Upstream
MPL.SPred.*frommpl#8745 merged
Jun 20, 2025 -
feat: enable the new compiler
#8577 merged
Jun 20, 2025 -
chore: Init: clean up some simp calls
#8897 merged
Jun 20, 2025 -
chore: remove old LEAN_AUTO_THREAD_FINALIZATION workaround
#8885 merged
Jun 20, 2025 -
chore: convert
DHashMapto a structure#8761 merged
Jun 20, 2025 -
fix: missing
isEqFalse#8893 merged
Jun 20, 2025 -
style: replace
HEq x ywithx ≍ y#8872 merged
Jun 20, 2025 -
feat: add doc-string to grind algebra typeclasses
#8890 merged
Jun 20, 2025 -
feat: improve error behavior of
endcommand#8387 merged
Jun 20, 2025 -
chore: minimize grind panic
#8889 merged
Jun 20, 2025 -
chore: @[expose] defs that appear in grind proof terms
#8882 merged
Jun 19, 2025 -
feat: BitVec.msb_sdiv
#8178 merged
Jun 19, 2025 -
chore: remove redundant field from Lean.Grind.IntModule
#8879 merged
Jun 19, 2025 -
feat: add grind annotations for List/Array/Vector monadic functions
#8878 merged
Jun 19, 2025 -
feat: grind annotations for List/Array/Vector.attach/pmap
#8877 merged
Jun 19, 2025 -
feat: generalize Lean.Grind.IsCharP to semirings
#8847 merged
Jun 19, 2025 -
chore: remove brittle new compiler tests that depend on internal decls
#8875 merged
Jun 19, 2025 -
chore: delete disabled new-compiler tests that are no longer very useful
#8873 merged
Jun 18, 2025 -
chore: address stage0 update TODOs
#8869 merged
Jun 18, 2025 -
feat:
ForIn'andsizefor iterators#8768 merged
Jun 18, 2025 -
fix: restore code action incrementality
#8868 merged
Jun 18, 2025 -
feat: add elaborators, completions, and hovers for named errors
#8730 merged
Jun 18, 2025 -
feat: add leading zero counter
BitVec.clzand bitblaster circuit/infrastructure#8546 merged
Jun 18, 2025
22 Pull requests opened by 16 people
-
feat: links libidn2
#8871 opened
Jun 18, 2025 -
perf: better isDefEq cache in the presence of metavariables
#8883 opened
Jun 19, 2025 -
fix: `match` discriminant congruence in `simp`
#8884 opened
Jun 19, 2025 -
feat: improve error message when passing local hypotheses to `grind`
#8891 opened
Jun 20, 2025 -
perf: use `MVarId.assign` instead of `isDefEq` in type class search
#8915 opened
Jun 21, 2025 -
fix: use an unreachable default for cases with > 2 alts
#8917 opened
Jun 21, 2025 -
feat: lake: local artifact cache
#8922 opened
Jun 22, 2025 -
feat: Upstream `MPL.SPred.*` from `mpl`
#8928 opened
Jun 22, 2025 -
fix: remove the IR elim_dead_branches pass
#8932 opened
Jun 23, 2025 -
feat: introduce slices
#8947 opened
Jun 23, 2025 -
feat: add `BitVec.toFin_(sdiv, smod, srem)` and `BitVec.toNat_srem`
#8950 opened
Jun 23, 2025 -
feat: optimized simp routine for let telescopes
#8968 opened
Jun 24, 2025 -
feat: introduce `MonadLiftT Id m`
#8977 opened
Jun 24, 2025 -
fix: make hasLocalInst ignore instance params of erased type
#8979 opened
Jun 24, 2025 -
chore: use `note` and `hint'` for message addenda
#8980 opened
Jun 24, 2025 -
chore: try to expose more of Lean.Grind.CommRing
#8985 opened
Jun 25, 2025 -
feat: improve projection and field-notation errors
#8986 opened
Jun 25, 2025 -
fix: do not assign mvars when validating unification hint conclusion
#8988 opened
Jun 25, 2025 -
feat: generalize withCtor functions to eliminate to Sort
#8994 opened
Jun 25, 2025 -
feat: Hoare logic for monadic programs and verification condition generation
#8995 opened
Jun 25, 2025 -
chore: initial Grove setup
#8997 opened
Jun 25, 2025 -
doc: review Repr and Format docstrings
#8998 opened
Jun 25, 2025
11 Issues closed by 5 people
-
non-linear `noConfusionType` construction: universes too complicated in `noConfusionType.withCtorType`
#8962 closed
Jun 25, 2025 -
Monotonicity tactic on mutual blocks with distinct `Order` instances
#8894 closed
Jun 25, 2025 -
unusedSimpArgs linter confused by syntax antiquotation
#8969 closed
Jun 24, 2025 -
New compiler surprisingly eliminating calls to `dbg_trace`
#8944 closed
Jun 24, 2025 -
Compilation with `MonadLog` for a `StateT` is surprisingly slow
#5457 closed
Jun 23, 2025 -
RFC: simp to detect, report and ignore inherently looping rewrite rules
#5111 closed
Jun 23, 2025 -
RFC: Make `simp only` warn on unused list elements
#4483 closed
Jun 22, 2025 -
`Thunk.casesOn` and `Task.casesOn` cause segfault when used
#8659 closed
Jun 22, 2025 -
Segmentation Fault with mutual, HashMap, and string interpolation
#5188 closed
Jun 20, 2025 -
Compiler error with `casesOn`
#2121 closed
Jun 20, 2025
10 Issues opened by 8 people
-
@[expose] instance implementations via `deriving`
#8984 opened
Jun 25, 2025 -
unsound `unif_hint` can cause crash
#8982 opened
Jun 24, 2025 -
Error message regression for nested inductive types
#8960 opened
Jun 24, 2025 -
RFC: Remove Redundant Deprecation Warnings
#8942 opened
Jun 23, 2025 -
@[expose] vs. AbstractNestedProofs vs. nested structural recursion
#8939 opened
Jun 23, 2025 -
@[expose] vs. AbstractNestedProofs vs. functional induction
#8938 opened
Jun 23, 2025 -
RFC: revisit error ranges for `by`, `.`, `next`, `case`
#8919 opened
Jun 21, 2025 -
Lake panics when creating new project with a numeric name
#8912 opened
Jun 21, 2025 -
`(kernel) deep recursion detected` error with `BitVec.umulOverflow` in an if-then-else
#8898 opened
Jun 20, 2025
53 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 `lean_setup_libuv` for initializing required LIBUV components
#8636 commented on
Jun 25, 2025 • 6 new comments -
feat: add DNS resolution functions to the standard library
#8072 commented on
Jun 25, 2025 • 4 new comments -
feat: add system information functions to the standard library
#8109 commented on
Jun 18, 2025 • 3 new comments -
feat: add fast circuit for unsigned multiplication overflow detection `fastUmulOverflow_eq` and definitions
#7858 commented on
Jun 24, 2025 • 2 new comments -
feat: monadic interface for asynchronous operations in Std
#8003 commented on
Jun 25, 2025 • 1 new comment -
Error "(kernel) application type mismatch" in theorem on inductive type
#8839 commented on
Jun 20, 2025 • 0 new comments -
Slow code generation for an instance declaration
#6328 commented on
Jun 20, 2025 • 0 new comments -
Bad performance on iterated HOrElse
#2227 commented on
Jun 20, 2025 • 0 new comments -
Linearisation failure in `Array.mapMUnsafe`
#4699 commented on
Jun 21, 2025 • 0 new comments -
INTERNAL PANIC: unreachable code has been reached
#5774 commented on
Jun 21, 2025 • 0 new comments -
Inferred value for implicit argument leads to suboptimal IR
#4157 commented on
Jun 21, 2025 • 0 new comments -
Some functions using `List.foldr` are specialized for common argument types before the tail-recursive `foldr` is available
#7750 commented on
Jun 21, 2025 • 0 new comments -
Can't compile for loop with two mut vars in an if branch
#7874 commented on
Jun 24, 2025 • 0 new comments -
Turning `abbrev` into `def` defeats type inference
#8766 commented on
Jun 25, 2025 • 0 new comments -
Universe level normalization has associativity of `max` backwards from parsing associativity
#5695 commented on
Jun 25, 2025 • 0 new comments -
feat: define `Squash` as a `Quotient`
#6642 commented on
Jun 21, 2025 • 0 new comments -
fix: finalize libuv
#7752 commented on
Jun 19, 2025 • 0 new comments -
chore: update to mimalloc 3.0.3 beta
#7786 commented on
Jun 20, 2025 • 0 new comments -
test: FunInd vs. module system
#8151 commented on
Jun 23, 2025 • 0 new comments -
chore: `Decidable` as subtype of `Bool` using the new compiler
#8309 commented on
Jun 21, 2025 • 0 new comments -
feat: use Meta.letToHave
#8373 commented on
Jun 24, 2025 • 0 new comments -
feat: add word-level hint suggestion diffs
#8574 commented on
Jun 23, 2025 • 0 new comments -
feat: polymorphic ranges
#8784 commented on
Jun 25, 2025 • 0 new comments -
doc: fix typo in docstring for `fieldIdxKind`
#8814 commented on
Jun 19, 2025 • 0 new comments -
draft: range migration test run
#8841 commented on
Jun 21, 2025 • 0 new comments -
feat: complete level def eq
#8867 commented on
Jun 24, 2025 • 0 new comments -
RFC: linters should be able to use try this
#4363 commented on
Jun 20, 2025 • 0 new comments -
If-then-else breaks apparent linearity
#2218 commented on
Jun 20, 2025 • 0 new comments -
Linear code leads to non-linear IR
#6058 commented on
Jun 20, 2025 • 0 new comments -
Revise closed term extraction
#467 commented on
Jun 20, 2025 • 0 new comments -
Invalid projection on field of a dependent cast in a dependent structure constructor
#1370 commented on
Jun 20, 2025 • 0 new comments -
"unknown free variable" kernel error with complex `do` block
#1415 commented on
Jun 20, 2025 • 0 new comments -
Compiler error with subtypes of erased types
#2104 commented on
Jun 20, 2025 • 0 new comments -
Code generator support for recursors
#2049 commented on
Jun 20, 2025 • 0 new comments -
Do notation inhibits tail call optimization
#444 commented on
Jun 20, 2025 • 0 new comments -
Fields having inductive types with trivial structure are always stored boxed
#2589 commented on
Jun 20, 2025 • 0 new comments -
"compiler IR check failed" error when trying to create `ToString` instance
#2602 commented on
Jun 20, 2025 • 0 new comments -
using Option.attach can crash lean
#6957 commented on
Jun 20, 2025 • 0 new comments -
unknown free variable: _kernel_fresh.1210
#4548 commented on
Jun 20, 2025 • 0 new comments -
Control run-time execution of pure functions
#8591 commented on
Jun 20, 2025 • 0 new comments -
bug: projection on `unsafeCast` leads to "unknown free variable: _neutral" error/segfault
#8407 commented on
Jun 20, 2025 • 0 new comments -
unknown free variable since v4.8.0
#4418 commented on
Jun 20, 2025 • 0 new comments -
SIGSEGV in elaboration
#4703 commented on
Jun 20, 2025 • 0 new comments -
Closed term extraction for large list literals produces large call stacks
#6047 commented on
Jun 20, 2025 • 0 new comments -
Importing a `Lean` module inflates binary size
#5274 commented on
Jun 20, 2025 • 0 new comments -
kernel invalid projection in old code generator
#3761 commented on
Jun 20, 2025 • 0 new comments -
compiler produces `(kernel) function expected`
#1774 commented on
Jun 20, 2025 • 0 new comments -
Decide on memory representation of opaque type definitions
#1536 commented on
Jun 20, 2025 • 0 new comments -
FFI generates boxed accessor for a trivial structure containing a UInt64 inside nontrivial structure
#4278 commented on
Jun 20, 2025 • 0 new comments -
Add a safe wrapper around `ptrEq`
#1502 commented on
Jun 20, 2025 • 0 new comments -
Closed-term extraction creates out-of-bound array accesses
#1965 commented on
Jun 20, 2025 • 0 new comments -
Mutual recursion and `@[specialize]` lead to `(kernel) deep recursion detected`
#4716 commented on
Jun 20, 2025 • 0 new comments