Zulip Chat Archive
Stream: lean4 dev
Topics:
- Type and universe information kept during compilation (2 messages, latest: Apr 30 2025 at 17:41)
- ✔ Failing to compile Lean (8 messages, latest: Apr 30 2025 at 13:29)
- ✔ Task Termination (19 messages, latest: Apr 29 2025 at 16:39)
- Prevent memory exhaustion (8 messages, latest: Apr 27 2025 at 18:05)
- ✔ casesOn with implemented_by attribute: when? (6 messages, latest: Apr 18 2025 at 18:21)
- linux vs linux_x86/linux_aarch64 (4 messages, latest: Apr 16 2025 at 08:23)
- ✔ Deriving DecidableEq for Lean.Syntax (5 messages, latest: Apr 15 2025 at 16:58)
- ✔ libleanshared.dll.a symbols (3 messages, latest: Apr 06 2025 at 22:16)
- mathlib test build fails (8 instead of 7 heartbeats) (23 messages, latest: Mar 31 2025 at 09:14)
- ✔
lean_environment_find
(7 messages, latest: Mar 30 2025 at 20:12) - lean_io_check_canceled_core (1 message, latest: Mar 18 2025 at 20:36)
- A detail of
kabstract
(1 message, latest: Feb 25 2025 at 02:04) - Misleading error message on type mismatch (92 messages, latest: Feb 23 2025 at 15:58)
- Catching mvars in
MVarId.apply
(3 messages, latest: Feb 13 2025 at 01:58) - LEAN_SMALL_ALLOCATOR (3 messages, latest: Feb 01 2025 at 09:22)
- publications on locally nameless optimizations (6 messages, latest: Jan 20 2025 at 23:17)
- ✔ Typeclass search implementation (4 messages, latest: Jan 17 2025 at 15:57)
- Indexing lambdas with
DiscrTree
(71 messages, latest: Dec 22 2024 at 20:54) - Lean4 Compiler Documentation (1 message, latest: Dec 21 2024 at 02:42)
- Lean4 nix build? (20 messages, latest: Dec 11 2024 at 18:49)
- How best to determine if an Expr has loose bvars? (6 messages, latest: Dec 09 2024 at 15:07)
- Upstreaming
ToExpr
derive handler (12 messages, latest: Nov 04 2024 at 07:34) - Lean 4 hanging - unsure how to debug (17 messages, latest: Nov 01 2024 at 02:27)
- ✔ lean-toolchain (3 messages, latest: Oct 24 2024 at 23:17)
- Type mismatch after moving instNatCast to Lean (173 messages, latest: Oct 18 2024 at 20:38)
- Code generator/compiler/memory allocator docs? (41 messages, latest: Oct 03 2024 at 23:37)
- Regarding the API for IO.FS.Handle (4 messages, latest: Oct 01 2024 at 13:36)
- Broken commit convention link (4 messages, latest: Sep 27 2024 at 22:25)
- Conversion from String to ByteArray (26 messages, latest: Sep 18 2024 at 00:09)
- Bug: 'unterminated comment' when you have
/-
in a docstrin (1 message, latest: Aug 12 2024 at 18:04) - Lake dependency graph command similar to
cargo tree
(10 messages, latest: Aug 09 2024 at 13:06) - Build failure on macOS with Nix (13 messages, latest: Jul 01 2024 at 02:18)
- API rate limit exceeded for user ID 129911861 (6 messages, latest: Jun 20 2024 at 14:13)
- Resolve import dependencies into a flat file (3 messages, latest: Jun 13 2024 at 07:40)
- doc-gen4 post 4.8.0-rc1 (3 messages, latest: May 28 2024 at 14:53)
- simp to keep showing the goal state as you type theorems (3 messages, latest: May 15 2024 at 21:09)
- ✔ tag naming schema impact on lean4checker in lean-action (5 messages, latest: May 09 2024 at 00:42)
- Find references broken in lean core (16 messages, latest: May 05 2024 at 06:09)
- ✔ Meaning of "batteries" (4 messages, latest: May 03 2024 at 11:06)
- Document ordering of constructor fields in ffi.md (3 messages, latest: Apr 30 2024 at 23:33)
- ✔ Issue to expand docs of
Init.Data.List.BasicAux
(6 messages, latest: Apr 14 2024 at 17:21) - ✔ Lean.HashMap vs Std.HashMap and similar cases (5 messages, latest: Apr 11 2024 at 23:44)
- Correctly Changing Lean.Compiler.IR Data Structures (9 messages, latest: Apr 05 2024 at 13:27)
- Generalizing over
MetaM
(5 messages, latest: Mar 25 2024 at 19:27) - Initial numerals in import paths (2 messages, latest: Mar 14 2024 at 21:48)
- multiple input pipes (8 messages, latest: Mar 11 2024 at 04:04)
- go to definition jumps to incorrect file (23 messages, latest: Mar 08 2024 at 08:29)
- General Suggestion for Better Error Message (8 messages, latest: Mar 07 2024 at 09:56)
- Protect LD_LIBRARY_PATH environment variable for leanc (6 messages, latest: Feb 26 2024 at 22:01)
- kabstract that works under binders (1 message, latest: Jan 26 2024 at 11:26)
- IntN Lean representation? (25 messages, latest: Jan 16 2024 at 04:24)
- unnecessary
getFunInfoNArgs
inDiscrTree
(30 messages, latest: Jan 05 2024 at 16:36) - Lean 4 Parser (3 messages, latest: Dec 19 2023 at 18:46)
- [RFC] Int.div convention (86 messages, latest: Dec 01 2023 at 03:12)
- actions/setup-lean (1 message, latest: Nov 25 2023 at 01:16)
- stage0 lean uses oleans from stage1 (44 messages, latest: Nov 19 2023 at 08:31)
- Syntax quotation for a tuple (10 messages, latest: Nov 17 2023 at 20:00)
- ElabTermM and saveState (9 messages, latest: Nov 10 2023 at 16:16)
- Adding tests (6 messages, latest: Nov 03 2023 at 16:31)
- Elan override and VSCode extension (10 messages, latest: Nov 03 2023 at 11:05)
- RFC: Extensible pre-definition-compilers (1 message, latest: Nov 03 2023 at 10:18)
- Nix CI job broken (2 messages, latest: Oct 19 2023 at 12:41)
- Imports and jump-to-def in lean4 repo (VS code) (2 messages, latest: Oct 15 2023 at 23:20)
- Compiling runtime to LLVM bitcode? (13 messages, latest: Oct 13 2023 at 20:45)
- Bootstrapping issue? (24 messages, latest: Oct 10 2023 at 18:52)
- ✔ LSP tests? (6 messages, latest: Oct 10 2023 at 13:07)
- What's in a sanitized
Name
? (2 messages, latest: Oct 10 2023 at 06:35) - Elaboration of swift notation (1 message, latest: Oct 06 2023 at 16:26)
- More compact DiscrTree (60 messages, latest: Sep 25 2023 at 20:24)
- lean4 PR conventions (15 messages, latest: Sep 21 2023 at 20:36)
- make test for specific tests (6 messages, latest: Sep 21 2023 at 08:32)
- vscode (1 message, latest: Sep 20 2023 at 20:23)
- Unused PrefixTrie and NameTrie (3 messages, latest: Sep 18 2023 at 21:10)
- Confusing build failure sometimes in stage1 (16 messages, latest: Sep 14 2023 at 10:18)
- [Compiler] LLVM Backend (212 messages, latest: Sep 14 2023 at 05:30)
- Implementing independent kernel (8 messages, latest: Sep 08 2023 at 19:50)
- A test suite for new backends (1 message, latest: Aug 22 2023 at 16:23)
- update-stage0 (3 messages, latest: Aug 14 2023 at 07:37)
- How to infer type post-
runFrontend
(1 message, latest: Jul 25 2023 at 09:43) - master currently failing (4 messages, latest: May 31 2023 at 01:47)
- bumping up LLVM 15 -> 16? (2 messages, latest: May 03 2023 at 08:13)
- Vulnerabilities (15 messages, latest: Apr 16 2023 at 22:43)
- RFC: MonadFail (5 messages, latest: Apr 16 2023 at 10:07)
- Syntax extensions from within the compiler (6 messages, latest: Apr 09 2023 at 06:34)
- RFC: Lazy code generation (30 messages, latest: Apr 02 2023 at 14:01)
- Build setup under elan proposal (27 messages, latest: Mar 23 2023 at 17:06)
- FYI CI now merges master (5 messages, latest: Feb 25 2023 at 09:27)
- Parser in another category breaks antiquotations (4 messages, latest: Feb 21 2023 at 12:39)
- [Frontend] meeting notes (24 messages, latest: Feb 04 2023 at 15:49)
- isDefEq on structures (6 messages, latest: Jan 30 2023 at 09:40)
- resuming synthesis (2 messages, latest: Jan 30 2023 at 08:04)
- Windows build is broken (1 message, latest: Jan 27 2023 at 19:11)
- Platform distribution (5 messages, latest: Jan 27 2023 at 18:58)
- RFC: Use unsigned ints for
FVarId
etc. (11 messages, latest: Jan 26 2023 at 10:34) - isDefEq on projections (8 messages, latest: Jan 20 2023 at 19:26)
- synthInstances & universe metavariables (1 message, latest: Jan 20 2023 at 16:10)
- Should instance names inherit macro scopes? (5 messages, latest: Jan 18 2023 at 09:10)
- [Compiler] meeting notes (88 messages, latest: Jan 18 2023 at 04:44)
- Mathlib profiling (9 messages, latest: Jan 11 2023 at 10:26)
- GH project list (1 message, latest: Jan 11 2023 at 01:18)
- Lean LLVM/MLIR (37 messages, latest: Jan 04 2023 at 21:07)
- [Compiler]
compile #\[
Lean.AssocList.contains\]
(22 messages, latest: Dec 28 2022 at 21:38) - Data.List.Basic is a server stress test (6 messages, latest: Dec 20 2022 at 19:54)
- [Compiler]
compile #\[
Heq.noConfusionType\]
(4 messages, latest: Dec 14 2022 at 07:34) - [Compiler] next meeting (3 messages, latest: Dec 14 2022 at 01:39)
- [Compiler] Partially applied constructors? (2 messages, latest: Dec 08 2022 at 20:21)
- [Compiler] escape analysis … (14 messages, latest: Dec 07 2022 at 20:48)
- Beginner Questions (15 messages, latest: Dec 07 2022 at 11:24)
- [Compiler] LCNF for Array.get (12 messages, latest: Dec 01 2022 at 18:17)
- Top-level task (5 messages, latest: Nov 29 2022 at 19:28)
- [Compiler] moving meeting to Wednesday (1 message, latest: Nov 26 2022 at 15:45)
- [Compiler] lean-souffle (Datalog) (18 messages, latest: Nov 24 2022 at 13:23)
?a
name hygiene issues (6 messages, latest: Nov 18 2022 at 12:38)- General contribution question: adding basic utilities (6 messages, latest: Nov 11 2022 at 03:38)
- [Compiler] Meeting link (4 messages, latest: Nov 07 2022 at 18:02)
- ✔ [Compiler] adding sharing automatically (2 messages, latest: Oct 29 2022 at 01:07)
- [Compiler] adding sharing automatically (4 messages, latest: Oct 28 2022 at 22:54)
- [Compiler] Friday meetings (1 message, latest: Oct 19 2022 at 13:58)
- Potential mathlib scalability issues (5 messages, latest: Oct 15 2022 at 14:52)
- [Compiler] Probe library (1 message, latest: Oct 15 2022 at 03:55)
- Running benchmarks interactively? (9 messages, latest: Oct 14 2022 at 07:39)
- [Compiler] Recursive join points (7 messages, latest: Oct 11 2022 at 08:35)
- ✔ LCNF Code size (4 messages, latest: Oct 10 2022 at 19:41)
- Weak symbols (141 messages, latest: Oct 08 2022 at 08:25)
- Building on Mac (9 messages, latest: Oct 06 2022 at 18:10)
- [Compiler] second phase (aka mono) (3 messages, latest: Oct 06 2022 at 16:28)
- Development setup (4 messages, latest: Oct 04 2022 at 23:58)
- Available options for compiler and tracing output (11 messages, latest: Oct 02 2022 at 23:30)
- [Compiler] new compiler first phase is active (46 messages, latest: Sep 30 2022 at 15:48)
- [Compiler] inline + let (41 messages, latest: Sep 30 2022 at 00:56)
- Unresolved symbols (2 messages, latest: Sep 26 2022 at 07:44)
- [Compiler] specialization reuse (9 messages, latest: Sep 24 2022 at 22:57)
- [Compiler] Environment after elaboration … (8 messages, latest: Sep 23 2022 at 15:00)
- try_for (2 messages, latest: Sep 23 2022 at 09:36)
- [Compiler] meeting dates & link (1 message, latest: Sep 22 2022 at 17:59)
- [Compiler] first meeting notes (44 messages, latest: Sep 19 2022 at 20:10)
- Multiply delayed assignments? (16 messages, latest: Sep 18 2022 at 13:58)
- [Compiler] constant propagation (3 messages, latest: Sep 18 2022 at 13:24)
- [RFC] Syntax of documentation comments for constructors (7 messages, latest: Sep 16 2022 at 18:34)
- [Compiler] OCaml Flambda (3 messages, latest: Sep 14 2022 at 22:41)
- ✔ Compilation errors in simpleTypes.lean (1 message, latest: Sep 13 2022 at 14:38)
- Compilation errors in simpleTypes.lean (5 messages, latest: Sep 13 2022 at 14:21)
- Panics in syntax accessors (5 messages, latest: Sep 13 2022 at 11:24)
- ✔ nix help building docs (1 message, latest: Sep 10 2022 at 00:17)
- nix help building docs (5 messages, latest: Sep 06 2022 at 21:43)
- conv zoom button (21 messages, latest: Sep 06 2022 at 16:20)
- stream events (1 message, latest: Sep 01 2022 at 20:44)
Last updated: May 02 2025 at 03:31 UTC