Zulip Chat Archive

Stream: lean4 dev

---

Topics:

• 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)
• Indexing lambdas with DiscrTree (68 messages, latest: Nov 26 2023 at 23:20)
• 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: Dec 20 2023 at 11:08 UTC