Commit graph

Select branches

Hide pull requests

master

Mono Color

• 56fe75eef4
  fix: prevent corruption of the small allocator state (#13548) Eric Wieser 2026-05-06 06:46:03 -07:00
• e3eb9aa832
  chore: rename reldebug preset to more appropriate relwithassert (#13657) Sebastian Ullrich 2026-05-06 15:27:53 +02:00
• 8d2b5d08a1
  perf: upgrade to LLVM 22 (#13545) Henrik Böving 2026-05-06 14:36:06 +02:00
• e6dfdfdcee
  fix: reject attribute uses whose module is reachable only via IR (#13613) Sebastian Ullrich 2026-05-06 13:55:43 +02:00
• 0e2088fc83
  feat: upstream unreachableTactic linter (#13580) Wojciech Różowski 2026-05-06 12:55:26 +01:00
• 9533f3f5ac
  doc: how to LLVM upgrade (#13656) Henrik Böving 2026-05-06 12:03:53 +02:00
• ea6e767078
  feat: rename --clippy to --extra and run defaults under it (#13649) Wojciech Różowski 2026-05-05 21:24:11 +01:00
• ad5ec0e196
  feat: user-specified init fn when loading plugins (#13510) Mac Malone 2026-05-05 16:20:54 -04:00
• 25ec7e5b0f chore: update stage0 Lean stage0 autoupdater 2026-05-05 18:38:42 +00:00
• 03bd8847dc
  fix: distinguish recursive applications by source position (#13645) Joachim Breitner 2026-05-05 18:40:29 +02:00
• 6998af1850
  fix: record instances unfolded by wrapInstance as shake dependencies (#13579) Sebastian Ullrich 2026-05-05 17:00:23 +02:00
• aa6fa1cf1a
  chore: use the lean-llvm LLVM for benchmarking (#13634) Henrik Böving 2026-05-05 16:26:08 +02:00
• e47636cdca
  chore: fix CI for PRs from external repos (#13643) Garmelon 2026-05-05 15:38:54 +02:00
• 42eb0385a5
  test: bring Sym-based mvcgen' on par with mvcgen (#13578) Sebastian Graf 2026-05-05 15:17:20 +02:00
• a43972c856
  chore: don't use grind in HTTP (#13639) Henrik Böving 2026-05-05 15:06:12 +02:00
• bd20c51ae4
  feat: add trace.Meta.Tactic.simp.backwardDefEq (#13640) Joachim Breitner 2026-05-05 15:02:27 +02:00
• e4c0a5a511
  fix: perform severity overrides before counting errors (#13589) Eric Wieser 2026-05-05 02:31:50 -07:00
• 94a29d1952
  fix: prevent undefined behavior without LEAN_MMAP (#13521) Eric Wieser 2026-05-05 00:42:20 -07:00
• 70098e432b
  fix: handle interrupted reads (#13493) Eric Wieser 2026-05-05 00:41:52 -07:00
• c9855f5dbf
  fix: propagate memory errors in mpz.cpp (#13547) Eric Wieser 2026-05-05 00:40:35 -07:00
• a2c4b7305d
  fix: indicate in readModuleDataParts if memory is exhausted (#13549) Eric Wieser 2026-05-05 00:38:46 -07:00
• 8ebd294673
  fix: kernel projection panic in Sym.simp match reduction (#13635) Leonardo de Moura 2026-05-04 20:20:20 -07:00
• 9e5c86eac9
  chore: move more radar bench logic to this repo (#13633) Garmelon 2026-05-04 20:21:22 +02:00
• c8191c5e2c
  refactor: align ScopedEnvExtension.exportEntry? with new PersistentEnvExtension.exportEntriesFn (#13628) Sebastian Ullrich 2026-05-04 17:35:59 +02:00
• 5f262d3b18
  chore: update release tooling and docs (#13631) Garmelon 2026-05-04 17:33:36 +02:00
• 666e8302c7
  chore: use self-hosted actions runner for some runs (#13543) Garmelon 2026-05-04 17:33:24 +02:00
• ba502f7027
  chore: rename UInt8.ofNatTruncate to UInt8.ofNatClamp (#13627) Julia Markus Himmel 2026-05-04 13:02:10 +02:00
• dae325700c
  fix: lake: await needs before processing module headers (#13601) Mac Malone 2026-05-03 14:17:08 -04:00
• 326f43aa3a
  fix: lake: meta import transitive import artifacts (#13600) Mac Malone 2026-05-03 13:44:46 -04:00
• 316c39ffe4
  fix: grind congruence-table invariant for lazy ite branches (#13624) Leonardo de Moura 2026-05-03 10:27:54 -07:00
• ee8acc14e2
  fix: grind cast internalization order (#13625) Leonardo de Moura 2026-05-03 09:32:10 -07:00
• 1b23b051f3
  fix: missing proof hints in grind propagators (#13623) Leonardo de Moura 2026-05-03 07:51:03 -07:00
• 2d79ec2883
  fix: another grind AC invariant (#13622) Leonardo de Moura 2026-05-03 06:33:13 -07:00
• fe3c7394fd
  fix: grind AC invariant (#13614) Leonardo de Moura 2026-05-02 19:19:51 -07:00
• 030397785c
  fix: missing case in processLevel at SymM (#13612) Leonardo de Moura 2026-05-02 10:52:43 -07:00
• 75e37def8c
  fix: remove incorrect assertion at Sym/Simp/Have.lean (#13611) Leonardo de Moura 2026-05-02 09:26:35 -07:00
• 508a113242
  feat: add .instances-transparency type-check diagnostics (#13368) Sebastian Ullrich 2026-05-02 14:17:51 +02:00
• b7ca76a96e
  chore: refine PR description guidance in .claude/CLAUDE.md (#13597) Sebastian Ullrich 2026-05-02 14:02:25 +02:00
• 4b8e74b27a
  chore: disable flaky test (#13603) Sebastian Ullrich 2026-05-02 13:58:17 +02:00
• 06ac472859
  feat: detect further sub-instances in wrapInstance (#13536) Sebastian Ullrich 2026-05-02 13:55:04 +02:00
• c53c4b4d2e
  fix: prevent private default instances from leaking into public scope (#13596) Sebastian Ullrich 2026-05-02 09:53:44 +02:00
• 659249a7df
  fix: always fail on unsolved metavariables after Verso docstring elab (#13574) David Thrane Christiansen 2026-05-02 00:34:52 +02:00
• 53db221124
  fix: disable model-based theory combination in grind derived tactics (#13593) Leonardo de Moura 2026-04-30 18:45:17 -07:00
• a9946fe4ac
  fix: case-split on arithmetic implications with And/Or antecedents (#13590) Leonardo de Moura 2026-04-30 16:15:34 -07:00
• 84f8c167c4
  feat: script for finding deprecated options, modules and syntax (#13586) Wojciech Różowski 2026-04-30 18:30:43 +01:00
• 427e3bcdbc
  fix: limit ring solver polynomial degree in grind (#13585) Leonardo de Moura 2026-04-30 07:00:00 -07:00
• 19baa470e5
  feat: MVarId.assertAfter fvar alias info, MVarId.replace mvar dependencies, specialize tactic using eta arguments (#13528) Kyle Miller 2026-04-30 03:36:29 -07:00
• ad5a3291dc
  chore: switch Invariant helpers from abbrev to def + @[simp] (#13583) Sebastian Graf 2026-04-30 11:57:44 +02:00
• 9efe4283e2
  fix: propagate parent cancel token to parallel tactic subtasks (#13428) Joachim Breitner 2026-04-30 11:22:33 +02:00
• 906d9cf848
  feat: add SPred and PostCond entailment lemmas (#13582) Sebastian Graf 2026-04-30 08:30:49 +02:00
• 2b5d154a4c
  feat: upstream unnecessarySeqFocus linter (#13540) Wojciech Różowski 2026-04-29 15:51:10 +01:00
• e6f44eeeec
  test: regression tests for do issues fixed by the new elaborator (#13541) Sebastian Graf 2026-04-29 16:37:23 +02:00
• 2ba4c55a84
  feat: upstream dupNamespace environment linter (#13538) Wojciech Różowski 2026-04-29 13:50:40 +01:00
• 897e556d90
  feat: add E-matching diagnostics to grind (#13558) Leonardo de Moura 2026-04-29 14:17:55 +02:00
• 10b2efba51
  feat: new foundations for mvcgen tactic (#12965) Vladimir Gladshtein 2026-04-29 19:28:30 +08:00
• b763ab8a5e
  refactor: keep IO.CancelToken task private, resolve promise before setting flag (#13569) Joachim Breitner 2026-04-29 13:12:54 +02:00
• 0a6c31520b
  doc: note TransparencyMode and ReducibilityStatus constructors are not in unfolding order (#13564) Kim Morrison 2026-04-29 14:22:55 +10:00
• 9df737d492
  fix: lake: race condition in monitor queue (#13559) Mac Malone 2026-04-28 18:44:48 -04:00
• 5852865c92
  fix: beta reduction in grind must respect generation threshold (#13560) Leonardo de Moura 2026-04-28 23:51:14 +02:00
• c36b0fb165
  refactor: make CancelToken Promise-based (#13303) Joachim Breitner 2026-04-28 23:50:54 +02:00
• 6819c805b9
  fix: propagate memory errors when allocating for libuv (#13546) Eric Wieser 2026-04-28 08:29:25 -07:00
• 1a15db69ec
  feat: lake: add support for running text linters from lake lint (#13513) Wojciech Różowski 2026-04-28 16:09:04 +01:00
• 432d11541b
  feat: add try? => tac syntax and parallel cancellation test (#13301) Joachim Breitner 2026-04-28 12:00:35 +02:00
• 87120c312e
  fix: typo in enableInitializersExecution error message (#13553) Kim Morrison 2026-04-28 11:13:30 +10:00
• 2ad0f96d48
  fix: avoid duplicate buffered writes when IO.Process.output exec fails (#13464) Kim Morrison 2026-04-28 09:51:20 +10:00
• 5b252f2c3d
  fix: surface meaningful pattern errors inside do-notation (#13542) Sebastian Graf 2026-04-27 23:12:04 +02:00
• 234186185d
  chore: fix missing dec on rare error path (#13551) Henrik Böving 2026-04-27 23:09:46 +02:00
• a2cf1d6e2a
  chore: remove namespace repo caching logic (#13539) Garmelon 2026-04-27 17:14:03 +02:00
• 7f5fac9d9f
  feat: add warn.redundantExpose for redundant @[expose]/@[no_expose] attributes (#13359) Sebastian Ullrich 2026-04-27 12:33:58 +02:00
• 824ccd9662 chore: update stage0 Lean stage0 autoupdater 2026-04-27 11:06:16 +00:00
• ac9a1cb415
  feat: add @[backward_defeq] attribute and local useBackward simp option (#13492) Joachim Breitner 2026-04-27 12:07:59 +02:00
• b0d6a3c283 chore: update stage0 Lean stage0 autoupdater 2026-04-27 10:14:31 +00:00
• 4d7b7dd8e6
  feat: support while let in do blocks via unified condition syntax (#13534) Sebastian Graf 2026-04-27 11:23:36 +02:00
• 3c6317b6d7
  feat: notify satellite solvers about asserted equalities in grind (#13532) Leonardo de Moura 2026-04-26 21:45:15 +02:00
• e843e5a155
  feat: add [no_fallback] attribute for tactic elaborators and macros (#13523) Sebastian Ullrich 2026-04-26 15:59:54 +02:00
• a21d3b1ef7
  test: copy srcHash test data to temp dir before modifying (#13524) Sebastian Ullrich 2026-04-26 10:13:39 +02:00
• 24bef91f9a
  test: tests/lake/run_test.sh (#13501) Mac Malone 2026-04-25 00:36:08 -04:00
• 09fabf3c39
  fix: lake: namespace in Lake.Util.Opaque (reapplied) (#13526) Mac Malone 2026-04-24 18:25:24 -04:00
• 5b87ab6625
  feat: use explicit allowlist instead of transparency bump in whnfMatcher (#13363) Joachim Breitner 2026-04-24 15:50:30 +02:00
• 45bdae81c9
  test: grind homomorphism predicates (#13520) Leonardo de Moura 2026-04-24 10:19:04 +02:00
• 2e48cd293a
  refactor: move Async and Http from Internal to Std (#13511) Sofia Rodrigues 2026-04-23 16:55:22 -03:00
• 5637b3374c
  refactor: lake: use modifyGet in StoreInsts (#13517) Mac Malone 2026-04-23 15:13:01 -04:00
• 848122d1f9
  fix: lake: namespace in Lake.Util.Opaque (#13516) Mac Malone 2026-04-23 14:50:26 -04:00
• 1e0ddbb90d
  fix: do not bump transparency to instances in eqn LHS whnf (#13512) Joachim Breitner 2026-04-23 13:58:10 +02:00
• e3d42400ce
  feat: inject unreachable! after break-less repeat (#13506) Sebastian Graf 2026-04-23 09:16:03 +02:00
• 525021c01e
  feat: pluggable pure/bind builders for do elaboration (#13507) Sebastian Graf 2026-04-23 09:15:25 +02:00
• 30a3fde8aa
  feat: lake: empty build detection & --allow-empty (#13500) Mac Malone 2026-04-22 23:27:29 -04:00
• 48c7a4f7d9
  feat: informative metavariable hovers, better delayed assignment pretty printing (#13446) Kyle Miller 2026-04-22 18:43:55 -07:00
• 87c123bb1b
  feat: lake: add support for running environment linters (#13431) Wojciech Różowski 2026-04-22 19:17:41 +01:00
• cae4decead
  test: speed up bench/mvcgen/sym ctest entry (#13498) Sebastian Graf 2026-04-22 15:41:07 +02:00
• a1240f7b80
  fix: correct alternative-fold base in do match (#13491) Sebastian Graf 2026-04-22 15:25:30 +02:00
• 2b99012545
  feat: split ControlInfo.noFallthrough from syntactic numRegularExits (#13502) Sebastian Graf 2026-04-22 14:32:11 +02:00
• b6f5892e22
  fix: leantar architecture detection for Linux aarch64 (#13499) Mac Malone 2026-04-22 01:20:59 -04:00
• 3387404f10
  chore: lake: rm autoParam in Lake.Load.Resolve (#13495) Mac Malone 2026-04-21 17:43:40 -04:00
• e542810e79
  test: grind homomorphism demo (#13497) Leonardo de Moura 2026-04-21 23:17:32 +02:00
• f32106283f
  fix: pin repeat's numRegularExits at 1 to match for (#13494) Sebastian Graf 2026-04-21 18:15:19 +02:00
• eadf1404c5 chore: update stage0 Lean stage0 autoupdater 2026-04-21 15:22:01 +00:00
• bf269ce250
  fix: preserve nesting level across empty doc snippet nesting (#13489) Robert J. Simmons 2026-04-21 08:58:52 -04:00
• 25bab8bcc4
  feat: server-side support for incremental diagnostics (#13260) Marc Huisinga 2026-04-21 14:48:15 +02:00
• fcaebdad22
  refactor: lake: fix setDepPkgs & further verify resolution (#13487) Mac Malone 2026-04-20 23:47:27 -04:00