/ toolchains / lean.bzl
lean.bzl
1 # lean.bzl 2 # Lean 4 compilation rules for Buck2 with Nix toolchain integration 3 # 4 # Lean 4 compiles to C, which we then compile with our C++ toolchain. 5 # This enables proof-carrying code: Lean theorems constrain generated C, 6 # which links into Rust/Haskell/Python via FFI. 7 # 8 # Key features: 9 # - lean_library: Build a Lean library (.olean files + C extraction) 10 # - lean_binary: Build a Lean executable 11 # - lean_c_library: Extract C code from Lean for FFI linking 12 # 13 # Configuration (in .buckconfig): 14 # [lean] 15 # lean = /path/to/lean # Lean compiler 16 # leanc = /path/to/leanc # Lean C compiler wrapper 17 # lean_lib_dir = /path/to/lib # Lean standard library 18 # lean_include_dir = /path/to/include # Lean C headers 19 # 20 # Usage: 21 # lean_library( 22 # name = "proofs", 23 # srcs = ["VillaStraylight.lean"], 24 # deps = ["//lib:mathlib"], 25 # ) 26 # 27 # lean_c_library( 28 # name = "verified_kernel", 29 # srcs = ["Kernel.lean"], 30 # deps = [":proofs"], 31 # # Extracted C code can be linked into cxx_library 32 # ) 33 # 34 # The proof-carrying pattern: 35 # 1. Write theorems in Lean (compile-time verification) 36 # 2. Extract to C via lean_c_library 37 # 3. Link C into Rust/C++ via FFI 38 # 4. Fuzz at runtime against Lean specs (omega tactic IRL) 39 40 # ═══════════════════════════════════════════════════════════════════════════════ 41 # PROVIDERS 42 # ═══════════════════════════════════════════════════════════════════════════════ 43 44 LeanLibraryInfo = provider(fields = { 45 "olean_dir": provider_field(Artifact | None, default = None), 46 "c_dir": provider_field(Artifact | None, default = None), 47 "lib_name": provider_field(str, default = ""), 48 "deps": provider_field(list, default = []), 49 }) 50 51 LeanCLibraryInfo = provider(fields = { 52 "c_sources": provider_field(list[Artifact], default = []), 53 "include_dir": provider_field(Artifact | None, default = None), 54 "objects": provider_field(list[Artifact], default = []), 55 "archive": provider_field(Artifact | None, default = None), 56 }) 57 58 # ═══════════════════════════════════════════════════════════════════════════════ 59 # CONFIGURATION 60 # ═══════════════════════════════════════════════════════════════════════════════ 61 62 def _get_lean() -> str: 63 """Get lean compiler path from config.""" 64 path = read_root_config("lean", "lean", None) 65 if path == None: 66 fail(""" 67 lean compiler not configured. 68 69 Configure your toolchain via Nix: 70 71 [lean] 72 lean = /nix/store/.../bin/lean 73 leanc = /nix/store/.../bin/leanc 74 lean_lib_dir = /nix/store/.../lib/lean 75 lean_include_dir = /nix/store/.../include 76 77 Then run: nix develop 78 """) 79 return path 80 81 def _get_leanc() -> str: 82 """Get leanc (Lean C compiler wrapper) path from config.""" 83 path = read_root_config("lean", "leanc", None) 84 if path == None: 85 fail("leanc not configured. See [lean] section in .buckconfig") 86 return path 87 88 def _get_lean_lib_dir() -> str | None: 89 """Get Lean standard library directory.""" 90 return read_root_config("lean", "lean_lib_dir", None) 91 92 def _get_lean_include_dir() -> str | None: 93 """Get Lean C headers directory.""" 94 return read_root_config("lean", "lean_include_dir", None) 95 96 # ═══════════════════════════════════════════════════════════════════════════════ 97 # LEAN LIBRARY RULE 98 # ═══════════════════════════════════════════════════════════════════════════════ 99 100 def _lean_library_impl(ctx: AnalysisContext) -> list[Provider]: 101 """ 102 Build a Lean library. 103 104 Compiles Lean source files to .olean (compiled interface) files. 105 Optionally extracts C code for FFI. 106 107 Lean compilation model: 108 - Each .lean file compiles to .olean (binary interface) 109 - Dependencies must be compiled first (no circular deps) 110 - C extraction happens via --c flag 111 """ 112 lean = _get_lean() 113 lean_lib_dir = _get_lean_lib_dir() 114 115 if not ctx.attrs.srcs: 116 return [DefaultInfo(), LeanLibraryInfo()] 117 118 # Output directories 119 olean_dir = ctx.actions.declare_output("olean", dir = True) 120 c_dir = ctx.actions.declare_output("c", dir = True) if ctx.attrs.extract_c else None 121 122 # Collect dependency olean directories 123 dep_paths = [] 124 for dep in ctx.attrs.deps: 125 if LeanLibraryInfo in dep: 126 info = dep[LeanLibraryInfo] 127 if info.olean_dir: 128 dep_paths.append(info.olean_dir) 129 130 # Build script 131 script_parts = ["set -e"] 132 script_parts.append("mkdir -p $OLEAN_DIR") 133 if c_dir: 134 script_parts.append("mkdir -p $C_DIR") 135 136 # Build LEAN_PATH from dependencies and stdlib 137 lean_path_parts = ["$OLEAN_DIR"] 138 if lean_lib_dir: 139 lean_path_parts.append(lean_lib_dir) 140 for dep_path in dep_paths: 141 lean_path_parts.append(cmd_args(dep_path)) 142 143 script_parts.append(cmd_args( 144 "export LEAN_PATH=", 145 cmd_args(lean_path_parts, delimiter = ":"), 146 delimiter = "", 147 )) 148 149 # Compile each source file 150 # Lean requires sources to be in --root directory, so we copy to scratch 151 for src in ctx.attrs.srcs: 152 # Module name from filename (Foo/Bar.lean -> Foo.Bar) 153 # Simplified: just use basename without extension for now 154 module_name = src.basename.removesuffix(".lean") 155 156 # Copy source to scratch dir (Lean's --root requirement) 157 script_parts.append(cmd_args("cp", src, "$BUCK_SCRATCH_PATH/", delimiter = " ")) 158 159 compile_cmd = [lean, "--root=$BUCK_SCRATCH_PATH"] 160 compile_cmd.extend(ctx.attrs.lean_flags) 161 compile_cmd.extend(["-o", cmd_args("$OLEAN_DIR/", module_name, ".olean", delimiter = "")]) 162 163 if c_dir: 164 compile_cmd.append(cmd_args("--c=$C_DIR/", module_name, ".c", delimiter = "")) 165 166 compile_cmd.append("$BUCK_SCRATCH_PATH/{}".format(src.basename)) 167 168 script_parts.append(cmd_args(compile_cmd, delimiter = " ")) 169 170 # Assemble full command 171 script = cmd_args(script_parts, delimiter = "\n") 172 173 outputs = [olean_dir.as_output()] 174 env_parts = ["OLEAN_DIR=", olean_dir.as_output()] 175 176 if c_dir: 177 outputs.append(c_dir.as_output()) 178 env_parts.extend([" C_DIR=", c_dir.as_output()]) 179 180 cmd = cmd_args( 181 "/bin/sh", "-c", 182 cmd_args(env_parts, " && ", script, delimiter = ""), 183 ) 184 185 # Hidden inputs for dependency tracking 186 hidden = list(ctx.attrs.srcs) 187 for dep_path in dep_paths: 188 hidden.append(dep_path) 189 190 ctx.actions.run( 191 cmd_args(cmd, hidden = hidden), 192 category = "lean_compile", 193 identifier = ctx.attrs.name, 194 local_only = True, # Lean compilation needs consistent LEAN_PATH 195 ) 196 197 return [ 198 DefaultInfo( 199 default_output = olean_dir, 200 sub_targets = { 201 "olean": [DefaultInfo(default_outputs = [olean_dir])], 202 } | ({"c": [DefaultInfo(default_outputs = [c_dir])]} if c_dir else {}), 203 ), 204 LeanLibraryInfo( 205 olean_dir = olean_dir, 206 c_dir = c_dir, 207 lib_name = ctx.attrs.name, 208 deps = ctx.attrs.deps, 209 ), 210 ] 211 212 lean_library = rule( 213 impl = _lean_library_impl, 214 attrs = { 215 "srcs": attrs.list(attrs.source(), default = [], doc = "Lean source files (.lean)"), 216 "deps": attrs.list(attrs.dep(), default = [], doc = "Lean library dependencies"), 217 "lean_flags": attrs.list(attrs.string(), default = [], doc = "Additional lean compiler flags"), 218 "extract_c": attrs.bool(default = False, doc = "Extract C code for FFI"), 219 }, 220 ) 221 222 # ═══════════════════════════════════════════════════════════════════════════════ 223 # LEAN BINARY RULE 224 # ═══════════════════════════════════════════════════════════════════════════════ 225 226 def _lean_binary_impl(ctx: AnalysisContext) -> list[Provider]: 227 """ 228 Build a Lean executable. 229 230 Compiles Lean sources and links into an executable using leanc. 231 232 Supports hierarchical module structure via root_module attr: 233 - root_module = "Straylight" means files map to Straylight.Foo, Straylight.Bar 234 - Sources are copied preserving structure under $ROOT/Straylight/ 235 - Main.lean is compiled last and linked 236 237 For flat projects (no root_module), files compile as top-level modules. 238 """ 239 lean = _get_lean() 240 leanc = _get_leanc() 241 lean_lib_dir = _get_lean_lib_dir() 242 243 if not ctx.attrs.srcs: 244 fail("lean_binary requires at least one source file") 245 246 # Output 247 exe = ctx.actions.declare_output(ctx.attrs.name) 248 olean_dir = ctx.actions.declare_output("olean", dir = True) 249 c_dir = ctx.actions.declare_output("c", dir = True) 250 251 # Collect dependency olean directories 252 dep_paths = [] 253 dep_c_dirs = [] 254 for dep in ctx.attrs.deps: 255 if LeanLibraryInfo in dep: 256 info = dep[LeanLibraryInfo] 257 if info.olean_dir: 258 dep_paths.append(info.olean_dir) 259 if info.c_dir: 260 dep_c_dirs.append(info.c_dir) 261 262 # Build LEAN_PATH - include scratch dir for local modules 263 lean_path_parts = ["$OLEAN_DIR", "$BUCK_SCRATCH_PATH"] 264 if lean_lib_dir: 265 lean_path_parts.append(lean_lib_dir) 266 for dep_path in dep_paths: 267 lean_path_parts.append(cmd_args(dep_path)) 268 269 # Script: setup, compile to C, then link 270 script_parts = ["set -e"] 271 script_parts.append("mkdir -p $OLEAN_DIR $C_DIR") 272 273 script_parts.append(cmd_args( 274 "export LEAN_PATH=", 275 cmd_args(lean_path_parts, delimiter = ":"), 276 delimiter = "", 277 )) 278 279 # Determine module structure 280 root_module = ctx.attrs.root_module 281 282 # Copy sources to scratch with proper structure 283 # For hierarchical modules: Foo.lean -> $SCRATCH/RootModule/Foo.lean 284 # For flat modules: Foo.lean -> $SCRATCH/Foo.lean 285 c_files = [] 286 compile_order = [] 287 main_src = None 288 289 for src in ctx.attrs.srcs: 290 if src.basename == "Main.lean": 291 main_src = src 292 else: 293 compile_order.append(src) 294 295 # Main.lean must be compiled last 296 if main_src: 297 compile_order.append(main_src) 298 else: 299 # No Main.lean, use first source as main 300 main_src = ctx.attrs.srcs[0] 301 302 # Setup scratch directory structure 303 if root_module: 304 script_parts.append("mkdir -p $BUCK_SCRATCH_PATH/{}".format(root_module)) 305 306 # Copy and compile each source 307 for src in compile_order: 308 module_name = src.basename.removesuffix(".lean") 309 310 if root_module and src.basename != "Main.lean": 311 # Hierarchical: copy to RootModule/Foo.lean 312 dest_path = "$BUCK_SCRATCH_PATH/{}/{}".format(root_module, src.basename) 313 full_module = "{}.{}".format(root_module, module_name) 314 c_file = "$C_DIR/{}.{}.c".format(root_module, module_name) 315 olean_file = "$OLEAN_DIR/{}/{}.olean".format(root_module, module_name) 316 script_parts.append("mkdir -p $OLEAN_DIR/{}".format(root_module)) 317 else: 318 # Flat: copy to Foo.lean or Main.lean at root 319 dest_path = "$BUCK_SCRATCH_PATH/{}".format(src.basename) 320 full_module = module_name 321 c_file = "$C_DIR/{}.c".format(module_name) 322 olean_file = "$OLEAN_DIR/{}.olean".format(module_name) 323 324 c_files.append(c_file) 325 326 # Copy source 327 script_parts.append(cmd_args("cp", src, dest_path, delimiter = " ")) 328 329 # Compile 330 compile_cmd = [ 331 lean, 332 "--root=$BUCK_SCRATCH_PATH", 333 "-o", olean_file, 334 "--c={}".format(c_file), 335 ] 336 compile_cmd.extend(ctx.attrs.lean_flags) 337 compile_cmd.append(dest_path) 338 339 script_parts.append(cmd_args(compile_cmd, delimiter = " ")) 340 341 # Link with leanc 342 link_cmd = [leanc, "-o", exe.as_output()] 343 link_cmd.extend(ctx.attrs.link_flags) 344 345 # Add all C files 346 for c_file in c_files: 347 link_cmd.append(c_file) 348 349 # Add dependency C files 350 for dep_c_dir in dep_c_dirs: 351 link_cmd.append(cmd_args(dep_c_dir, "/*.c", delimiter = "")) 352 353 script_parts.append(cmd_args(link_cmd, delimiter = " ")) 354 355 script = cmd_args(script_parts, delimiter = "\n") 356 357 cmd = cmd_args( 358 "/bin/sh", "-c", 359 cmd_args( 360 "OLEAN_DIR=", olean_dir.as_output(), 361 " C_DIR=", c_dir.as_output(), 362 " && ", script, 363 delimiter = "", 364 ), 365 ) 366 367 hidden = list(ctx.attrs.srcs) 368 hidden.extend(dep_paths) 369 hidden.extend(dep_c_dirs) 370 371 ctx.actions.run( 372 cmd_args(cmd, hidden = hidden), 373 category = "lean_link", 374 identifier = ctx.attrs.name, 375 local_only = True, 376 ) 377 378 return [ 379 DefaultInfo(default_output = exe), 380 RunInfo(args = cmd_args(exe)), 381 ] 382 383 lean_binary = rule( 384 impl = _lean_binary_impl, 385 attrs = { 386 "srcs": attrs.list(attrs.source(), default = [], doc = "Lean source files (.lean)"), 387 "deps": attrs.list(attrs.dep(), default = [], doc = "Lean library dependencies"), 388 "root_module": attrs.option(attrs.string(), default = None, doc = "Root module name for hierarchical imports (e.g., 'Straylight')"), 389 "lean_flags": attrs.list(attrs.string(), default = [], doc = "Additional lean compiler flags"), 390 "link_flags": attrs.list(attrs.string(), default = [], doc = "Additional linker flags"), 391 }, 392 ) 393 394 # ═══════════════════════════════════════════════════════════════════════════════ 395 # LEAN C LIBRARY RULE 396 # ═══════════════════════════════════════════════════════════════════════════════ 397 398 def _lean_c_library_impl(ctx: AnalysisContext) -> list[Provider]: 399 """ 400 Extract C code from Lean for FFI linking. 401 402 This is the proof-carrying code pattern: 403 1. Theorems are proven in Lean (compile-time) 404 2. C code is extracted (guaranteed to satisfy the theorems) 405 3. C code links into Rust/C++/Haskell via FFI 406 407 The extracted C can be used as a cxx_library dependency. 408 409 **Relevant for computational linear algebra:** 410 This is how Villa Straylight's layout proofs become callable from CUDA kernels. 411 The Lean theorem (e.g., FTTC) constrains the generated C types. 412 """ 413 lean = _get_lean() 414 lean_include_dir = _get_lean_include_dir() 415 lean_lib_dir = _get_lean_lib_dir() 416 417 if not ctx.attrs.srcs: 418 return [DefaultInfo(), LeanCLibraryInfo()] 419 420 # Outputs 421 c_dir = ctx.actions.declare_output("c", dir = True) 422 olean_dir = ctx.actions.declare_output("olean", dir = True) 423 include_dir = ctx.actions.declare_output("include", dir = True) 424 obj_dir = ctx.actions.declare_output("obj", dir = True) 425 archive = ctx.actions.declare_output("lib{}.a".format(ctx.attrs.name)) 426 427 # Collect dependencies 428 dep_paths = [] 429 for dep in ctx.attrs.deps: 430 if LeanLibraryInfo in dep: 431 info = dep[LeanLibraryInfo] 432 if info.olean_dir: 433 dep_paths.append(info.olean_dir) 434 435 # Build LEAN_PATH - use env var since olean_dir is output 436 lean_path_parts = ["$OLEAN_DIR"] 437 if lean_lib_dir: 438 lean_path_parts.append(lean_lib_dir) 439 for dep_path in dep_paths: 440 lean_path_parts.append(cmd_args(dep_path)) 441 442 # Get C compiler from cxx config (we use our Clang, not leanc's default) 443 cc = read_root_config("cxx", "cxx", "clang++") 444 445 script_parts = ["set -e"] 446 script_parts.append("mkdir -p $OLEAN_DIR $C_DIR $INCLUDE_DIR $OBJ_DIR") 447 448 script_parts.append(cmd_args( 449 "export LEAN_PATH=", 450 cmd_args(lean_path_parts, delimiter = ":"), 451 delimiter = "", 452 )) 453 454 # Compile Lean to C 455 # Lean requires sources to be in --root directory, so we copy to scratch 456 c_files = [] 457 for src in ctx.attrs.srcs: 458 module_name = src.basename.removesuffix(".lean") 459 c_file = "{}.c".format(module_name) 460 c_files.append(c_file) 461 462 # Copy source to scratch dir (Lean's --root requirement) 463 script_parts.append(cmd_args("cp", src, "$BUCK_SCRATCH_PATH/", delimiter = " ")) 464 465 compile_cmd = [ 466 lean, 467 "--root=$BUCK_SCRATCH_PATH", 468 "-o", "$OLEAN_DIR/{}.olean".format(module_name), 469 "--c=$C_DIR/{}".format(c_file), 470 ] 471 compile_cmd.extend(ctx.attrs.lean_flags) 472 compile_cmd.append("$BUCK_SCRATCH_PATH/{}".format(src.basename)) 473 474 script_parts.append(cmd_args(compile_cmd, delimiter = " ")) 475 476 # Generate header file for FFI exports 477 # Lean generates lean.h style headers; we create a wrapper 478 header_content = [ 479 "// Generated by lean_c_library: {}".format(ctx.attrs.name), 480 "#pragma once", 481 "#include <lean/lean.h>", 482 "", 483 "// Exported functions from Lean", 484 ] 485 for export in ctx.attrs.exports: 486 header_content.append("extern lean_object* {}(lean_object*);".format(export)) 487 488 script_parts.append(cmd_args( 489 "cat > $INCLUDE_DIR/{}.h << 'LEAN_HEADER_EOF'\n{}\nLEAN_HEADER_EOF".format( 490 ctx.attrs.name, 491 "\n".join(header_content), 492 ), 493 )) 494 495 # Compile C to objects 496 for c_file in c_files: 497 obj_file = c_file.removesuffix(".c") + ".o" 498 499 cc_cmd = [cc, "-c", "-O2", "-fPIC"] 500 if lean_include_dir: 501 cc_cmd.extend(["-I", lean_include_dir]) 502 cc_cmd.extend(["-I", "$INCLUDE_DIR"]) 503 cc_cmd.extend(ctx.attrs.cflags) 504 cc_cmd.extend(["-o", "$OBJ_DIR/{}".format(obj_file)]) 505 cc_cmd.append("$C_DIR/{}".format(c_file)) 506 507 script_parts.append(cmd_args(cc_cmd, delimiter = " ")) 508 509 # Archive objects 510 script_parts.append(cmd_args( 511 "ar rcs", archive.as_output(), "$OBJ_DIR/*.o", 512 delimiter = " ", 513 )) 514 515 script = cmd_args(script_parts, delimiter = "\n") 516 517 cmd = cmd_args( 518 "/bin/sh", "-c", 519 cmd_args( 520 "OLEAN_DIR=", olean_dir.as_output(), 521 " C_DIR=", c_dir.as_output(), 522 " INCLUDE_DIR=", include_dir.as_output(), 523 " OBJ_DIR=", obj_dir.as_output(), 524 " && ", script, 525 delimiter = "", 526 ), 527 ) 528 529 hidden = list(ctx.attrs.srcs) 530 hidden.extend(dep_paths) 531 532 ctx.actions.run( 533 cmd_args(cmd, hidden = hidden), 534 category = "lean_c_extract", 535 identifier = ctx.attrs.name, 536 local_only = True, 537 ) 538 539 return [ 540 DefaultInfo( 541 default_output = archive, 542 sub_targets = { 543 "c": [DefaultInfo(default_outputs = [c_dir])], 544 "include": [DefaultInfo(default_outputs = [include_dir])], 545 "olean": [DefaultInfo(default_outputs = [olean_dir])], 546 }, 547 ), 548 LeanLibraryInfo( 549 olean_dir = olean_dir, 550 c_dir = c_dir, 551 lib_name = ctx.attrs.name, 552 deps = ctx.attrs.deps, 553 ), 554 LeanCLibraryInfo( 555 c_sources = [], # We don't track individual files in dir output 556 include_dir = include_dir, 557 objects = [], 558 archive = archive, 559 ), 560 ] 561 562 lean_c_library = rule( 563 impl = _lean_c_library_impl, 564 attrs = { 565 "srcs": attrs.list(attrs.source(), default = [], doc = "Lean source files (.lean)"), 566 "deps": attrs.list(attrs.dep(), default = [], doc = "Lean library dependencies"), 567 "lean_flags": attrs.list(attrs.string(), default = [], doc = "Additional lean compiler flags"), 568 "cflags": attrs.list(attrs.string(), default = [], doc = "Additional C compiler flags"), 569 "exports": attrs.list(attrs.string(), default = [], doc = "Functions to export in header"), 570 }, 571 ) 572 573 # ═══════════════════════════════════════════════════════════════════════════════ 574 # LEAN TOOLCHAIN RULE 575 # ═══════════════════════════════════════════════════════════════════════════════ 576 577 LeanToolchainInfo = provider(fields = { 578 "lean": provider_field(str), 579 "leanc": provider_field(str), 580 "lean_lib_dir": provider_field(str | None, default = None), 581 "lean_include_dir": provider_field(str | None, default = None), 582 }) 583 584 def _lean_toolchain_impl(ctx: AnalysisContext) -> list[Provider]: 585 """ 586 Lean toolchain with paths from .buckconfig.local. 587 588 Reads [lean] section for absolute Nix store paths: 589 lean - Lean compiler 590 leanc - Lean C code generator 591 lean_lib_dir - Lean library directory 592 lean_include_dir - Lean include directory 593 """ 594 # Read from config, fall back to attrs 595 lean = read_root_config("lean", "lean", ctx.attrs.lean) 596 leanc = read_root_config("lean", "leanc", ctx.attrs.leanc) 597 lean_lib_dir = read_root_config("lean", "lean_lib_dir", ctx.attrs.lean_lib_dir) 598 lean_include_dir = read_root_config("lean", "lean_include_dir", ctx.attrs.lean_include_dir) 599 600 return [ 601 DefaultInfo(), 602 LeanToolchainInfo( 603 lean = lean, 604 leanc = leanc, 605 lean_lib_dir = lean_lib_dir, 606 lean_include_dir = lean_include_dir, 607 ), 608 ] 609 610 lean_toolchain = rule( 611 impl = _lean_toolchain_impl, 612 attrs = { 613 "lean": attrs.string(default = "lean", doc = "Path to lean compiler"), 614 "leanc": attrs.string(default = "leanc", doc = "Path to leanc"), 615 "lean_lib_dir": attrs.option(attrs.string(), default = None, doc = "Lean library directory"), 616 "lean_include_dir": attrs.option(attrs.string(), default = None, doc = "Lean include directory"), 617 }, 618 is_toolchain_rule = True, 619 ) 620 621 def _system_lean_toolchain_impl(_ctx: AnalysisContext) -> list[Provider]: 622 """ 623 System Lean toolchain. 624 625 DISABLED. No fallbacks. Configure via Nix or fail. 626 """ 627 fail(""" 628 system_lean_toolchain is disabled. 629 630 Zeitschrift does not support fallback toolchains. 631 Configure your Lean toolchain via Nix: 632 633 [lean] 634 lean = /nix/store/.../bin/lean 635 leanc = /nix/store/.../bin/leanc 636 lean_lib_dir = /nix/store/.../lib/lean 637 lean_include_dir = /nix/store/.../include 638 639 Then run: nix develop 640 641 If you see this error, your .buckconfig.local is missing or stale. 642 """) 643 644 system_lean_toolchain = rule( 645 impl = _system_lean_toolchain_impl, 646 attrs = {}, 647 is_toolchain_rule = True, 648 ) 649 650 # ═══════════════════════════════════════════════════════════════════════════════ 651 # LEAN LAKE PROJECT RULE - DISABLED 652 # ═══════════════════════════════════════════════════════════════════════════════ 653 # 654 # Lake is Lean's package manager but introduces non-hermetic builds: 655 # - Downloads ~2GB for Mathlib 656 # - Caches in .lake/ outside Buck2's control 657 # - No content-addressed derivations 658 # 659 # If you need Mathlib, manage it via Nix overlays or a separate toolchain. 660 # The lean_library/lean_binary rules work for standalone Lean code. 661 662 def _lean_lake_build_impl(ctx: AnalysisContext) -> list[Provider]: 663 """DISABLED: Lake builds are non-hermetic.""" 664 fail(""" 665 lean_lake_build is disabled. 666 667 Lake introduces non-hermetic builds that bypass Buck2's caching and 668 content-addressed derivation model. Mathlib downloads (~2GB) and 669 .lake/ caches are not tracked. 670 671 Options: 672 1. Use lean_library/lean_binary for standalone Lean code (no Lake deps) 673 2. Manage Mathlib via Nix overlay (recommended for large proofs) 674 3. Build outside Buck2 with 'lake build' directly 675 676 See: toolchains/lean.bzl for lean_library, lean_binary, lean_c_library 677 """) 678 679 lean_lake_build = rule( 680 impl = _lean_lake_build_impl, 681 attrs = { 682 "srcs": attrs.list(attrs.source(), default = [], doc = "Lean source files"), 683 "lakefile": attrs.option(attrs.source(), default = None, doc = "lakefile.lean"), 684 "toolchain_file": attrs.option(attrs.source(), default = None, doc = "lean-toolchain file"), 685 }, 686 )