Zulip Chat Archive

Stream: lean4 dev

Topics:

Lean4 build fails on Linux x86-64 (5 messages, latest: Feb 26 2026 at 22:13)
Lean-TUI (self-contained infoview) (1 message, latest: Jan 25 2026 at 19:41)
Add -headerpad to linker args (2 messages, latest: Dec 11 2025 at 21:54)
Where to put tests related to Lake (2 messages, latest: Dec 07 2025 at 01:19)
Unboxed structure types (18 messages, latest: Nov 30 2025 at 00:48)
Building shared dynamic libraries with dependencies (1 message, latest: Nov 30 2025 at 00:41)
PDF, single HTML, and LaTeX versions of learning materials (3 messages, latest: Oct 14 2025 at 09:16)
stage0 builds twice on windows (29 messages, latest: Sep 30 2025 at 01:24)
supported OS/architectures (3 messages, latest: Sep 29 2025 at 22:18)
Adjusting error ranges for by, etc (RFC #8919) (2 messages, latest: Sep 15 2025 at 11:54)
Algebraic effects in Lean (30 messages, latest: Aug 25 2025 at 14:45)
The Nix CI is broken for Lean v4.22.0 (9 messages, latest: Aug 15 2025 at 16:32)
Can't build lean due to old libuv (14 messages, latest: Jul 31 2025 at 17:46)
Can diagnostics be more resilient to unfinished proofs? (97 messages, latest: Jul 31 2025 at 12:22)
'leaning tower of macros' slides link broken (2 messages, latest: Jul 29 2025 at 23:46)
Documentation of Array runtime Behaviour (6 messages, latest: Jul 26 2025 at 13:28)
Can autocomplete suggestions LSP be smarter? (4 messages, latest: Jul 23 2025 at 13:42)
✔ Allocating external data (4 messages, latest: Jul 16 2025 at 15:22)
Efficient dev flow for parser work (3 messages, latest: Jul 05 2025 at 20:09)
Proposal: Customizable runtime representations (17 messages, latest: Jul 03 2025 at 03:02)
Set of all auxiliary lemmas (2 messages, latest: Jul 02 2025 at 23:00)
Unsafe prohibition flag in Elab.Term.Context (19 messages, latest: Jul 02 2025 at 17:13)
Understanding meta import (6 messages, latest: Jun 24 2025 at 22:34)
Core.transform vs Expr.replace usage in new codegen (15 messages, latest: Jun 16 2025 at 08:46)
How to check local changes? (8 messages, latest: Jun 14 2025 at 19:32)
✔ casesOn with implemented_by attribute: when? (7 messages, latest: Jun 13 2025 at 20:33)
✔ Translation of Nat to arbitrary-precision integers (3 messages, latest: Jun 04 2025 at 07:54)
✔ Type and universe information kept during compilation (1 message, latest: Jun 03 2025 at 13:25)
segmentation fault at Lean/Elab/Tactic/Try (3 messages, latest: Jun 03 2025 at 11:25)
Feature suggestion: Nonempty for thunks (4 messages, latest: May 15 2025 at 05:30)
Should try/catch be whitespace-sensitive? (2 messages, latest: May 11 2025 at 12:41)
How to build releases from tags in my fork (7 messages, latest: May 10 2025 at 18:29)
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)
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 ofInit.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 in DiscrTree (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: Feb 28 2026 at 14:05 UTC