Conversation
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: defaults Review profile: CHILL Plan: Pro Run ID: ⛔ Files ignored due to path filters (1)
📒 Files selected for processing (1)
🚧 Files skipped from review as they are similar to previous changes (1)
📝 WalkthroughWalkthroughAdds Lean language support: new Bazel Starlark rules and toolchain targets, http_archive entries for platform-specific Lean toolchains, a resolved toolchain exporter exposing LEAN/LEANC/LEANCHECKER, build helpers for Lean-generated C, a minimal Hello.lean example, and env wiring for tool substitutions. Changes
Sequence Diagram(s)sequenceDiagram
participant DEV as Developer
participant BAZEL as Bazel
participant REG as ToolchainRegistry
participant ARCH as http_archive
participant TC as resolved_toolchain
participant GEN as genrule/action
participant TOOL as Lean binaries
DEV->>BAZEL: Invoke build referencing $(LEAN)/$(LEANC)/$(LEANCHECKER)
BAZEL->>REG: Lookup registered toolchains
REG->>ARCH: Fetch & unpack archives
REG->>TC: Instantiate toolchain (toolchain_type -> tool labels)
TC-->>BAZEL: Provide TemplateVariableInfo (LEAN, LEANC, LEANCHECKER) + tool files
BAZEL->>GEN: Run genrule using provided tool paths
GEN->>TOOL: Invoke lean/leanc/leanchecker
TOOL-->>GEN: Emit generated C/artifacts
GEN-->>BAZEL: Produce outputs
BAZEL-->>DEV: Build complete
Estimated code review effort🎯 4 (Complex) | ⏱️ ~60 minutes Poem
🚥 Pre-merge checks | ✅ 3✅ Passed checks (3 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 2
🧹 Nitpick comments (3)
experiments/leaning/BUILD.bazel (1)
11-11: Harden the genrule command for determinism.Since
srcshas a single file, prefer$<and explicit file paths instead of unquoted$(SRCS)and*expansion.Proposed command tweak
- cmd = "mkdir $(RULEDIR)/src && cp $(SRCS) $(RULEDIR)/src && $(LEAN) -c $@ $(RULEDIR)/src/*", + cmd = "mkdir -p $(RULEDIR)/src && cp $< $(RULEDIR)/src/Hello.lean && $(LEAN) -c $@ $(RULEDIR)/src/Hello.lean",🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@experiments/leaning/BUILD.bazel` at line 11, The genrule command is brittle due to unquoted $(SRCS) and wildcard '*' expansion; update the genrule so it uses the single-source automatic variable ($<) and explicit file paths into $(RULEDIR)/src instead of $(SRCS) and *: copy $< into $(RULEDIR)/src (preserving filename), then invoke $(LEAN) -c $@ on that specific copied filename (use $(notdir $<) or equivalent to reference the basename) so the rule is deterministic and avoids shell globbing/word-splitting issues involving $(SRCS) and '*'.third_party/lean/lean.MODULE.bazel (2)
7-7: Consider adding a backup mirror URL per archive for fetch resilience.Each archive currently has a single GitHub URL. A secondary mirror can reduce CI flakiness during upstream outages/rate limits.
Also applies to: 15-15, 23-23
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@third_party/lean/lean.MODULE.bazel` at line 7, Update each urls = [...] attribute in third_party/lean/lean.MODULE.bazel to include a secondary mirror entry for each archive (i.e., add a backup URL alongside the existing GitHub URL). Locate the three occurrences of the urls attribute in this MODULE file and append a reliable mirror or CDN URL as the next item in the list so fetch operations can fall back without changing the attribute name; keep the original GitHub URL first and ensure both entries are valid and use the same archive filename.
3-25: Reduce repeated Lean release literals to avoid version-drift mistakes.The three
http_archiveblocks duplicate version/build-file/release-prefix strings. Centralizing constants will make upgrades safer.♻️ Suggested refactor
+LEAN_VERSION = "4.28.0" +LEAN_BUILD_FILE = "@//third_party/lean:lean.BUILD.bazel" +LEAN_RELEASE_PREFIX = "https://github.com/leanprover/lean4/releases/download/v4.28.0" + http_archive( name = "lean_linux_x86_64", sha256 = "ceb3a3f844f7aebf63245e2b51c28d5b0ed38942c19f93cf3febd520302160bd", strip_prefix = "lean-4.28.0-linux", - urls = ["https://github.com/leanprover/lean4/releases/download/v4.28.0/lean-4.28.0-linux.tar.zst"], - build_file = "@//third_party/lean:lean.BUILD.bazel", + urls = [LEAN_RELEASE_PREFIX + "/lean-4.28.0-linux.tar.zst"], + build_file = LEAN_BUILD_FILE, ) http_archive( name = "lean_linux_aarch64", sha256 = "c865801261c747d4f15d08beca9abc20aca907904abbb284de25a37f4b4558bc", strip_prefix = "lean-4.28.0-linux_aarch64", - urls = ["https://github.com/leanprover/lean4/releases/download/v4.28.0/lean-4.28.0-linux_aarch64.tar.zst"], - build_file = "@//third_party/lean:lean.BUILD.bazel", + urls = [LEAN_RELEASE_PREFIX + "/lean-4.28.0-linux_aarch64.tar.zst"], + build_file = LEAN_BUILD_FILE, ) http_archive( name = "lean_darwin_aarch64", sha256 = "61942f9d1907db918020154a517c87fb64841e48cebb0032fc0909df8d189a05", strip_prefix = "lean-4.28.0-darwin_aarch64", - urls = ["https://github.com/leanprover/lean4/releases/download/v4.28.0/lean-4.28.0-darwin_aarch64.tar.zst"], - build_file = "@//third_party/lean:lean.BUILD.bazel", + urls = [LEAN_RELEASE_PREFIX + "/lean-4.28.0-darwin_aarch64.tar.zst"], + build_file = LEAN_BUILD_FILE, )🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@third_party/lean/lean.MODULE.bazel` around lines 3 - 25, The three http_archive entries (names: lean_linux_x86_64, lean_linux_aarch64, lean_darwin_aarch64) duplicate the Lean release/version/strip_prefix/urls/build_file literals; extract shared constants (e.g., LEAN_VERSION = "4.28.0", BASE_URL = "https://github.com/leanprover/lean4/releases/download/v{LEAN_VERSION}/", BUILD_FILE = "@//third_party/lean:lean.BUILD.bazel") and per-arch values (sha256 and strip_prefix suffixes) into variables at the top of the MODULE, then reference those variables in each http_archive call (replace inline urls, strip_prefix and build_file literals with the variables) so upgrades only change the centralized constants and avoid version-drift across lean_linux_x86_64 / lean_linux_aarch64 / lean_darwin_aarch64.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@third_party/lean/lean.BUILD.bazel`:
- Around line 3-21: The BUILD currently only declares native_binary targets
("lean", "leanc", "leanchecker") but does not model the Lean runtime shared
library, causing CI failures for libInit_shared.so; add a cc_library (e.g., name
= "libinit_shared" or "lean_runtime_shared") that declares the runtime
sources/headers and produces a shared library (.so/.dylib) and then make the
binaries depend on it (add it to the dep list of the corresponding
native_binary/cc_binary targets or export it via a cc_library wrapper) so the
runtime shared object is built and linked into the distribution; ensure correct
visibility and platform-specific linkopts so CI can find libInit_shared at
runtime.
In `@third_party/lean/resolved_toolchain.bzl`:
- Around line 4-11: The DefaultInfo currently only exposes the executable files
and omits transitive runfiles; collect and merge the default_runfiles (or
runfiles) from toolchain.tools.lean, toolchain.tools.leanc, and
toolchain.tools.leanchecker into a single depset (following the pattern in
tools/c64/basic_binary.bzl) and pass that merged runfiles via
DefaultInfo(default_runfiles = merged_runfiles, files = depset([...])) so
dynamically linked shared libraries are propagated; update the return list near
the TemplateVariableInfo block and the DefaultInfo invocation that references
toolchain.tools.lean, toolchain.tools.leanc, and toolchain.tools.leanchecker.
---
Nitpick comments:
In `@experiments/leaning/BUILD.bazel`:
- Line 11: The genrule command is brittle due to unquoted $(SRCS) and wildcard
'*' expansion; update the genrule so it uses the single-source automatic
variable ($<) and explicit file paths into $(RULEDIR)/src instead of $(SRCS) and
*: copy $< into $(RULEDIR)/src (preserving filename), then invoke $(LEAN) -c $@
on that specific copied filename (use $(notdir $<) or equivalent to reference
the basename) so the rule is deterministic and avoids shell
globbing/word-splitting issues involving $(SRCS) and '*'.
In `@third_party/lean/lean.MODULE.bazel`:
- Line 7: Update each urls = [...] attribute in
third_party/lean/lean.MODULE.bazel to include a secondary mirror entry for each
archive (i.e., add a backup URL alongside the existing GitHub URL). Locate the
three occurrences of the urls attribute in this MODULE file and append a
reliable mirror or CDN URL as the next item in the list so fetch operations can
fall back without changing the attribute name; keep the original GitHub URL
first and ensure both entries are valid and use the same archive filename.
- Around line 3-25: The three http_archive entries (names: lean_linux_x86_64,
lean_linux_aarch64, lean_darwin_aarch64) duplicate the Lean
release/version/strip_prefix/urls/build_file literals; extract shared constants
(e.g., LEAN_VERSION = "4.28.0", BASE_URL =
"https://github.com/leanprover/lean4/releases/download/v{LEAN_VERSION}/",
BUILD_FILE = "@//third_party/lean:lean.BUILD.bazel") and per-arch values (sha256
and strip_prefix suffixes) into variables at the top of the MODULE, then
reference those variables in each http_archive call (replace inline urls,
strip_prefix and build_file literals with the variables) so upgrades only change
the centralized constants and avoid version-drift across lean_linux_x86_64 /
lean_linux_aarch64 / lean_darwin_aarch64.
ℹ️ Review info
Configuration used: defaults
Review profile: CHILL
Plan: Pro
⛔ Files ignored due to path filters (1)
MODULE.bazel.lockis excluded by!**/*.lock
📒 Files selected for processing (9)
BUILD.bazelMODULE.bazelexperiments/leaning/BUILD.bazelexperiments/leaning/Hello.leanthird_party/lean/BUILD.bazelthird_party/lean/lean.BUILD.bazelthird_party/lean/lean.MODULE.bazelthird_party/lean/lean_toolchain.bzlthird_party/lean/resolved_toolchain.bzl
| native_binary( | ||
| name = "lean", | ||
| src = "bin/lean", | ||
| visibility = ["//visibility:public"], | ||
| ) | ||
|
|
||
| native_binary( | ||
| name = "leanc", | ||
| src = "bin/leanc", | ||
| visibility = ["//visibility:public"], | ||
| ) | ||
|
|
||
| native_binary( | ||
| name = "leanchecker", | ||
| src = "bin/leanchecker", | ||
| visibility = ["//visibility:public"], | ||
| ) | ||
|
|
||
| # TODO: Add cc_library for lean runtime |
There was a problem hiding this comment.
Lean runtime shared libraries are not modeled, and CI is already failing.
The current setup exports executables (Lines 3-19), but runtime .so/.dylib dependencies are not represented; this matches the libInit_shared.so failure from CI. Line 21’s TODO is now a release blocker, not a follow-up item.
Suggested direction
+# Expose Lean runtime shared libraries so toolchain consumers can propagate them.
+filegroup(
+ name = "lean_runtime_libs",
+ srcs = glob([
+ "lib/**/*.so",
+ "lib/**/*.dylib",
+ ]),
+ visibility = ["//visibility:public"],
+)📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
| native_binary( | |
| name = "lean", | |
| src = "bin/lean", | |
| visibility = ["//visibility:public"], | |
| ) | |
| native_binary( | |
| name = "leanc", | |
| src = "bin/leanc", | |
| visibility = ["//visibility:public"], | |
| ) | |
| native_binary( | |
| name = "leanchecker", | |
| src = "bin/leanchecker", | |
| visibility = ["//visibility:public"], | |
| ) | |
| # TODO: Add cc_library for lean runtime | |
| native_binary( | |
| name = "lean", | |
| src = "bin/lean", | |
| visibility = ["//visibility:public"], | |
| ) | |
| native_binary( | |
| name = "leanc", | |
| src = "bin/leanc", | |
| visibility = ["//visibility:public"], | |
| ) | |
| native_binary( | |
| name = "leanchecker", | |
| src = "bin/leanchecker", | |
| visibility = ["//visibility:public"], | |
| ) | |
| # TODO: Add cc_library for lean runtime | |
| # Expose Lean runtime shared libraries so toolchain consumers can propagate them. | |
| filegroup( | |
| name = "lean_runtime_libs", | |
| srcs = glob([ | |
| "lib/**/*.so", | |
| "lib/**/*.dylib", | |
| ]), | |
| visibility = ["//visibility:public"], | |
| ) |
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@third_party/lean/lean.BUILD.bazel` around lines 3 - 21, The BUILD currently
only declares native_binary targets ("lean", "leanc", "leanchecker") but does
not model the Lean runtime shared library, causing CI failures for
libInit_shared.so; add a cc_library (e.g., name = "libinit_shared" or
"lean_runtime_shared") that declares the runtime sources/headers and produces a
shared library (.so/.dylib) and then make the binaries depend on it (add it to
the dep list of the corresponding native_binary/cc_binary targets or export it
via a cc_library wrapper) so the runtime shared object is built and linked into
the distribution; ensure correct visibility and platform-specific linkopts so CI
can find libInit_shared at runtime.
| return [ | ||
| platform_common.TemplateVariableInfo({ | ||
| "LEAN": toolchain.tools.lean.path, | ||
| "LEANC": toolchain.tools.leanc.path, | ||
| "LEANCHECKER": toolchain.tools.leanchecker.path, | ||
| }), | ||
| DefaultInfo(files = depset([toolchain.tools.lean, toolchain.tools.leanc, toolchain.tools.leanchecker])), | ||
| ] |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
# Verify resolved_toolchain currently exports only files and no runfiles propagation.
rg -n -C3 'TemplateVariableInfo|DefaultInfo\(|files\s*=\s*depset|runfiles\s*=' third_party/lean/resolved_toolchain.bzlRepository: ffortier/mono
Length of output: 529
🏁 Script executed:
#!/bin/bash
# Find the toolchain definition and understand how Lean tools are provided
fd -t f "toolchain" third_party/lean/ 2>/dev/null | head -20
echo "=== Searching for Lean toolchain_type definition ==="
rg -n "toolchain_type" third_party/lean/
echo "=== Searching for libInit_shared.so references ==="
rg -r "libInit_shared" .
echo "=== Looking at Lean tool definitions ==="
rg -n -B2 -A5 "tools\.lean\|tools\.leanc" third_party/lean/ | head -50Repository: ffortier/mono
Length of output: 50372
🏁 Script executed:
#!/bin/bash
# Examine lean_toolchain.bzl to understand tool structure
head -100 third_party/lean/lean_toolchain.bzl
echo "=== Look for tool definitions and how they're created ==="
rg -n -A10 "tools\s*=" third_party/lean/lean_toolchain.bzl | head -60Repository: ffortier/mono
Length of output: 1772
🏁 Script executed:
#!/bin/bash
# Find where the actual lean tools are sourced from
find third_party/lean -name "*.bzl" -o -name "*.bazel" | head -20
echo "=== Check the BUILD file ==="
cat third_party/lean/BUILD.bazel 2>/dev/null || echo "File not found"
echo "=== Look for any references to lean tools being provided with deps ==="
rg -n "lean|leanc|leanchecker" third_party/lean/ --type bazel -B2 -A2 | head -100Repository: ffortier/mono
Length of output: 7636
🏁 Script executed:
#!/bin/bash
# Check the full lean.BUILD.bazel to see if there are any data/deps on shared libraries
cat third_party/lean/lean.BUILD.bazel
echo "=== Look for any data files or runtime dependencies ==="
rg -n "data\s*=|runfiles|\.so" third_party/lean/
echo "=== Check if lean tools are dynamically linked (look for lib directories in archive) ==="
rg -n "lib/" third_party/lean/Repository: ffortier/mono
Length of output: 725
🏁 Script executed:
#!/bin/bash
# Understand the issue better: check if native_binary targets have runfiles
echo "=== Search for native_binary usage and runfiles pattern ==="
rg -n "native_binary" . --type bazel -B2 -A5 | head -100
echo "=== Check if there are any Bazel configuration or CI files that document the libInit_shared.so error ==="
fd -e log -e txt -e sh | xargs rg "libInit_shared" 2>/dev/null | head -20
echo "=== Look at how other toolchains handle DefaultInfo with tools ==="
rg -n "DefaultInfo.*files.*depset" . --type bazel -B3 -A3 | head -80Repository: ffortier/mono
Length of output: 3820
Propagate tool runfiles to include shared library dependencies.
The DefaultInfo at line 10 exposes only the executable files without propagating their transitive runfiles. For dynamically-linked Lean tools, this drops required shared libraries at runtime. Merge the default_runfiles from each tool target (following the pattern in tools/c64/basic_binary.bzl) and pass the merged runfiles to DefaultInfo.
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@third_party/lean/resolved_toolchain.bzl` around lines 4 - 11, The DefaultInfo
currently only exposes the executable files and omits transitive runfiles;
collect and merge the default_runfiles (or runfiles) from toolchain.tools.lean,
toolchain.tools.leanc, and toolchain.tools.leanchecker into a single depset
(following the pattern in tools/c64/basic_binary.bzl) and pass that merged
runfiles via DefaultInfo(default_runfiles = merged_runfiles, files =
depset([...])) so dynamically linked shared libraries are propagated; update the
return list near the TemplateVariableInfo block and the DefaultInfo invocation
that references toolchain.tools.lean, toolchain.tools.leanc, and
toolchain.tools.leanchecker.
There was a problem hiding this comment.
Actionable comments posted: 3
♻️ Duplicate comments (1)
third_party/lean/lean.BUILD.bazel (1)
5-21:⚠️ Potential issue | 🔴 CriticalModel the shared Lean runtime, not just the static archives.
leanrtonly wraps headers plus.afiles, and Line 51 still leaves the actual runtime shared objects as a TODO. The exportednative_binarytargets therefore still have no way to carry the Lean shared runtime in runfiles, solean/leanc/leancheckerremain broken on platforms where the distribution expectslibInit_shared.so/.dylibbeside the executable.Suggested direction
+filegroup( + name = "lean_runtime_shared", + srcs = glob([ + "lib/**/*.so", + "lib/**/*.dylib", + ]), + visibility = ["//visibility:public"], +) + -# TODO: Add cc_library for lean runtimeThen wire
:lean_runtime_sharedinto whatever rule packages or executes thesenative_binarytargets so the shared objects land in runfiles/artifacts.Also applies to: 23-51
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@third_party/lean/lean.BUILD.bazel` around lines 5 - 21, The native binaries (targets named "lean", "leanc", "leanchecker") are not shipping the Lean shared runtime; update the packaging so the shared runtime artifacts are modeled and included: create or update the target (referenced as :lean_runtime_shared or expand leanrt) to list the platform shared libraries (libInit_shared.so/.dylib etc.) as outputs/inputs and then add that target to each native_binary's runfiles by adding data = [":lean_runtime_shared"] (or equivalent attribute used in this repo) to the native_binary declarations so the shared objects are present in runfiles alongside the executables.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@third_party/lean/lean_binary.bzl`:
- Around line 4-15: The lean_binary wrapper currently passes deps explicitly to
cc_binary and also forwards **kwargs, which will conflict if a caller supplies
deps; update lean_binary (and similarly the lean_cc_library wrapper) to remove
or merge any deps from kwargs before forwarding: in lean_binary capture deps =
kwargs.pop("deps", []) (or equivalent), then call cc_binary with deps = [":" +
name + "_cc"] + deps and the remaining **kwargs; do the analogous pop/merge for
the select(...) deps in the lean_cc_library helper so no attribute is passed
twice.
In `@third_party/lean/lean_cc_library.bzl`:
- Around line 16-19: The deps select in lean_cc_library.bzl currently keys only
on OS and hardcodes aarch64 runtimes, so add CPU-aware cases or mirror toolchain
constraints: update the select(...) used for deps to include combinations for
both OS and CPU (e.g. entries that match linux + x86_64 ->
"@lean_linux_x86_64//:leanrt" and linux + aarch64 ->
"@lean_linux_aarch64//:leanrt", and similarly for darwin), ensuring the labels
referenced match the toolchain names registered (e.g.
lean_linux_x86_64_toolchain / lean_linux_aarch64_toolchain); alternatively, if
x86_64 runtimes are not supported, remove the x86_64 toolchain registration
instead of leaving an incorrect runtime mapping.
- Around line 3-10: The lean_cc_library wrapper currently allows multiple
entries in srcs but generates outs and uses $@ in cmd (which only works for a
single out) and flattens sources into one directory; update the lean_cc_library
function to guard against multi-file targets by checking srcs and failing fast
when len(srcs) != 1 (use Starlark's fail() with a clear message referencing
srcs, outs and the genrule invocation), so only single Lean source files are
allowed until full multi-file support (and proper copying/preservation of module
paths) is implemented.
---
Duplicate comments:
In `@third_party/lean/lean.BUILD.bazel`:
- Around line 5-21: The native binaries (targets named "lean", "leanc",
"leanchecker") are not shipping the Lean shared runtime; update the packaging so
the shared runtime artifacts are modeled and included: create or update the
target (referenced as :lean_runtime_shared or expand leanrt) to list the
platform shared libraries (libInit_shared.so/.dylib etc.) as outputs/inputs and
then add that target to each native_binary's runfiles by adding data =
[":lean_runtime_shared"] (or equivalent attribute used in this repo) to the
native_binary declarations so the shared objects are present in runfiles
alongside the executables.
ℹ️ Review info
⚙️ Run configuration
Configuration used: defaults
Review profile: CHILL
Plan: Pro
Run ID: de739612-f486-4763-a610-d33608096980
📒 Files selected for processing (4)
experiments/leaning/BUILD.bazelthird_party/lean/lean.BUILD.bazelthird_party/lean/lean_binary.bzlthird_party/lean/lean_cc_library.bzl
🚧 Files skipped from review as they are similar to previous changes (1)
- experiments/leaning/BUILD.bazel
| def lean_binary(name, srcs, **kwargs): | ||
| lean_cc_library( | ||
| name = name + "_cc", | ||
| srcs = srcs, | ||
| ) | ||
|
|
||
| cc_binary( | ||
| name = name, | ||
| srcs = [], | ||
| deps = [":" + name + "_cc"], | ||
| **kwargs | ||
| ) |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
find . -type f -name "lean_binary.bzl" -o -name "lean_cc_library.bzl" | head -20Repository: ffortier/mono
Length of output: 130
🏁 Script executed:
cat -n ./third_party/lean/lean_binary.bzlRepository: ffortier/mono
Length of output: 491
🏁 Script executed:
cat -n ./third_party/lean/lean_cc_library.bzlRepository: ffortier/mono
Length of output: 997
🌐 Web query:
Bazel legacy macro kwargs duplicate keyword argument collision behavior
💡 Result:
In Bazel legacy macros (regular Starlark functions), the expansion ultimately performs normal Starlark function calls to rules (e.g. native.cc_library(...)). In Starlark, keyword argument names must be unique across the entire call, including keywords coming from **kwargs. If the same keyword appears twice (e.g. once explicitly and once inside **kwargs, or in two different ** expansions), the call fails with an error (duplicate keyword argument) rather than picking one value. [1], [2]
What this means for macros that forward **kwargs
This is an error pattern:
def my_macro(name, **kwargs):
native.cc_library(
name = name,
linkstatic = 1, # macro hard-codes
**kwargs, # user might also pass linkstatic
)If the caller does my_macro(name="x", linkstatic=0), the inner native.cc_library(...) call has linkstatic twice ⇒ error. [1], [2]
Common ways to avoid collisions
- Pop the key before forwarding:
def my_macro(name, **kwargs):
linkstatic = kwargs.pop("linkstatic", 1)
native.cc_library(name = name, linkstatic = linkstatic, **kwargs)- Merge into a dict so only one value is passed, with a defined precedence (example: “user wins”):
def my_macro(name, **kwargs):
attrs = dict(kwargs)
attrs.setdefault("linkstatic", 1)
native.cc_library(name = name, **attrs)If you want an explicit “last wins” merge helper, bazel-skylib’s dicts.add documents that later dictionaries override earlier ones (useful for building attrs), but you must still ensure the final call doesn’t pass the same keyword twice. [3]
Sources:
[1] Starlark Rust API docs: named argument names must be unique (explicit + **kwargs)
[2] starlark-go implementation: raises duplicate keyword arg
[3] bazel-skylib dicts.add: later dict overrides earlier ones in merges
Don't expose deps via **kwargs.
Both files have explicit deps attributes followed by **kwargs forwarding. In Bazel legacy macros (Starlark), passing a keyword argument twice—once explicitly and once inside **kwargs—causes a runtime error. If a caller passes deps = [...] to lean_binary(), the deps = [":" + name + "_cc"] on line 13 will collide with the kwargs, causing the call to fail.
The same pattern exists in third_party/lean/lean_cc_library.bzl (lines 16–20), where explicit deps = select({...}) conflicts with any deps in kwargs.
Extract conflicting attributes before forwarding **kwargs, either by popping from kwargs or by merging into a single dict before calling the inner rule. For example:
def lean_binary(name, srcs, **kwargs):
lean_cc_library(name = name + "_cc", srcs = srcs)
deps = kwargs.pop("deps", [])
cc_binary(
name = name,
srcs = [],
deps = [":" + name + "_cc"] + deps,
**kwargs
)🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@third_party/lean/lean_binary.bzl` around lines 4 - 15, The lean_binary
wrapper currently passes deps explicitly to cc_binary and also forwards
**kwargs, which will conflict if a caller supplies deps; update lean_binary (and
similarly the lean_cc_library wrapper) to remove or merge any deps from kwargs
before forwarding: in lean_binary capture deps = kwargs.pop("deps", []) (or
equivalent), then call cc_binary with deps = [":" + name + "_cc"] + deps and the
remaining **kwargs; do the analogous pop/merge for the select(...) deps in the
lean_cc_library helper so no attribute is passed twice.
| def lean_cc_library(name, srcs, **kwargs): | ||
| native.genrule( | ||
| name = name + "_source", | ||
| srcs = srcs, | ||
| outs = [s + ".c" for s in srcs], | ||
| # TODO: Lean don't like symlinks. When building the actual rules, we will need to create a proper source root with hardlinks or copies. | ||
| cmd = "mkdir $(RULEDIR)/src && cp $(SRCS) $(RULEDIR)/src && $(LEAN) -c $@ $(RULEDIR)/src/*", | ||
| toolchains = ["//third_party/lean:resolved"], |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
find . -name "lean_cc_library.bzl" -type fRepository: ffortier/mono
Length of output: 95
🏁 Script executed:
cat -n ./third_party/lean/lean_cc_library.bzlRepository: ffortier/mono
Length of output: 997
🏁 Script executed:
rg "lean_cc_library" --type bzl -B 2 -A 5Repository: ffortier/mono
Length of output: 84
🏁 Script executed:
rg "lean_cc_library" -B 2 -A 5Repository: ffortier/mono
Length of output: 1269
🏁 Script executed:
rg "lean_binary\(" -B 3 -A 10Repository: ffortier/mono
Length of output: 1158
🏁 Script executed:
rg "srcs\s*=\s*\[" experiments/leaning/BUILD.bazel -A 2Repository: ffortier/mono
Length of output: 85
🌐 Web query:
Bazel genrule $@ variable multiple outputs outs semantics
💡 Result:
In a genrule, $@ is only defined when outs has exactly one file. If outs has multiple entries, using $@ (or @) is a build error. Use $(OUTS) or per-output $(location ...)/$(locations ...) instead. [1]
What to use with multiple outputs
-
All outputs as a list:
$(OUTS)expands to theoutslist (space-delimited). [1]
Caveat: it’s not robust if filenames can contain spaces/special characters. [1] -
A specific output:
$(location :some_out_file)wheresome_out_fileis one of the filenames inouts(Bazel allows referencing an output file by name here). [2] -
Output directory:
- Prefer
$(RULEDIR)for the rule’s output directory (stable semantics). [1] $(@d)means:- with one output: directory containing that output
- with multiple outputs: the package’s root under the genfiles tree (even if all outs are in the same subdir). [1]
- Prefer
Example pattern (multiple outs)
genrule(
name = "g",
outs = ["a.txt", "b.txt"],
cmd = "echo hi > $(location :a.txt) && echo bye > $(location :b.txt)",
)This avoids $@ entirely and is explicit per output. [1][2]
🏁 Script executed:
rg "lean_binary\|lean_cc_library" -A 5 | grep -E "srcs\s*=" | head -20Repository: ffortier/mono
Length of output: 39
🏁 Script executed:
find . -name "BUILD.bazel" -type f -exec grep -l "lean_binary\|lean_cc_library" {} \; | head -10Repository: ffortier/mono
Length of output: 90
🏁 Script executed:
cat -n ./experiments/leaning/BUILD.bazelRepository: ffortier/mono
Length of output: 219
Rule only supports single Lean source files.
outs generates multiple outputs for each file in srcs, but the command uses $@, which Bazel only defines when outs has exactly one file. Multi-source targets will fail with a build error. Additionally, the cp $(SRCS) $(RULEDIR)/src step collapses all sources into one directory, breaking module paths and causing basename collisions. Add a guard to enforce single-source constraint until full multi-file support is implemented.
Fail-fast guard
def lean_cc_library(name, srcs, **kwargs):
+ if len(srcs) != 1:
+ fail("lean_cc_library currently supports exactly one Lean source")
native.genrule(📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
| def lean_cc_library(name, srcs, **kwargs): | |
| native.genrule( | |
| name = name + "_source", | |
| srcs = srcs, | |
| outs = [s + ".c" for s in srcs], | |
| # TODO: Lean don't like symlinks. When building the actual rules, we will need to create a proper source root with hardlinks or copies. | |
| cmd = "mkdir $(RULEDIR)/src && cp $(SRCS) $(RULEDIR)/src && $(LEAN) -c $@ $(RULEDIR)/src/*", | |
| toolchains = ["//third_party/lean:resolved"], | |
| def lean_cc_library(name, srcs, **kwargs): | |
| if len(srcs) != 1: | |
| fail("lean_cc_library currently supports exactly one Lean source") | |
| native.genrule( | |
| name = name + "_source", | |
| srcs = srcs, | |
| outs = [s + ".c" for s in srcs], | |
| # TODO: Lean don't like symlinks. When building the actual rules, we will need to create a proper source root with hardlinks or copies. | |
| cmd = "mkdir $(RULEDIR)/src && cp $(SRCS) $(RULEDIR)/src && $(LEAN) -c $@ $(RULEDIR)/src/*", | |
| toolchains = ["//third_party/lean:resolved"], |
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@third_party/lean/lean_cc_library.bzl` around lines 3 - 10, The
lean_cc_library wrapper currently allows multiple entries in srcs but generates
outs and uses $@ in cmd (which only works for a single out) and flattens sources
into one directory; update the lean_cc_library function to guard against
multi-file targets by checking srcs and failing fast when len(srcs) != 1 (use
Starlark's fail() with a clear message referencing srcs, outs and the genrule
invocation), so only single Lean source files are allowed until full multi-file
support (and proper copying/preservation of module paths) is implemented.
There was a problem hiding this comment.
🧹 Nitpick comments (1)
third_party/lean/BUILD.bazel (1)
6-10: Missing macOS x86_64 platform support.The platforms list covers Linux (x86_64, aarch64) and macOS aarch64, but omits macOS x86_64 (Intel Macs). If Intel Mac support is needed, add:
("macos", "x86_64", "lean_darwin_x86_64"),This would also require a corresponding
http_archiveinlean.MODULE.bazel.🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@third_party/lean/BUILD.bazel` around lines 6 - 10, The platforms list in the BUILD.bazel fragment (the platforms variable) is missing macOS x86_64 support; add the tuple ("macos", "x86_64", "lean_darwin_x86_64") to the platforms list and ensure you also add the corresponding http_archive entry named lean_darwin_x86_64 in lean.MODULE.bazel so the new platform artifact is fetched and available.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Nitpick comments:
In `@third_party/lean/BUILD.bazel`:
- Around line 6-10: The platforms list in the BUILD.bazel fragment (the
platforms variable) is missing macOS x86_64 support; add the tuple ("macos",
"x86_64", "lean_darwin_x86_64") to the platforms list and ensure you also add
the corresponding http_archive entry named lean_darwin_x86_64 in
lean.MODULE.bazel so the new platform artifact is fetched and available.
ℹ️ Review info
⚙️ Run configuration
Configuration used: defaults
Review profile: CHILL
Plan: Pro
Run ID: 6da3acc3-d17e-489a-bbd8-feb339f07289
📒 Files selected for processing (12)
BUILD.bazelMODULE.bazelenv/BUILD.bazelexperiments/leaning/BUILD.bazelexperiments/leaning/Hello.leanthird_party/lean/BUILD.bazelthird_party/lean/lean.BUILD.bazelthird_party/lean/lean.MODULE.bazelthird_party/lean/lean_binary.bzlthird_party/lean/lean_cc_library.bzlthird_party/lean/lean_toolchain.bzlthird_party/lean/resolved_toolchain.bzl
🚧 Files skipped from review as they are similar to previous changes (6)
- third_party/lean/lean_binary.bzl
- third_party/lean/lean_cc_library.bzl
- experiments/leaning/BUILD.bazel
- third_party/lean/lean_toolchain.bzl
- BUILD.bazel
- experiments/leaning/Hello.lean
1 participant
Summary by CodeRabbit
New Features
Chores