Commit graph

Select branches

Hide pull requests

master

Mono Color

• fd2723d9c0
  feat: add linter for rfl simp theorems at restricted transparency (#13317) Leonardo de Moura 2026-04-07 21:49:07 -07:00
• ad2105dc94
  feat: add List.prod, Array.prod, and Vector.prod (#13200) Kim Morrison 2026-04-08 14:01:49 +10:00
• 235aedfaf7
  chore: use --wfail for core CI build (#13294) Mac Malone 2026-04-07 22:17:39 -04:00
• 30dca7b545
  fix: make delta-derived Prop-valued instances theorems (#13304) Kim Morrison 2026-04-08 11:19:48 +10:00
• 7e04970c58
  fix: skip nightly-testing merge when branch does not exist (#13308) Kim Morrison 2026-04-08 10:31:22 +10:00
• 0a6ee838df
  fix: update lean-toolchain in verso test-projects during release (#13309) Kim Morrison 2026-04-08 10:29:38 +10:00
• ec72785927
  chore: git ignore .claude/worktrees (#13299) Sebastian Graf 2026-04-07 11:51:39 +02:00
• ba33c3daa4
  fix: match stub signature of lean_uv_dns_get_info to real implementation (#13234) Keith Seim 2026-04-07 05:39:53 -04:00
• db1e2ac34c
  fix: add missing release() and adopt_lock_t to single-threaded unique_lock stub (#13233) Keith Seim 2026-04-07 05:30:13 -04:00
• cb06946972
  chore: fix typo in annotatedBorrows (#13276) Jason Yuen 2026-04-07 02:17:26 -07:00
• 4f6bcc5ada
  chore: avoid segfault in stage2 (#13296) Sebastian Ullrich 2026-04-07 11:08:04 +02:00
• 0650cbe0fa
  chore: fix typo in isInvalidContinuationByte (#13275) Jason Yuen 2026-04-07 02:01:19 -07:00
• 8bb07f336d
  chore: add leansqlite to release repos (#13293) Kim Morrison 2026-04-07 18:54:42 +10:00
• c16e88644c
  feat: Runtime.hold (#13270) Mac Malone 2026-04-07 04:44:35 -04:00
• 96d502bd11
  refactor: introduce LakefileConfig & well-formed workspaces (#13282) Mac Malone 2026-04-06 19:34:48 -04:00
• d48863fc2b
  fix: add checkInterrupted to Core.withIncRecDepth (#13290) Joachim Breitner 2026-04-06 15:45:30 +02:00
• c4a664eb5d
  fix: add checkSystem to LCNF compiler passes (#13231) Joachim Breitner 2026-04-06 11:35:58 +02:00
• 0cd6dbaad2
  feat: add Sym.Arith infrastructure for arithmetic normalization (#13289) Leonardo de Moura 2026-04-05 22:21:09 -07:00
• 34d00cb50d
  feat: add checkSystem calls to bv_decide for cancellation responsiveness (#13284) Joachim Breitner 2026-04-05 15:11:39 +02:00
• a73be70607
  doc: fix typo in doc of Functor.mapConst (#13285) Tom Levy 2026-04-05 21:16:49 +12:00
• 3d49476058 chore: update stage0 Lean stage0 autoupdater 2026-04-05 00:39:54 +00:00
• adc45d7c7b
  feat: mark exposed match auxiliary declarations as implicit_reducible (#13281) Leonardo de Moura 2026-04-04 16:55:47 -07:00
• 9efba691e7
  chore: fix typo in checkArtifactsExist (#13277) Jason Yuen 2026-04-04 11:56:10 -07:00
• 681856324f chore: update stage0 Lean stage0 autoupdater 2026-04-04 18:50:11 +00:00
• 9f49ea63e2
  feat: add backward.isDefEq.respectTransparency.types option (#13280) Leonardo de Moura 2026-04-04 11:05:33 -07:00
• 3770b3dcb8
  chore: fix spelling errors (#13274) Jason Yuen 2026-04-04 00:34:34 -07:00
• 3c6ea49d0e
  feat: add mkAppNS, mkAppRevS, betaRevS, betaS, and related Sym functions (#13273) Leonardo de Moura 2026-04-03 19:31:16 -07:00
• 608e0d06a8
  fix: extend sym canonicalizer reductions to value positions (#13272) Leonardo de Moura 2026-04-03 18:52:24 -07:00
• 5fdeaf0d5a
  fix: handle propositional and decidable instances in sym canonicalizer (#13271) Leonardo de Moura 2026-04-03 17:40:39 -07:00
• da91aed2e2
  feat: verification of String.dropWhile and String.takeWhile (#13155) Julia Markus Himmel 2026-04-03 16:02:21 +02:00
• e57d84bba0
  fix: show missing match cases in declaration order (#13266) Joachim Breitner 2026-04-03 15:33:54 +02:00
• 772b5663d2
  perf: correct over-allocated capacity for imported constant hashmaps (#13238) Sebastian Ullrich 2026-04-03 10:58:42 +02:00
• c7983a8c65
  perf: limit counter-example generation in match compiler (#13222) Joachim Breitner 2026-04-03 10:37:20 +02:00
• d3b04871f5
  perf: add checkInterrupted to inferType cache miss path (#13258) Joachim Breitner 2026-04-03 08:03:55 +02:00
• acae2b44fd
  feat: no default values for structure instance notation patterns (#13243) Kyle Miller 2026-04-02 20:25:23 -07:00
• fcc070f18f
  chore: getElemV tests (#13249) Paul Reichert 2026-04-02 23:24:04 +02:00
• 9aad86a576
  feat: allow deprecating options (#13195) Wojciech Różowski 2026-04-02 15:44:11 +01:00
• 2bcbb676f5
  chore: disable flaky tests (#13253) Garmelon 2026-04-02 14:59:59 +02:00
• f7ec39d6a1
  test: add empty-by completion tests and column-0 test marker (#13257) Joachim Breitner 2026-04-02 14:40:38 +02:00
• aaf0f6e7f5
  feat: add letConfig support to do block let/have (#13255) Sebastian Graf 2026-04-02 14:36:20 +02:00
• 5bf590e710
  chore: fixes from #13103 "enable separate codegen" (#13241) Sebastian Ullrich 2026-04-02 13:13:22 +02:00
• 159f069863 chore: update stage0 Lean stage0 autoupdater 2026-04-02 10:20:07 +00:00
• aa1144602b
  feat: add letConfig syntax to do block let/have parsers (#13250) Sebastian Graf 2026-04-02 11:40:44 +02:00
• ffc2c0ab1a
  chore: remove hardcoded maxSteps limit in Sym mvcgen' (#13252) Sebastian Graf 2026-04-02 11:16:43 +02:00
• 8dc4c16fce
  fix: correct String cases codegen to use String.toByteArray (#13242) Sebastian Ullrich 2026-04-02 10:17:20 +02:00
• 861bc19e0c
  feat: allow dotted function notation to use @ and explicit universes (#13245) Kyle Miller 2026-04-01 20:12:54 -07:00
• 8f1c18d9f4
  feat: pretty print level metavariables using index (#13030) Kyle Miller 2026-04-01 15:34:29 -07:00
• 097f3ebdbc
  perf: use memcmp for ByteArray equality (#13235) Henrik Böving 2026-04-01 17:30:03 +02:00
• 861f722844
  fix: handle multi-discriminant casesOn in WF unfold equation generation (#13232) Joachim Breitner 2026-04-01 17:23:13 +02:00
• eac9315962
  feat: add deprecated_module (#13002) Wojciech Różowski 2026-04-01 15:40:43 +01:00
• 8b52f4e8f7
  fix: make FirstTokens.seq (.optTokens _) .unknown return .unkown (#13205) Robin Arnez 2026-04-01 15:21:26 +02:00
• 402a6096b9
  fix: add checkSystem calls to long-running elaboration paths (#13220) Joachim Breitner 2026-04-01 14:54:57 +02:00
• 978bde4a0f chore: update stage0 Lean stage0 autoupdater 2026-04-01 12:56:25 +00:00
• 8aa0c21bf8
  chore: begin development cycle for v4.31.0 (#13230) Garmelon 2026-04-01 14:23:00 +02:00
• 1aa860af33
  fix: avoid heartbeat timeout in symbolFrequencyExt export (#13202) Sebastian Ullrich 2026-04-01 12:54:13 +02:00
• cdd982a030
  feat: add deprecated_syntax (#13108) Wojciech Różowski 2026-04-01 11:51:59 +01:00
• f11d137a30
  feat: add unlock_limits command to disable all resource limits (#13211) Sebastian Ullrich 2026-04-01 11:26:13 +02:00
• fc0cf68539
  fix: make -DLEAN_VERSION_* CMake overrides actually work (#13226) Kim Morrison 2026-04-01 16:31:23 +11:00
• 46a0a0eb59
  chore: add safety notes to release command (#13225) Kim Morrison 2026-04-01 16:01:00 +11:00
• 916004bd3c
  fix: add checkSystem calls to hasAssignableMVar (#13219) Joachim Breitner 2026-03-31 21:27:15 +02:00
• a145b9c11a
  chore: use FetchContent for mimalloc source acquisition (#13196) Nadja Yang 2026-03-31 14:00:39 -04:00
• 67b6e815b9
  chore: strip binaries only in release builds (#13208) Garmelon 2026-03-31 19:18:43 +02:00
• 33c3604b87
  fix: use correct shared library directory for Lake plugin on Windows (#13128) Kim Morrison 2026-04-01 03:33:58 +11:00
• 504e099c5d
  test: lazy let-binding unfolding in sym mvcgen (#13210) Sebastian Graf 2026-03-31 17:29:11 +02:00
• 17795b02ee
  fix: missing borrow annotations in Std.Internal.UV.System (#13172) Sofia Rodrigues 2026-03-31 12:10:23 -03:00
• 48800e438c
  fix: assorted fixes in the string library (#13201) Julia Markus Himmel 2026-03-31 08:28:20 +02:00
• f395593ffc
  feat: missingDocs linter warns about empty doc strings (#13188) Wojciech Różowski 2026-03-30 20:48:25 +01:00
• a88f81bc28
  test: use DFS ordering for subgoals in mvcgen (#13193) Sebastian Graf 2026-03-30 19:11:13 +02:00
• 313abdb49f
  fix: if _ : p ... syntax in new do elaborator (#13192) Sebastian Graf 2026-03-30 18:58:48 +02:00
• f08983bf01
  chore: support jj workspaces in cmake git hash detection (#13190) Sebastian Ullrich 2026-03-30 18:32:07 +02:00
• 22308dbaaa
  chore: CLAUDE.md individual module build instructions (#13189) Sebastian Ullrich 2026-03-30 16:30:16 +02:00
• 51e87865c5
  feat: add deprecated_arg attribute (#13011) Wojciech Różowski 2026-03-30 11:20:44 +01:00
• 75ec8e42c8
  test: simplify assumptions in mvcgen' with grind benchmark (#13186) Sebastian Graf 2026-03-30 12:03:43 +02:00
• 9fc62b7042
  chore: clean up old test artifacts (#13179) Sebastian Ullrich 2026-03-30 10:02:52 +02:00
• 583c223b16
  style: correct typos in comments and documentation (#13181) Yang Song 2026-03-30 08:00:18 +01:00
• ccc7157c08
  fix: expose grind gadgets abstractFn and simpMatchDiscrsOnly (#13177) Sebastian Ullrich 2026-03-29 12:37:54 +02:00
• 05046dc3d7 chore: update stage0 Lean stage0 autoupdater 2026-03-29 01:00:22 +00:00
• 43f18fd502
  fix: lake: large cache get bulk fetch (#13173) Mac Malone 2026-03-28 18:58:56 -04:00
• b06eb981a3
  fix: remove non-deterministic http-body test (#13175) Sofia Rodrigues 2026-03-28 17:36:35 -03:00
• f72137f53a
  feat: introduce Body type class and some Body types for HTTP (#12144) Sofia Rodrigues 2026-03-28 14:14:53 -03:00
• 96dbc324f3 chore: update stage0 Lean stage0 autoupdater 2026-03-28 05:24:36 +00:00
• d6e69649b6
  refactor: lake: fetch artifact URLs in a single Reservoir request (#13164) Mac Malone 2026-03-28 00:46:43 -04:00
• 337f1c455b chore: update stage0 Lean stage0 autoupdater 2026-03-28 03:21:53 +00:00
• 6871abaa44
  refactor: replace grind canonicalizer with type-directed normalizer (#13166) Leonardo de Moura 2026-03-27 19:43:22 -07:00
• 8c0bb68ee5
  perf: prevent unnecessary allocations of EST.Out.ok (#13163) Henrik Böving 2026-03-27 23:10:24 +01:00
• ae19b3e248 chore: update stage0 Lean stage0 autoupdater 2026-03-27 21:21:38 +00:00
• d0d135dbe2
  refactor: lake: log process output as info on errors (#13151) Mac Malone 2026-03-27 12:49:14 -04:00
• 088b299343 chore: update stage0 Lean stage0 autoupdater 2026-03-27 16:47:06 +00:00
• 82c35eb517
  refactor: rename goalDotAlt/goalCaseAlt to invariantDotAlt/invariantCaseAlt (#13160) Sebastian Graf 2026-03-27 17:01:32 +01:00
• abcf400e90
  perf: tagged values can be interpreted as borrowed (#13152) Henrik Böving 2026-03-27 16:55:57 +01:00
• 42854412c3
  refactor: use simpTelescope in mvcgen' simplifying_assumptions (#13159) Sebastian Graf 2026-03-27 16:48:35 +01:00
• c84aa086c7 chore: update stage0 Lean stage0 autoupdater 2026-03-27 15:17:24 +00:00
• 7168289c57
  refactor: make elabInvariants resilient to goalDotAlt/goalCaseAlt renames (#13137) Sebastian Graf 2026-03-27 15:30:19 +01:00
• febd1caf36
  doc: fix inferInstanceAs docstring (#13158) Sebastian Ullrich 2026-03-27 15:03:38 +01:00
• 79ac2d93b0 chore: update stage0 Lean stage0 autoupdater 2026-03-27 14:06:36 +00:00
• 210d4d00fa
  test: add simplifying_assumptions clause to mvcgen' tactic (#13156) Sebastian Graf 2026-03-27 14:16:23 +01:00
• 938c19aace
  chore: rename mvcgen_invariant_type attribute to spec_invariant_type, part 2 (#13157) Sebastian Graf 2026-03-27 14:06:17 +01:00
• e06fc0b5e8 chore: update stage0 Lean stage0 autoupdater 2026-03-27 12:26:23 +00:00
• f2d36227cf
  chore: rename mvcgen_invariant_type attribute to spec_invariant_type, part 1 (#13153) Sebastian Graf 2026-03-27 12:29:26 +01:00
• 0b401cd17c
  refactor: compile @[extern] via standard pipeline (#13102) Sebastian Ullrich 2026-03-27 11:31:22 +01:00