max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

Commit graph

  • e2f9df6578 chore: update stage0 Lean stage0 autoupdater 2026-04-20 22:03:37 +00:00
  • a3cb98bb27
         fix: aggregate ControlInfo past numRegularExits == 0 elements (#13486) Sebastian Graf 2026-04-20 23:13:59 +02:00
  • a0b2e1f302
         feat: introduce HTTP/1.1 server (#12151) Sofia Rodrigues 2026-04-20 13:25:45 -03:00
  • 10338ed1b0
         fix: wrapInstance: do not leak via un-reducible instances (#13441) Sebastian Ullrich 2026-04-20 08:41:32 +02:00
  • cc9a217df8 chore: update stage0 Lean stage0 autoupdater 2026-04-19 21:43:33 +00:00
  • 81f559b0e4
         chore: remove repeat/while macro_rules bootstrap from Init.While (#13479) Sebastian Graf 2026-04-19 23:01:14 +02:00
  • 7cc3a4cc0b
         perf: use .local asyncMode for eqnOptionsExt (#13477) Joachim Breitner 2026-04-19 16:49:00 +02:00
  • e82cd9b62c
         fix: filter assigned metavariables before computing apply subgoal tags (#13476) Leonardo de Moura 2026-04-19 16:31:49 +02:00
  • 1d2cfb47e7
         feat: store eqn-affecting options at definition time instead of eager generation (#13475) Joachim Breitner 2026-04-19 14:30:08 +02:00
  • 439e6a85d3
         fix: prune goals assigned by isDefEq in sym => mode (#13474) Leonardo de Moura 2026-04-19 13:55:11 +02:00
  • 2d38a70d1c
         fix: auto-introduce in sym => mode when goal closes during preprocessing (#13472) Leonardo de Moura 2026-04-19 10:32:49 +02:00
  • 80cbab1642
         chore: don't fail on running build bench on built stage3 (#13467) Sebastian Ullrich 2026-04-19 00:07:21 +02:00
  • c0a53ffe97
         chore: minor tweaks to Sym.simp test and benchmark (#13468) Leonardo de Moura 2026-04-18 23:11:30 +02:00
  • 91aa82da7f chore: update stage0 Lean stage0 autoupdater 2026-04-18 11:10:08 +00:00
  • 3e9ed3c29d
         chore: add AGENTS.md symlink to CLAUDE.md (#13461) Kim Morrison 2026-04-18 16:48:05 +10:00
  • 43e1e8285b
         refactor: lake: introduce GitRev (#13456) Mac Malone 2026-04-17 23:44:26 -04:00
  • d3c069593b
         refactor: introduce Package.depPkgs (#13445) Mac Malone 2026-04-17 23:44:21 -04:00
  • 0fa749f71b
         refactor: lake: introduce lowerHexUInt64 (#13455) Mac Malone 2026-04-17 23:43:11 -04:00
  • 592eb02bb2
         feat: have level metavariable pretty printer instantiate level metavariables (#13438) Kyle Miller 2026-04-17 18:07:22 -07:00
  • 70df9742f4
         fix: kernel error in grind order module for Nat casts to non-Int types (#13453) Leonardo de Moura 2026-04-18 01:51:21 +02:00
  • 9c245d5531
         test: add regression test for Sym.simp eta-reduction (#13416) (#13452) Leonardo de Moura 2026-04-18 00:47:53 +02:00
  • 3c4440d3bc
         feat: lake: JobAction.reuse & .unpack (#13423) Mac Malone 2026-04-17 18:34:04 -04:00
  • 2964193af8
         fix: avoid assigning mvar when Sym.intros produces no binders (#13451) Leonardo de Moura 2026-04-17 23:47:47 +02:00
  • 43e96b119d
         fix: prevent a hang in acLt (#13367) Eric Wieser 2026-04-17 14:46:29 -07:00
  • 615f45ad7a
         chore: fix Sym benchmarks using stale run' API (#13450) Leonardo de Moura 2026-04-17 23:31:57 +02:00
  • 8a9a5ebd5e
         refactor: promote repeat/while builtin parsers to default priority (#13447) Sebastian Graf 2026-04-17 22:57:41 +02:00
  • 1af697a44b
         fix: eta-reduce patterns containing loose pattern variables (#13448) Leonardo de Moura 2026-04-17 22:49:21 +02:00
  • 234267b08a chore: update stage0 Lean stage0 autoupdater 2026-04-17 16:13:04 +00:00
  • 704df340cb
         feat: make repeat and while syntax builtin (#13442) Sebastian Graf 2026-04-17 17:19:59 +02:00
  • f180c9ce17
         fix: handling of EmitC for small hex string literals (#13435) Henrik Böving 2026-04-17 17:16:28 +02:00
  • 040376ebd0 chore: update stage0 Lean stage0 autoupdater 2026-04-17 10:09:17 +00:00
  • ce998700e6
         feat: add ControlInfo handler for doRepeat (#13437) Sebastian Graf 2026-04-17 11:17:52 +02:00
  • b09d39a766
         chore: build bench: replace warmup with selective build (#13432) Sebastian Ullrich 2026-04-17 10:01:17 +02:00
  • 348ed9b3b0 chore: update stage0 Lean stage0 autoupdater 2026-04-17 08:05:59 +00:00
  • f8b9610b74
         feat: add Lean.doRepeat elaborators for repeat/while loops (#13434) Sebastian Graf 2026-04-17 09:17:57 +02:00
  • 3fc99eef10
         feat: add instance validation checks in addInstance (#13389) Wojciech Różowski 2026-04-16 18:48:16 +01:00
  • b99356ebcf
         chore: enable warning.simp.varHead (#13403) Wojciech Różowski 2026-04-16 17:11:09 +01:00
  • 7e8a710ca3
         fix: two bugs in io.cpp (#13427) Henrik Böving 2026-04-16 14:38:17 +02:00
  • 621c558c13
         fix: make delta-derived instances respect enclosing meta sections (#13315) Kim Morrison 2026-04-16 19:18:54 +10:00
  • 490c79502b
         fix: improve result type mismatch errors and locations in new do elaborator (#13404) Sebastian Graf 2026-04-16 11:16:27 +02:00
  • fed2f32651
         chore: revert "feat: add lake builtin-lint (#13422) Wojciech Różowski 2026-04-15 20:28:59 +01:00
  • 5949ae8664
         fix: expand reset reuse in the presence of double oproj (#13421) Henrik Böving 2026-04-15 21:16:22 +02:00
  • fe77e4d2d1
         fix: coinductive syntax causing panic in macro scopes (#13420) Wojciech Różowski 2026-04-15 19:50:31 +01:00
  • 9b1426fd9c
         feat: add lake builtin-lint (#13393) Wojciech Różowski 2026-04-15 19:14:40 +01:00
  • b6bfe019a1 chore: update stage0 Lean stage0 autoupdater 2026-04-15 10:55:52 +00:00
  • 748783a5ac
         feat: add internal skip do-element parser (#13413) Sebastian Graf 2026-04-15 12:01:01 +02:00
  • df23b79c90
         fix: tactic completion in empty by blocks (#13348) Marc Huisinga 2026-04-15 10:39:55 +02:00
  • 8156373037
         fix: pass CMake Lake args to the Lake make build (#13410) Mac Malone 2026-04-14 18:07:29 -04:00
  • 75487a1bf8
         fix: universe normalization in getDecLevel (#13391) Sebastian Graf 2026-04-14 23:27:22 +02:00
  • 559f6c0ae7
         perf: specialize qsort properly onto the lt function (#13409) Henrik Böving 2026-04-14 21:57:30 +02:00
  • a0ee357152
         chore: add io compute benchmark (#13406) Henrik Böving 2026-04-14 20:33:32 +02:00
  • 1884c3b2ed
         feat: make mimalloc security options available (#13401) Henrik Böving 2026-04-14 15:22:07 +02:00
  • cdb6401c65
         chore: don't waste time building CMake mimalloc that we don't use (#13402) Sebastian Ullrich 2026-04-14 11:49:31 +02:00
  • d6b938d6c2
         fix: correct name for String.Pos.le_skipWhile (#13400) Julia Markus Himmel 2026-04-14 08:51:38 +02:00
  • eee2909c9d
         fix: deriving Inhabited for structures should inherit Inhabited instances (#13395) Kyle Miller 2026-04-13 19:46:07 -07:00
  • 106b39d278
         fix: remove private from private section (#13398) Sofia Rodrigues 2026-04-13 17:47:58 -03:00
  • cf53db3b13
         fix: add term info for for loop variables in new do elaborator (#13399) Sebastian Graf 2026-04-13 22:29:55 +02:00
  • a0f2a8bf60
         fix: improve error for join point assignment failure in do elaborator (#13397) Sebastian Graf 2026-04-13 21:32:43 +02:00
  • cbda692e7e
         fix: free variable in do bind when continuation type depends on bvar (#13396) Sebastian Graf 2026-04-13 20:51:45 +02:00
  • 4dced0287e chore: update stage0 Lean stage0 autoupdater 2026-04-13 19:08:51 +00:00
  • c4d9573342
         feat: warn when simp theorem LHS has variable or unrecognized head symbol (#13325) Wojciech Różowski 2026-04-13 20:11:06 +02:00
  • 9db52c7fa6
         fix: file read buffer overflow (#13392) Henrik Böving 2026-04-13 19:56:27 +02:00
  • ea209d19e0
         chore: enable pipefail in test and bench suite (#13124) Garmelon 2026-04-13 19:54:47 +02:00
  • f0c999a668
         feat: introduce HTTP/1.1 protocol state machine (#12146) Sofia Rodrigues 2026-04-13 14:41:19 -03:00
  • c769515d94
         refactor: use Nat.decEq in derived BEq instances (#13390) Joachim Breitner 2026-04-13 17:24:04 +02:00
  • 1b81a9889b chore: update stage0 Lean stage0 autoupdater 2026-04-13 14:07:41 +00:00
  • 1c9e26420f
         feat: upstream environment linters to core lean (#13356) Wojciech Różowski 2026-04-13 15:13:15 +02:00
  • cd697eac81
         chore: remove module build instructions from CLAUDE.md (#13386) Sebastian Ullrich 2026-04-13 12:08:33 +02:00
  • c54f691f4a
         fix: end_local_scope does not work with compound namespace names (#13360) Wojciech Różowski 2026-04-13 12:05:26 +02:00
  • 0d7e76ea88
         fix: include ignoreNoncomputable in LCNF cache key (#13384) Sebastian Ullrich 2026-04-13 11:27:25 +02:00
  • 2b8c273687
         feat: add linter.redundantVisibility for redundant private/public modifiers (#13132) Sebastian Ullrich 2026-04-13 10:34:20 +02:00
  • ff19ad9c38
         fix: keep wrapInstance mvar-free (#13346) Sebastian Ullrich 2026-04-13 10:11:10 +02:00
  • d76e5a1886
         chore: cache-get Make target (#13341) Sebastian Ullrich 2026-04-12 19:37:52 +02:00
  • 86579c8e24
         fix: generate SizeOf spec theorems for inductives with private constructors (#13374) Joachim Breitner 2026-04-12 14:00:51 +02:00
  • 41ab492142
         chore: CI: ignore compile_bench/channel in Linux Reldebug Sebastian Ullrich 2026-04-11 13:16:12 +02:00
  • 790d294e50
         fix: use commondir to resolve git directory in worktrees (#13045) Kim Morrison 2026-04-11 16:45:02 +10:00
  • d53b46a0f3 chore: update stage0 Sebastian Ullrich 2026-04-10 12:30:49 +00:00
  • 5a9d3bc991 chore: update stage0 Sebastian Ullrich 2026-04-10 12:26:25 +00:00
  • 8678c99b76 fix: respect module visibility in initialize/builtin_initialize Sebastian Ullrich 2026-03-30 15:47:59 +00:00
  • bc2da2dc74
         perf: assorted compiler annotations (#13357) Henrik Böving 2026-04-10 13:47:40 +02:00
  • e0a29f43d2
         feat: adjust deriving Inhabited to use structure field defaults (#9815) Kyle Miller 2026-04-09 11:54:24 -07:00
  • a07649a4c6
         feat: add warning for non-portable module names (#13318) Wojciech Różowski 2026-04-09 18:16:51 +02:00
  • 031bfa5989
         fix: handle flattened inheritance in wrapInstance (#13302) Sebastian Ullrich 2026-04-09 17:53:21 +02:00
  • 1d1c5c6e30 chore: update stage0 Lean stage0 autoupdater 2026-04-09 15:26:42 +00:00
  • c0fbddbf6f
         chore: scale nat_repr to a more reasonable runtime (#13347) Sebastian Ullrich 2026-04-09 15:54:56 +02:00
  • c60f97a3fa
         feat: allow field notation to use explicit universe levels (#13262) Kyle Miller 2026-04-09 06:29:10 -07:00
  • 82bb27fd7d
         fix: lake: report bad imports from a library build (#13340) Mac Malone 2026-04-09 00:03:52 -04:00
  • ab0ec9ef95
         chore: use weakLeanArgs for Lake plugin (#13335) Mac Malone 2026-04-08 20:02:39 -04:00
  • f9b2f6b597
         fix: use getDecLevel/isLevelDefEq for for loop mut var universe constraints (#13332) Sebastian Graf 2026-04-08 18:34:51 +02:00
  • a3cc301de5
         fix: wrapInstance should not reduce non-constructor instances (#13327) Sebastian Ullrich 2026-04-08 18:31:28 +02:00
  • 3a8db01ce8 chore: update stage0 Lean stage0 autoupdater 2026-04-08 15:28:03 +00:00
  • 06fb4bec52
         feat: require indentation in commands, allow empty tactic sequences (#13229) Joachim Breitner 2026-04-08 16:05:47 +02:00
  • 35b4c7dbfc
         feat: implicit public meta import Init in non-prelude files (#13323) Sebastian Ullrich 2026-04-08 13:46:46 +02:00
  • 2398d2cc66
         feat: no [defeq] attribute on sizeOf_spec lemmas (#13320) Joachim Breitner 2026-04-08 13:10:50 +02:00
  • 8353964e55
         feat: wire PowIdentity into grind ring solver (#13088) Kim Morrison 2026-04-08 20:14:10 +10:00
  • 334d9bd4f3
         feat: add markMeta parameter to addAndCompile (#13311) Kim Morrison 2026-04-08 19:09:01 +10:00
  • f7f5fc5ecd
         feat: add PowIdentity typeclass for grind ring solver (#13086) Kim Morrison 2026-04-08 19:05:12 +10:00
  • 659db85510
         fix: suggest (rfl) not id rfl in linter (#13319) Joachim Breitner 2026-04-08 10:21:23 +02:00
  • 91dd99165a
         feat: add warning when applying global attribute using in (#13223) Wojciech Różowski 2026-04-08 07:20:34 +01:00
  • e44351add9 chore: update stage0 Lean stage0 autoupdater 2026-04-08 05:43:47 +00:00