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

  • a0680192e0 perf: remove void JP arguments hbv/void_jp_args Henrik Böving 2026-03-04 15:22:01 +00:00
  • 4005bd027b fix: size Sofia Rodrigues 2026-03-04 12:04:53 -03:00
  • 551086c854 feat: add core HTTP data types (#12126) Sofia Rodrigues 2026-03-04 11:32:29 -03:00
  • 36f05c4a18 fix: deriving instance should not require noncomputable for Prop-valued classes (#12789) Kim Morrison 2026-03-05 00:26:20 +11:00
  • fbf03e31f9 Merge branch 'sofia/async-http-data' into sofia/async-http-headers Sofia Rodrigues 2026-03-04 10:21:46 -03:00
  • 39ab2b289c test: move test from encode to the uri tests Sofia Rodrigues 2026-03-04 10:20:25 -03:00
  • b613add013 fix: deriving instance should not require noncomputable for Prop-valued classes kim/deriving-prop-noncomputable Kim Morrison 2026-03-04 13:14:49 +00:00
  • 6c6f9a5d83 refactor: change Char.isDigit and Char.isAlpha sofia/async-http-data Sofia Rodrigues 2026-03-04 10:00:41 -03:00
  • 41cb6dac1d chore: fix verso sub-manifest subverso sync in release_steps (#12787) Kim Morrison 2026-03-05 00:00:30 +11:00
  • 47b7c7e65e perf: add high priority to OfSemiring.Q instances (#12782) Leonardo de Moura 2026-03-04 04:58:15 -08:00
  • a7aea9a12d style: format Sofia Rodrigues 2026-03-04 09:50:15 -03:00
  • 162f99d998 test: update expected output in Module/Imported.lean grind_tc_issue Kim Morrison 2026-03-04 12:40:24 +00:00
  • 9e94b2e35b test: update expected output for instance priority change Kim Morrison 2026-03-04 12:39:20 +00:00
  • 9517b5bc2d fix: h1 informational Sofia Rodrigues 2026-03-04 09:27:56 -03:00
  • df3f685be1 chore: use de-modulized subverso rev for verso test-project sub-manifests chore-verso-submanifest-sync Kim Morrison 2026-03-04 12:06:52 +00:00
  • 1c61ba6420 chore: use de-modulized subverso rev for verso test-project sub-manifests Kim Morrison 2026-03-04 12:06:45 +00:00
  • cbee80d92c chore: improve CI failure reporting in release checklist (#12786) Kim Morrison 2026-03-04 22:55:34 +11:00
  • 1c60b40261 fix: parse LEAN_VERSION_MINOR correctly in release_checklist.py (#12785) Kim Morrison 2026-03-04 22:51:43 +11:00
  • a44644068c chore: fix verso sub-manifest subverso sync in release_steps Kim Morrison 2026-03-04 11:49:57 +00:00
  • 51cdf26936 chore: fix verso sub-manifest subverso sync in release_steps Kim Morrison 2026-03-04 11:48:55 +00:00
  • b1bf026f88 chore: improve CI failure reporting in release checklist chore-ci-failure-reporting Kim Morrison 2026-03-04 11:46:12 +00:00
  • 82f6653bca chore: improve CI failure reporting and prompting Kim Morrison 2026-03-04 11:43:23 +00:00
  • d02c50da5f fix: parse LEAN_VERSION_MINOR correctly in release_checklist.py fix-release-checklist-cmake-parse Kim Morrison 2026-03-04 11:28:29 +00:00
  • e8ebee6001 fix: parse LEAN_VERSION_MINOR correctly in release_checklist.py Kim Morrison 2026-03-04 11:28:29 +00:00
  • 0fb289c470 perf: inline a few Array functions (#9661) Henrik Böving 2026-03-04 11:31:58 +01:00
  • 59711e5cff feat: lemmas about String.contains (#12783) Markus Himmel 2026-03-04 10:35:04 +01:00
  • 81deb0a369 test: update expected output for beta-reduced delayed assignments Joachim Breitner 2026-03-04 08:39:12 +00:00
  • bc0324b381 fix: stack-based scope cache for pass 2 fvar substitution Joachim Breitner 2026-03-04 08:07:14 +00:00
  • f0b69dc841 perf: revert to fused pass 2, keep cached resolvability_checker Joachim Breitner 2026-03-04 07:14:25 +00:00
  • d72b0d5d02 test: benchmark all instantiateMVars implementations Joachim Breitner 2026-03-04 06:54:37 +00:00
  • 95583d74bd fix: normalize instance argument in getStuckMVar? for class projections (#12778) v4.29.0-rc4 Leonardo de Moura 2026-03-03 10:31:39 -08:00
  • 209af53427 perf: add high priority to OfSemiring.Q instances Leonardo de Moura 2026-03-03 18:28:16 -08:00
  • f3752861c9 fix: validate stage0 version matches release version (#12700) Kim Morrison 2026-03-04 12:31:29 +11:00
  • 5a69f85194 fix: remove stage0 version validation kimmo/check-stage0-version Kim Morrison 2026-03-04 01:14:54 +00:00
  • d03499322d chore: replace workspace file with .vscode/ settings (#12770) Kim Morrison 2026-03-04 12:10:04 +11:00
  • 66bc9ae177 chore: deprecate levelZero and levelOne (#12720) Kim Morrison 2026-03-04 12:03:08 +11:00
  • 0f7fb1ea4d feat: add ExceptConds.and_elim_left/right (#12760) Kim Morrison 2026-03-04 11:47:30 +11:00
  • 8a52b04fd9 Merge remote-tracking branch 'origin/master' into feat/exceptconds-and-elim feat/exceptconds-and-elim Kim Morrison 2026-03-04 00:03:19 +00:00
  • 93f75deaf3 perf: use replace_fvars in pass 2 to preserve sharing Joachim Breitner 2026-03-03 22:40:36 +00:00
  • f41b9d2e55 perf: inline a few trivial Array functions hbv/inline_array Henrik Böving 2025-08-01 11:26:47 +02:00
  • 4a5773e7f6 perf: compute delayed assignment resolvability via post-pass fixpoint Joachim Breitner 2026-03-03 21:49:25 +00:00
  • 530925c69b chore: fix test suite on macOS (#12780) Garmelon 2026-03-03 21:59:08 +01:00
  • 73640d3758 fix: preserve @[implicit_reducible] for WF-recursive definitions (#12776) Copilot 2026-03-03 18:57:55 +00:00
  • e14f2c8c93 feat: model for string patterns (#12779) Markus Himmel 2026-03-03 19:42:25 +01:00
  • df61abb08f fix: normalize instance argument in getStuckMVar? for class projections (#12778) Leonardo de Moura 2026-03-03 10:31:39 -08:00
  • 71debba5a2 refactor: change agentName field Sofia Rodrigues 2026-03-03 14:24:46 -03:00
  • a2c5f3c79e Merge branch 'sofia/async-http-h1' into sofia/async-http-server Sofia Rodrigues 2026-03-03 14:22:47 -03:00
  • fd9117fc12 fix: server name Sofia Rodrigues 2026-03-03 14:22:39 -03:00
  • b3b669cdd1 fix: whnf defEq_issue Leonardo de Moura 2026-03-03 09:13:44 -08:00
  • 1b6357dc03 Merge branch 'sofia/async-http-h1' into sofia/async-http-server Sofia Rodrigues 2026-03-03 13:59:18 -03:00
  • 38cb50d629 Merge branch 'sofia/async-http-body' into sofia/async-http-h1 Sofia Rodrigues 2026-03-03 13:59:13 -03:00
  • 74af777707 Merge branch 'sofia/async-http-uri' into sofia/async-http-body Sofia Rodrigues 2026-03-03 13:59:07 -03:00
  • 3dfb5e002a Merge branch 'sofia/async-http-headers' into sofia/async-http-uri Sofia Rodrigues 2026-03-03 13:59:01 -03:00
  • 3075e5091b Merge branch 'sofia/async-http-data' into sofia/async-http-headers Sofia Rodrigues 2026-03-03 13:58:55 -03:00
  • af12f7e9be revert: wrong comment Sofia Rodrigues 2026-03-03 13:58:08 -03:00
  • a2f9f74740 refactor: remove h1.0 tests Sofia Rodrigues 2026-03-03 13:57:14 -03:00
  • 13fb8a5980 fix: h1 discovers the port to host match Sofia Rodrigues 2026-03-03 13:56:41 -03:00
  • 41d2984f25 refactor: head -> line Sofia Rodrigues 2026-03-03 13:56:09 -03:00
  • f63639d42b Merge branch 'sofia/async-http-h1' into sofia/async-http-server Sofia Rodrigues 2026-03-03 13:42:13 -03:00
  • 6df74943e0 fix: http and https host port match Sofia Rodrigues 2026-03-03 13:41:30 -03:00
  • dc63bb0b70 feat: lemmas about String.find? and String.contains (#12777) Markus Himmel 2026-03-03 17:30:34 +01:00
  • 865b147a91 fix: http1.0 behavior Sofia Rodrigues 2026-03-03 13:30:28 -03:00
  • 7ca47aad7d feat: add cbv at location syntax (#12773) Wojciech Różowski 2026-03-03 16:12:07 +00:00
  • c2f2b3cf32 fix: refactor changes Sofia Rodrigues 2026-03-03 12:50:31 -03:00
  • c15c7f2d49 Fix instance_reducible not being preserved for WF-recursive definitions copilot/fix-wfrec-instance-reproducible copilot-swe-agent[bot] 2026-03-03 15:48:38 +00:00
  • 4173713f94 Merge branch 'sofia/async-http-body' into sofia/async-http-h1 Sofia Rodrigues 2026-03-03 12:45:10 -03:00
  • 53c9277209 test: rename head to line Sofia Rodrigues 2026-03-03 12:43:44 -03:00
  • 134e10955a Initial plan copilot-swe-agent[bot] 2026-03-03 15:43:08 +00:00
  • f14977f495 Merge branch 'sofia/async-http-uri' into sofia/async-http-body Sofia Rodrigues 2026-03-03 12:42:31 -03:00
  • cfa5cf76fc Merge branch 'sofia/async-http-headers' into sofia/async-http-uri Sofia Rodrigues 2026-03-03 12:42:23 -03:00
  • 238925a681 style: change field names Sofia Rodrigues 2026-03-03 12:38:52 -03:00
  • 8cb236e9eb style: remove parenthesis Sofia Rodrigues 2026-03-03 12:35:29 -03:00
  • 3d039f8dba fix: bugs and code style Sofia Rodrigues 2026-03-03 12:34:12 -03:00
  • 203d5362d4 Merge branch 'sofia/async-http-headers' into sofia/async-http-uri Sofia Rodrigues 2026-03-03 12:12:38 -03:00
  • 6189d4c130 Merge branch 'sofia/async-http-data' into sofia/async-http-headers Sofia Rodrigues 2026-03-03 12:10:31 -03:00
  • 58f14d34d7 chore: improve comments Sofia Rodrigues 2026-03-03 12:10:22 -03:00
  • 710eee2b49 refactor: head to line Sofia Rodrigues 2026-03-03 12:08:26 -03:00
  • bd4af50d04 Merge branch 'sofia/async-http-data' into sofia/async-http-headers Sofia Rodrigues 2026-03-03 12:03:55 -03:00
  • 8cb30347b6 fix: rename head to line Sofia Rodrigues 2026-03-03 12:03:47 -03:00
  • d8e6b09b90 Merge branch 'sofia/async-http-data' into sofia/async-http-headers Sofia Rodrigues 2026-03-03 11:58:30 -03:00
  • df8abc2b3f fix: remove token let tchar Sofia Rodrigues 2026-03-03 11:58:21 -03:00
  • 5a852bdffd Merge branch 'sofia/async-http-data' into sofia/async-http-headers Sofia Rodrigues 2026-03-03 11:57:32 -03:00
  • 11d3860c69 fix: remove char testBit Sofia Rodrigues 2026-03-03 11:57:20 -03:00
  • 5a253001b3 Merge branch 'sofia/async-http-data' into sofia/async-http-headers Sofia Rodrigues 2026-03-03 11:39:12 -03:00
  • 083fec29c8 test: fix Sofia Rodrigues 2026-03-03 11:38:54 -03:00
  • 1f04bf4fd1 feat: add simpDecideCbv simproc for cbv decide (#12766) Wojciech Różowski 2026-03-03 14:24:14 +00:00
  • ff6cd50b8d perf: integrate resolvability tracking into pass 1 traversal cache Joachim Breitner 2026-03-03 13:55:41 +00:00
  • d41753a5f9 fix: suggestions Sofia Rodrigues 2026-03-03 10:11:25 -03:00
  • a086a817e0 feat: v10 Sofia Rodrigues 2026-03-03 09:26:45 -03:00
  • e434a4d44b feat: v10 Sofia Rodrigues 2026-03-03 09:26:27 -03:00
  • 7295389284 Merge branch 'sofia/async-http-h1' into sofia/async-http-server Sofia Rodrigues 2026-03-03 08:34:31 -03:00
  • f8e1bc685a Merge branch 'sofia/async-http-body' into sofia/async-http-h1 Sofia Rodrigues 2026-03-03 08:34:23 -03:00
  • 5e1204e70d fix: test Sofia Rodrigues 2026-03-03 08:34:18 -03:00
  • a00ec10261 Merge branch 'sofia/async-http-h1' into sofia/async-http-server Sofia Rodrigues 2026-03-03 08:31:51 -03:00
  • cb9b182824 Merge branch 'sofia/async-http-body' into sofia/async-http-h1 Sofia Rodrigues 2026-03-03 08:31:44 -03:00
  • 61d7c151da fix: close status for empty Sofia Rodrigues 2026-03-03 08:31:33 -03:00
  • f9f1bdc77b chore: comments Sofia Rodrigues 2026-03-03 08:29:55 -03:00
  • f3452c09a9 Merge branch 'sofia/async-http-h1' into sofia/async-http-server Sofia Rodrigues 2026-03-03 08:26:37 -03:00
  • f0562fac73 Revert pass fusion, has perf issues Joachim Breitner 2026-03-03 11:19:28 +00:00
  • ec4538648b Merge branch 'nightly-with-mathlib' of https://github.com/leanprover/lean4 into joachim/instantiateMVarsNoUpdate Joachim Breitner 2026-03-03 11:18:47 +00:00