sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 10:24:07 +00:00
Code Issues Packages Projects Releases Wiki Activity

Commit Graph

  • 87bff2fa39 chore: fix update-stage0 with make build hbv/fix_stage0 Henrik Böving 2026-03-17 09:59:44 +00:00
  • b88612de62 chore: fix tests readert-update Henrik Böving 2026-03-17 10:08:48 +00:00
  • 34a7523611 chore: fix update-stage0 with make build Henrik Böving 2026-03-17 09:59:44 +00:00
  • 0ded1b629c mark it Henrik Böving 2026-03-17 09:29:14 +00:00
  • 3c32607020 fix: incorrect borrow annotation on demangleBtLinCStr leading to segfault on panic (#12939) master Sebastian Ullrich 2026-03-17 10:24:57 +01:00
  • 6714601ee4 fix: remove accidental type monomorphism in Id.run_seqLeft (#12936) nightly Eric Wieser 2026-03-16 23:43:51 -07:00
  • 6b604625f2 fix: add missing pp-spaces in grind_pattern (#11686) damiano 2026-03-17 04:15:02 +00:00
  • e96b0ff39c fix: use response files on all platforms to avoid ARG_MAX (#12540) Kim Morrison 2026-03-17 15:14:37 +11:00
  • 50ee6dff0a chore: update leantar to v0.1.19 (#12938) Kim Morrison 2026-03-17 14:55:21 +11:00
  • 3682604b78 chore: update leantar to v0.1.19 leantar-v0.1.19 Kim Morrison 2026-03-17 03:45:31 +00:00
  • 9e0aa14b6f feat: lake: fixedToolchain package configuration (#12935) Mac Malone 2026-03-16 22:37:55 -04:00
  • 19a1f578b1 refactor: rename MultiMap to IndexMultiMap sofia/async-http-headers Sofia Rodrigues 2026-03-16 19:13:08 -03:00
  • 5c685465bd chore: handle absence of meld in fix_expected.py (#12934) Garmelon 2026-03-16 20:07:44 +01:00
  • ef87f6b9ac chore: delete temp files before, not after tests (#12932) Garmelon 2026-03-16 20:02:28 +01:00
  • 5713082070 Map signals on c++ side to actual values joscha/fix-signal-numbers Joscha 2026-03-16 18:48:44 +01:00
  • e5b3a41247 fix: use process signal numbers from correct architecture Joscha 2026-03-12 19:05:00 +01:00
  • 49715fe63c chore: improve how test suite interacts with stages (#12913) Garmelon 2026-03-16 16:20:03 +01:00
  • 40d55c1eb6 fix: internal Sofia Rodrigues 2026-03-16 10:56:34 -03:00
  • af40af987c fix: tests sofia/async-http-client Sofia Rodrigues 2026-03-16 10:45:35 -03:00
  • 133fd016b4 chore: update stage0 Lean stage0 autoupdater 2026-03-16 13:15:14 +00:00
  • 76e593a52d fix: rename Int.sq_nonnneg to Int.sq_nonneg (#12909) Bhavik Mehta 2026-03-16 10:52:57 +00:00
  • fa9a32b5c8 fix: correct swapped operands in Std.Time subtraction instances (#12919) Jesse Alama 2026-03-16 11:52:06 +01:00
  • 5ab45e12ca first attempt hbv/lcnf_preserve_infer_annotations Henrik Böving 2026-03-06 16:09:33 +00:00
  • 0f2532f683 preserve in early pipeline Henrik Böving 2026-03-06 14:04:42 +00:00
  • 2d999d7622 refactor: ignore borrow annotations at export/extern tricks (#12930) Henrik Böving 2026-03-16 11:03:40 +01:00
  • ddd5c213c6 chore: CLAUDE.md: stage 2 build instructions (#12929) Sebastian Ullrich 2026-03-16 10:47:14 +01:00
  • c9ceba1784 fix: use null-safe while-read loop for subverso manifest sync (#12928) Kim Morrison 2026-03-16 19:17:32 +11:00
  • 0bbadfa02a feat: add Meta.synthInstance.apply trace class (#12699) releases/v4.29.0 Kim Morrison 2026-03-01 18:06:56 +11:00
  • 04d3ba35de feat: add structured TraceResult to TraceData (#12698) Kim Morrison 2026-03-10 13:42:57 +11:00
  • a813ce37fc fix: use null-safe while-read loop for subverso manifest sync fix-release-steps-subverso-sync Kim Morrison 2026-03-16 08:07:39 +00:00
  • b1ce232903 fix: use null-safe while-read loop for subverso manifest sync Kim Morrison 2026-03-16 08:07:39 +00:00
  • 57df23f27e feat: lake: cached compressed module artifacts (#12914) Mac Malone 2026-03-16 00:36:19 -04:00
  • 65da1ee047 feat: client Sofia Rodrigues 2026-03-16 00:01:33 -03:00
  • ea8fca2d9f refactor: lake: download arts by default in cache get (#12927) Mac Malone 2026-03-15 22:29:44 -04:00
  • 274997420a refactor: remove backward compatibility options from iterator/slice/range modules (#12925) Paul Reichert 2026-03-15 15:03:51 +01:00
  • 3896dfbf01 remove +instances paul/respectTransparency-cleanup Paul Reichert 2026-03-15 13:26:27 +01:00
  • 6790d3807f fixes Paul Reichert 2026-03-15 12:52:18 +01:00
  • bb4fcceace cleanups Paul Reichert 2026-03-15 12:04:57 +01:00
  • 6631352136 fix: remove accidentally added code from Sym.Simp.Pattern (#12926) Wojciech Różowski 2026-03-15 10:30:26 +00:00
  • 31883fa970 cleanups Paul Reichert 2026-03-15 10:43:18 +01:00
  • 8d13eabc30 fix: remove unused length simp argument in TakeDrop list_len_issue Leonardo de Moura 2026-03-15 01:41:44 +00:00
  • 9661c3ab67 test: add regression test for List.length implicit reducibility Leonardo de Moura 2026-03-15 01:27:05 +00:00
  • 38c4fd4afd fix: mark List.length as @[implicit_reducible] Leonardo de Moura 2026-03-15 01:25:12 +00:00
  • cfa8c5a036 fix: handle universe level commutativity in sym pattern matching (#12923) nightly-with-mathlib nightly-with-manual Leonardo de Moura 2026-03-14 18:06:16 -07:00
  • b81e51512d fix: handle universe level commutativity in sym pattern matching sym_bug_2 Leonardo de Moura 2026-03-15 00:42:36 +00:00
  • 7120d9aef5 fix: eta-reduce expressions in sym discrimination tree lookup (#12920) Leonardo de Moura 2026-03-14 09:57:10 -07:00
  • 2c46bd5639 fix: eta-reduce expressions in sym discrimination tree lookup sym_bugs Leonardo de Moura 2026-03-14 16:44:35 +00:00
  • c2d4079193 perf: optimize string literal equality simprocs for kernel efficiency (#12887) Joachim Breitner 2026-03-14 11:30:31 +01:00
  • 3064709349 perf: use Char.toNat + Nat.ne_of_beq_eq_false in string ne proofs joachim/string-neq-proc3 Joachim Breitner 2026-03-12 15:28:11 +00:00
  • aaaf1dcc23 perf: use get!Internal and drop+cons_ne_nil in string ne proofs Joachim Breitner 2026-03-12 15:21:36 +00:00
  • 005e81b788 perf: optimize string literal equality simprocs for kernel efficiency Joachim Breitner 2026-03-11 14:27:23 +00:00
  • 59f88e6663 perf: add persistent Sym.Simp cache and reassocNatAdd simproc to mvcgen' with grind mvcgen-with-grind Sebastian Graf 2026-03-14 06:42:10 +00:00
  • d4884cde14 fix: client uri Sofia Rodrigues 2026-03-14 00:48:51 -03:00
  • 49da0f2d9c Merge branch 'sofia/async-http-server' into sofia/async-http-client Sofia Rodrigues 2026-03-13 23:58:02 -03:00
  • 7fbecca6f0 fix: test Sofia Rodrigues 2026-03-13 23:54:45 -03:00
  • ae5a3d2c8b Merge branch 'sofia/async-http-h1' into sofia/async-http-server Sofia Rodrigues 2026-03-13 23:51:15 -03:00
  • 1a270555ae fix: uri Sofia Rodrigues 2026-03-13 23:51:00 -03:00
  • 72702c3538 Merge branch 'sofia/async-http-body' into sofia/async-http-h1 Sofia Rodrigues 2026-03-13 23:47:38 -03:00
  • e86dbf3992 Merge branch 'sofia/async-http-uri' into sofia/async-http-body Sofia Rodrigues 2026-03-13 23:46:40 -03:00
  • d71f0bdae7 fix: uri test Sofia Rodrigues 2026-03-13 23:46:35 -03:00
  • 6ae49d7639 Merge branch 'sofia/async-http-body' into sofia/async-http-h1 Sofia Rodrigues 2026-03-13 23:13:32 -03:00
  • 232d173af3 Merge branch 'sofia/async-http-uri' into sofia/async-http-body Sofia Rodrigues 2026-03-13 23:13:19 -03:00
  • 3a4a309aed feat: split uri types Sofia Rodrigues 2026-03-13 23:13:05 -03:00
  • 033b7b537a feat: client Sofia Rodrigues 2026-03-13 22:42:43 -03:00
  • 47b3be0524 feat: update RPC wire format (#12905) Wojciech Nawrocki 2026-03-13 19:46:16 -04:00
  • c86b59d6d0 Fix lakeprof_report_upload joscha/bench-suite-improvements Joscha 2026-03-13 20:10:44 +01:00
  • 920a3ee317 Update lint.py Joscha 2026-03-13 17:34:14 +01:00
  • 1f2819252a Update run_test and run_bench scripts Joscha 2026-03-13 17:30:55 +01:00
  • 67352d7a21 Update docs Joscha 2026-03-13 17:32:47 +01:00
  • e4b01709b1 Replace env_*.sh mechanism Joscha 2026-03-13 17:27:21 +01:00
  • de2b177423 fix: make cbv_opaque take precedence over cbv_eval (#12908) Wojciech Różowski 2026-03-13 14:52:33 +00:00
  • a32173e6f6 feat: add tracing to cbv (#12896) Wojciech Różowski 2026-03-13 12:05:49 +00:00
  • f39f6dcb1a Merge remote-tracking branch 'origin/master' into mvcgen-with-grind Sebastian Graf 2026-03-13 07:35:23 +00:00
  • 8fc4ea8493 refactor: reuse Grind.withProtectedMCtx in sym VCGen emitVC Sebastian Graf 2026-03-13 07:11:15 +00:00
  • e6d9220eee test: add dite and match splitting to sym-based MVCGen (#12903) Sebastian Graf 2026-03-13 06:39:43 +08:00
  • 0007ffa16a refactor: simplify mkBackwardRuleForSplit and fix fvar alt handling sg/sym-mvcgen-split Sebastian Graf 2026-03-12 11:08:51 +00:00
  • 4261fbe8ce Revert "WIP" Sebastian Graf 2026-03-12 10:03:28 +00:00
  • ea0a4ea329 WIP Sebastian Graf 2026-03-12 10:03:27 +00:00
  • 8bed0ff972 refactor: extract SplitInfo.withAbstract and SplitInfo.expr into Split.lean Sebastian Graf 2026-03-12 09:16:52 +00:00
  • 86773abb9e refactor: use SplitInfo.splitWith for matcher splitting in sym MVCGen Sebastian Graf 2026-03-12 07:28:32 +00:00
  • 239b520a8c chore: better comments and names Sebastian Graf 2026-03-12 07:23:32 +00:00
  • 8afae00064 refactor: merge two-phase split proof into single pass with metavariables Sebastian Graf 2026-03-12 07:11:45 +00:00
  • d1c1a7242c refactor: clean up split backward rule generation in sym MVCGen Sebastian Graf 2026-03-11 18:55:14 +00:00
  • f70abe08a5 feat: add dite and matcher splitting to sym-based MVCGen Sebastian Graf 2026-03-11 13:08:19 +00:00
  • aae827cb4c refactor: replace flat Array Expr with TransformAltFVars in MatcherApp.transform (#12902) Sebastian Graf 2026-03-13 05:48:08 +08:00
  • 9c87a9f044 Merge branch 'sofia/async-http-h1' into sofia/async-http-server sofia/async-http-server Sofia Rodrigues 2026-03-12 15:52:36 -03:00
  • 34c9cafc12 fix: type sofia/async-http-h1 Sofia Rodrigues 2026-03-12 15:52:29 -03:00
  • 014dd1d263 Merge branch 'sofia/async-http-h1' into sofia/async-http-server Sofia Rodrigues 2026-03-12 15:43:28 -03:00
  • 2a7a407875 Merge branch 'sofia/async-http-body' into sofia/async-http-h1 Sofia Rodrigues 2026-03-12 15:43:06 -03:00
  • e359001026 Merge branch 'sofia/async-http-uri' into sofia/async-http-body sofia/async-http-body Sofia Rodrigues 2026-03-12 15:39:08 -03:00
  • 72244398dc fix: test sofia/async-http-uri Sofia Rodrigues 2026-03-12 15:38:59 -03:00
  • c0e60b797c Merge branch 'sofia/async-http-uri' into sofia/async-http-body Sofia Rodrigues 2026-03-12 15:33:48 -03:00
  • 400908a2f4 fix: port and fragment Sofia Rodrigues 2026-03-12 15:09:49 -03:00
  • 394c999c2a fix: uri Sofia Rodrigues 2026-03-12 15:03:49 -03:00
  • b7e88dadeb Merge branch 'sofia/async-http-headers' into sofia/async-http-uri Sofia Rodrigues 2026-03-12 15:01:03 -03:00
  • a39a0575a0 Merge branch 'master' into sofia/async-http-headers Sofia Rodrigues 2026-03-12 14:35:25 -03:00
  • 5815f33342 Merge branch 'sofia/fix-native-decide' into sofia/async-http-headers Sofia Rodrigues 2026-03-12 14:17:13 -03:00
  • 47833725ea feat: add String simprocs to cbv (#12888) Wojciech Różowski 2026-03-12 11:52:06 +00:00
  • 24acf2b895 chore: update stage0 Lean stage0 autoupdater 2026-03-11 21:36:12 +00:00
  • d9ebd51c04 feat: option to ignore borrowing annotations completely (#12886) Henrik Böving 2026-03-11 21:59:06 +01:00