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

Commit Graph

  • a93ea184fe fix: status and chunkedbuffer Sofia Rodrigues 2026-01-25 11:19:34 -03:00
  • c309a3c07e feat: basic headers structure to more structured approach Sofia Rodrigues 2026-01-23 17:58:44 -03:00
  • 30641c617f feat: data components Sofia Rodrigues 2026-01-23 17:14:53 -03:00
  • ab0ef0e37b fix: remove unnecessary Functor constraint from LogT.run Kim Morrison 2026-03-02 13:54:27 +00:00
  • 6bebf9c529 feat: add short-circuit evaluation for Or and And in cbv (#12763) Wojciech Różowski 2026-03-02 13:47:04 +00:00
  • 04ccf7cb28 fix: remove expected constructorNameAsVariable warnings from unrelated tests Kim Morrison 2026-03-02 13:46:47 +00:00
  • df74c80973 feat: add bitblasting circuit for BitVec.cpop (#12433) Luisa Cicolini 2026-03-02 14:38:04 +01:00
  • 37fcb2ce55 refactor: comments Sofia Rodrigues 2026-03-02 09:22:43 -03:00
  • 7865841547 fix: use LinterOptions in constructorNameAsVariable linter Kim Morrison 2026-03-02 12:17:59 +00:00
  • e53f219d14 feat: also use ReaderT.run instead of function application Kim Morrison 2026-03-02 11:53:34 +00:00
  • 34a113119d chore: inline getLinterConstructorNameAsVariable Kim Morrison 2026-03-02 11:41:52 +00:00
  • df766e2ac4 Merge branch 'master' into constructorNameAsVariable_all Kim Morrison 2026-03-02 11:40:00 +00:00
  • 54aae0a320 perf: make instantiateAllMVars universal and expose instantiateMVarsOriginal Joachim Breitner 2026-03-02 11:32:31 +00:00
  • 85c15561dd perf: two-pass architecture and scope-tracked sharing for instantiateAllMVars Joachim Breitner 2026-03-02 10:13:47 +00:00
  • 3be124112c don't save to png file paul/array-mergeSort Paul Reichert 2026-02-25 15:13:48 +01:00
  • c74a93b72c don't save to png file Paul Reichert 2026-02-25 15:12:58 +01:00
  • bba4444539 clean up Paul Reichert 2026-02-25 10:27:19 +01:00
  • 1611ac1067 clen up readme Paul Reichert 2026-02-19 19:05:48 +01:00
  • 8c6f1d825b clean up Paul Reichert 2026-02-19 18:54:29 +01:00
  • 05b773ff0c chore: update benchmark scripts for per-pattern output format Paul Reichert 2026-02-19 17:41:57 +00:00
  • f81b24c9f0 perf: report per-pattern mergeSort benchmark results Paul Reichert 2026-02-19 17:09:37 +00:00
  • a253f86d88 benchmarks; need to wait until stack overflow is solved Paul Reichert 2026-02-16 14:27:05 +01:00
  • 2379950f38 cleanups Paul Reichert 2026-02-09 15:40:49 +01:00
  • 3a253294e0 lemmas Paul Reichert 2026-02-09 15:38:53 +01:00
  • c76c0f9c42 remove todos Paul Reichert 2026-02-09 14:32:47 +01:00
  • 0a5285bb4e fixes Paul Reichert 2026-02-09 10:49:05 +01:00
  • 87f9c0e808 poc Paul Reichert 2026-02-09 10:42:53 +01:00
  • ec41585523 sum consumer paul/iterators/improvements2 Paul Reichert 2026-02-10 18:27:51 +01:00
  • a94e8e6549 wip Paul Reichert 2026-02-10 17:53:51 +01:00
  • 2a3ee666d9 lemmas Paul Reichert 2026-02-10 17:35:17 +01:00
  • 292b423a17 feat: injectivity lemmas for getElem(?) on List and Option (#12435) Paul Reichert 2026-03-02 10:44:45 +01:00
  • f63c803585 test performance implications of implicit_reducible paul/shouldInline_simplify Paul Reichert 2026-03-02 10:25:44 +01:00
  • 3aff8d1c0d refactor: replace isImplicitReducible with Meta.isInstance in shouldInline shouldInline_simplify Leonardo de Moura 2026-03-01 20:36:24 -08:00
  • 645422aac6 feat(Std.Do): add ExceptConds.and_elim_left/right Kim Morrison 2026-03-02 05:41:49 +00:00
  • a584f8857c fix: unset project(LEAN) version variables that shadow cache Kim Morrison 2026-03-02 03:10:25 +00:00
  • 9540117acb Merge remote-tracking branch 'origin/master' into kimmo/check-stage0-version Kim Morrison 2026-03-02 02:51:55 +00:00
  • cda84702e9 doc: add guidance on waiting for CI/merges in release command (#12755) paul/base/iterators/improvements2 Kim Morrison 2026-03-02 13:49:34 +11:00
  • 457f3c20cf chore: update stage0 paul/idlint Paul Reichert 2026-03-01 22:49:20 +00:00
  • 1cad6c7de6 feat: add linter.warnOnUnfold to detect Id defeq abuse Paul Reichert 2026-03-01 22:38:22 +00:00
  • 132b5efb0f feat: add deriving noncomputable instance syntax Kim Morrison 2026-03-01 21:58:47 +00:00
  • 91c43040f4 doc: add guidance on waiting for CI/merges in release command doc/release-wait-guidance Kim Morrison 2026-03-01 21:40:18 +00:00
  • b9bfacd2da doc: add guidance on waiting for CI/merges in release command Kim Morrison 2026-03-01 21:40:18 +00:00
  • 1e12c1c2e4 chore: CI: bump actions/create-github-app-token from 2.0.2 to 2.2.1 dependabot/github_actions/actions/create-github-app-token-2.2.1 dependabot[bot] 2026-03-01 20:35:17 +00:00
  • e560f1b24e chore: CI: bump actions/upload-artifact from 5 to 7 dependabot/github_actions/actions/upload-artifact-7 dependabot[bot] 2026-03-01 20:35:11 +00:00
  • 277030ce43 chore: CI: bump actions/download-artifact from 7 to 8 dependabot/github_actions/actions/download-artifact-8 dependabot[bot] 2026-03-01 20:35:06 +00:00
  • 19413a20b5 chore: CI: bump dawidd6/action-download-artifact from 11 to 16 dependabot/github_actions/dawidd6/action-download-artifact-16 dependabot[bot] 2026-03-01 20:35:02 +00:00
  • 97cd66afde fix: comments Sofia Rodrigues 2026-03-01 16:45:51 -03:00
  • 82171a6bff cleanups paul/humanevup-34 paul/base/idlint Paul Reichert 2026-02-25 13:42:30 +01:00
  • b7993076a8 more lemmas Paul Reichert 2026-02-25 11:18:58 +01:00
  • d3854d8482 toArray/keysArray lemmas Paul Reichert 2026-02-13 21:34:54 +01:00
  • 161eaf29db feat: use terminology "non-recursive structure" instead of "struct-like". kmill_nonrecstruct_5891 Kyle Miller 2026-03-01 10:41:33 -08:00
  • d34f670487 doc: add stage0 editing guidance to CLAUDE.md Kim Morrison 2026-03-01 12:33:39 +00:00
  • 4962edfada Revert "doc: add stage0 editing guidance to CLAUDE.md" Kim Morrison 2026-03-01 12:33:20 +00:00
  • 86a8eb0051 doc: add stage0 editing guidance to CLAUDE.md Kim Morrison 2026-03-01 12:30:33 +00:00
  • b06e91ee3d fix: make -DLEAN_VERSION_* CMake overrides actually work Kim Morrison 2026-03-01 12:15:41 +00:00
  • 5d86aa4032 fix: set implicitReducible on grandparent subobject projections (#12701) v4.29.0-rc3 Kim Morrison 2026-03-01 17:39:17 +11:00
  • fd226c813d fix: use _fvar._ instead of _ for anonymous fvars (#12745) Kim Morrison 2026-03-01 20:59:13 +11:00
  • ca43b60947 [Backport releases/v4.29.0] feat: add pp.fvars.anonymous option (#12744) github-actions[bot] 2026-03-01 22:42:45 +11:00
  • 6979644c23 [Backport releases/v4.29.0] fix: mark levelZero, levelOne, and Level.ofNat as implicit_reducible (#12743) github-actions[bot] 2026-03-01 22:42:27 +11:00
  • ec565f3bf7 fix: use _fvar._ instead of _ for anonymous fvars (#12745) Kim Morrison 2026-03-01 20:59:13 +11:00
  • cd5ab6f9f9 fix: use _fvar._ instead of _ for anonymous fvars kim/pp-fvars-anonymous-fix Kim Morrison 2026-02-27 02:27:04 +00:00
  • feea8a7611 fix: use pull_request_target for label-triggered workflows (#12638) Kim Morrison 2026-03-01 19:20:56 +11:00
  • c873b4fab5 chore: retrigger CI fix-bot-approval-workflows Kim Morrison 2026-03-01 18:58:31 +11:00
  • 541a078f6f feat: add pp.fvars.anonymous option (#12688) backport-12688-to-releases/v4.29.0 Kim Morrison 2026-03-01 17:43:14 +11:00
  • 555b3cdc42 fix: mark levelZero, levelOne, and Level.ofNat as implicit_reducible (#12719) backport-12719-to-releases/v4.29.0 Kim Morrison 2026-03-01 17:37:54 +11:00
  • 6d305096e5 chore: fix profiler shebang and add profiling skill (#12519) Kim Morrison 2026-03-01 18:09:33 +11:00
  • 235b0eb987 feat: add Meta.synthInstance.apply trace class (#12699) Kim Morrison 2026-03-01 18:06:56 +11:00
  • 4937725202 Merge remote-tracking branch 'origin/master' into fix-bot-approval-workflows Kim Morrison 2026-03-01 17:52:02 +11:00
  • 5dd8d570fd feat: add pp.fvars.anonymous option (#12688) Kim Morrison 2026-03-01 17:43:14 +11:00
  • 3ea59e15b8 fix: set implicitReducible on grandparent subobject projections (#12701) Kim Morrison 2026-03-01 17:39:17 +11:00
  • d59f229b74 fix: mark levelZero, levelOne, and Level.ofNat as implicit_reducible (#12719) Kim Morrison 2026-03-01 17:37:54 +11:00
  • 6dbb6b8d0e Merge branch 'sofia/async-http-h1' into sofia/async-http-server Sofia Rodrigues 2026-02-28 15:41:39 -03:00
  • 4306782b93 Merge branch 'sofia/async-http-uri' into sofia/async-http-server Sofia Rodrigues 2026-02-28 15:41:35 -03:00
  • 6935306439 Merge branch 'sofia/async-http-body' into sofia/async-http-h1 Sofia Rodrigues 2026-02-28 15:41:25 -03:00
  • 1aa23cd92b Merge branch 'sofia/async-http-uri' into sofia/async-http-body Sofia Rodrigues 2026-02-28 15:41:18 -03:00
  • 0bb4ba72d4 Merge branch 'sofia/async-http-headers' into sofia/async-http-uri Sofia Rodrigues 2026-02-28 15:41:11 -03:00
  • 57a4d9ad4b Merge branch 'sofia/async-http-data' into sofia/async-http-headers Sofia Rodrigues 2026-02-28 15:41:04 -03:00
  • bfc6617c12 fix: method Sofia Rodrigues 2026-02-28 15:40:55 -03:00
  • c1b5b64797 Merge branch 'sofia/async-http-h1' into sofia/async-http-server Sofia Rodrigues 2026-02-28 12:41:44 -03:00
  • 9b563220b2 fix: strict method Sofia Rodrigues 2026-02-28 12:41:39 -03:00
  • 0eb4a6e8c6 fix: timeout and config Sofia Rodrigues 2026-02-28 12:40:46 -03:00
  • ced99013a3 Update tests joachim/kernel-delta-level-check copilot/fix-is-delta-level-check Joachim Breitner 2026-02-28 12:37:36 +00:00
  • 02a499c3fd Apply suggestion from @nomeata Joachim Breitner 2026-02-28 13:18:44 +01:00
  • 31630a8e29 chore: remove accidentally committed CodeQL build artifacts copilot-swe-agent[bot] 2026-02-28 11:38:27 +00:00
  • 525b5326e5 fix: move thm-is-prop check after check_constant_val in add_theorem for robustness copilot-swe-agent[bot] 2026-02-28 11:37:57 +00:00
  • 6d15f48bb4 chore: revert unrelated .gitignore changes copilot-swe-agent[bot] 2026-02-28 09:56:17 +00:00
  • 2c6ee17548 perf: add instantiateAllMVars for call sites where all mvars are assigned Joachim Breitner 2026-02-28 09:54:53 +00:00
  • 4390e2988f chore: remove accidentally committed CodeQL build artifacts and add to .gitignore copilot-swe-agent[bot] 2026-02-28 09:54:10 +00:00
  • 5f32014930 No additional changes - finalizing PR state copilot-swe-agent[bot] 2026-02-28 09:46:48 +00:00
  • 8361416a9a fix: move level param check into is_delta to prevent crash (#10577) copilot-swe-agent[bot] 2026-02-28 09:25:56 +00:00
  • 547ac1e0ec Initial plan copilot-swe-agent[bot] 2026-02-28 08:55:22 +00:00
  • a364595111 chore: fix ci after new linter was added (#12733) Garmelon 2026-02-28 04:05:07 +01:00
  • 4614def4cd Merge branch 'sofia/async-http-h1' into sofia/async-http-server Sofia Rodrigues 2026-02-27 21:14:21 -03:00
  • c97dfe585a feat: headers rfc refs Sofia Rodrigues 2026-02-27 21:14:09 -03:00
  • 74ecbca430 feat: tests Sofia Rodrigues 2026-02-27 21:12:33 -03:00
  • 08ab8bf7c3 chore: fix ci for new test suite (#12704) Garmelon 2026-02-28 00:25:37 +01:00
  • ae9230f19f Merge branch 'nightly-with-mathlib' of https://github.com/leanprover/lean4 into joachim/instantiateMVarsNoUpdate Joachim Breitner 2026-02-27 23:14:02 +00:00
  • 0cc92df9ad Undo changes to Injective Joachim Breitner 2026-02-27 23:13:17 +00:00
  • c5d6267cb8 perf: use instantiateMVarsNoUpdate as drop-in replacement Joachim Breitner 2026-02-27 23:04:34 +00:00
  • 54df5173d2 chore: update stage0 Lean stage0 autoupdater 2026-02-27 21:05:46 +00:00