feat(compile): add required_awf_mounts to CompilerExtension for Lean runtime#354
feat(compile): add required_awf_mounts to CompilerExtension for Lean runtime#354jamesadevine merged 8 commits intomainfrom
Conversation
…runtime
AWF replaces $HOME with an empty directory overlay for security,
only mounting specific known subdirectories (.cargo, .rustup, etc.).
The Lean toolchain installed at $HOME/.elan/ was not mounted,
causing lean/lake/elan binaries to be missing inside the chroot.
Add
equired_awf_mounts() to the CompilerExtension trait so
extensions can declare Docker volume mounts needed inside the AWF
chroot. The Lean extension returns $HOME/.elan:C:\Users\devinejames/.elan:ro
to mount the elan toolchain read-only.
The compiler collects mounts from all extensions via
generate_awf_mounts() and injects them as --mount flags on
the AWF invocation through a new {{ awf_mounts }} template
marker in both standalone and 1ES base templates.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
| - Adds Lean-specific domains to the network allowlist: `elan.lean-lang.org`, `leanprover.github.io`, `lean-lang.org` | ||
| - Symlinks lean tools into `/tmp/awf-tools/` for AWF chroot compatibility | ||
| - Mounts `$HOME/.elan` into the AWF container via `--mount` flag so the elan toolchain is accessible inside the chroot (AWF replaces `$HOME` with an empty overlay for security) | ||
| - Symlinks lean tools into `/tmp/awf-tools/` as a defense-in-depth fallback |
There was a problem hiding this comment.
@copilot let's drop the symlinks from the compiler extension. Not necessary.
There was a problem hiding this comment.
Done — removed the symlink loop and the echo "Lean tools symlinked..." line from the install script in e241b35. The module doc comment and generate_lean_install doc were also updated to drop the symlink references.
| --skip-pull \ | ||
| --env-all \ | ||
| --container-workdir "{{ working_directory }}" \ | ||
| {{ awf_mounts }}--container-workdir "{{ working_directory }}" \ |
There was a problem hiding this comment.
@copilot shouldn't awf mounts be on a different line?
There was a problem hiding this comment.
Fixed in 4915eae — {{ awf_mounts }} now expands each mount as its own --mount "spec" \ continuation line (followed by a newline and appropriate indentation), so --container-workdir always starts on its own line.
| --skip-pull \ | ||
| --env-all \ | ||
| --container-workdir "{{ working_directory }}" \ | ||
| {{ awf_mounts }}--container-workdir "{{ working_directory }}" \ |
There was a problem hiding this comment.
@copilot awf mounts is not required for threat detection!
There was a problem hiding this comment.
Removed in 4915eae — {{ awf_mounts }} is now only in the agent job AWF invocation; the detection job in both base.yml and 1es-base.yml no longer has the marker.
Agent-Logs-Url: https://github.com/githubnext/ado-aw/sessions/3352a7f0-905a-491f-a9df-3aefb8ffec4b Co-authored-by: jamesadevine <4742697+jamesadevine@users.noreply.github.com>
| vec![generate_lean_install(&self.config)] | ||
| } | ||
|
|
||
| fn required_awf_mounts(&self) -> Vec<String> { |
There was a problem hiding this comment.
@copilot formaliza this as a struct that can be serialized and deserialized from a docker format string (like this)
There was a problem hiding this comment.
Done in 4915eae — introduced AwfMount struct with Display/FromStr (Docker bind-mount format host:container[:mode]) and custom Serialize/Deserialize that round-trips through the format string. required_awf_mounts() now returns Vec<AwfMount> and LeanExtension uses AwfMount::new("$HOME/.elan", "$HOME/.elan", Some("ro")).
|
Just as a heads up, I was blocked by some firewall rules while working on your feedback. Expand below for details. Warning Firewall rules blocked me from connecting to one or more addresses (expand for details)I tried to connect to the following addresses, but was blocked by firewall rules:
If you need me to access, download, or install something from one of these locations, you can either:
|
🔍 Rust PR ReviewSummary: Core implementation looks solid, but there's an accidentally committed internal file that must be removed, a doc/code discrepancy in the mount formatting, and the Lean integration test doesn't assert the new behavior. Findings🐛 Bugs / Logic Issues
🔒 Security Concerns
✅ What Looks Good
|
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
🔍 Rust PR ReviewSummary: Looks good overall — clean extension pattern, consistent wiring across both targets. One doc/code contradiction to fix before merging. Findings🐛 Bugs / Logic Issues
|
…emove from detection job Agent-Logs-Url: https://github.com/githubnext/ado-aw/sessions/5651c5dd-be03-4f3b-86d5-4f925a895a21 Co-authored-by: jamesadevine <4742697+jamesadevine@users.noreply.github.com>
|
Just as a heads up, I was blocked by some firewall rules while working on your feedback. Expand below for details. Warning Firewall rules blocked me from connecting to one or more addresses (expand for details)I tried to connect to the following addresses, but was blocked by firewall rules:
If you need me to access, download, or install something from one of these locations, you can either:
|
| /// Corresponding path inside the container. | ||
| pub container_path: String, | ||
| /// Optional mount mode (e.g. `"ro"` for read-only, `"rw"` for read-write). | ||
| pub mode: Option<String>, |
There was a problem hiding this comment.
Done in d7f3055 — added AwfMountMode enum with ReadOnly (ro) and ReadWrite (rw) variants, each with Display/FromStr/Serialize/Deserialize. AwfMount.mode is now Option<AwfMountMode> and LeanExtension uses AwfMountMode::ReadOnly. Parsing an unknown mode string now returns a descriptive error.
Agent-Logs-Url: https://github.com/githubnext/ado-aw/sessions/f5e68c33-b3b9-4193-bb1f-fac6137f299f Co-authored-by: jamesadevine <4742697+jamesadevine@users.noreply.github.com>
|
Just as a heads up, I was blocked by some firewall rules while working on your feedback. Expand below for details. Warning Firewall rules blocked me from connecting to one or more addresses (expand for details)I tried to connect to the following addresses, but was blocked by firewall rules:
If you need me to access, download, or install something from one of these locations, you can either:
|
Move {{ awf_mounts }} to its own template line so replace_with_indent
handles indentation automatically. When no mounts exist, emit a bare
bash continuation marker (\) to preserve the surrounding \-chain.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
🔍 Rust PR ReviewSummary: Looks good overall — clean trait design, well-tested, correct bash continuation logic. One documentation bug and one PR description inaccuracy to resolve. Findings🐛 Bugs / Logic Issues
|
Always store an explicit AwfMountMode instead of Option<AwfMountMode>. Parsing 'host:container' without a mode suffix now defaults to ReadOnly (secure default). Display/Serialize always emit the mode suffix so generated AWF flags are self-documenting. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
… test The symlink loop was removed from generate_lean_install() but the doc still referenced it. Also adds a test for single-segment AwfMount parse input to lock the error contract. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
🔍 Rust PR ReviewSummary: Looks good overall — clean trait extension, solid test coverage for new types, and the template/indent wiring is correct. One integration test gap and a PR description inaccuracy are worth addressing. Findings🐛 Bugs / Logic Issues
|
Summary
AWF replaces
$HOMEwith an empty directory overlay for security, only mounting specific known subdirectories (.cargo,.rustup,.npm, etc.). When the Lean runtime is enabled, the toolchain installed at$HOME/.elan/was not mounted into the AWF container, causinglean,lake, andelanbinaries to be missing inside the chroot — regardless of PATH configuration.This PR extends
CompilerExtensionwith a newrequired_awf_mounts()method, following the same pattern asrequired_hosts()→{{ allowed_domains }}. The Lean extension uses this to declare--mount "$HOME/.elan:$HOME/.elan:ro"on the AWF invocation, making the elan toolchain accessible inside the chroot.Changes
New trait method:
required_awf_mounts()src/compile/extensions/mod.rs— Addedrequired_awf_mounts() -> Vec<String>toCompilerExtensionwith empty default, plus macro delegation inextension_enum!--mountformat (host_path:container_path[:mode])Lean runtime implementation
src/runtimes/lean/extension.rs— Returns["$HOME/.elan:$HOME/.elan:ro"]to mount the elan toolchain read-onlysrc/runtimes/lean/mod.rs— Updated comments: mount is now primary mechanism, symlinks are defense-in-depth fallbackGenerator + template wiring
src/compile/common.rs— Newgenerate_awf_mounts()function that collects mounts from all extensions and formats as--mountCLI flagssrc/data/base.yml—{{ awf_mounts }}marker in agent AWF invocationsrc/data/1es-base.yml—{{ awf_mounts }}marker in agent AWF invocationsrc/compile/standalone.rs— Wiresawf_mountsintoextra_replacementssrc/compile/onees.rs— Wiresawf_mountsintoextra_replacementsTests
test_lean_required_awf_mounts,test_default_required_awf_mounts_emptytest_generate_awf_mounts_no_extensions,test_generate_awf_mounts_with_leanDocumentation
docs/extending.md— Addedrequired_awf_mounts()to trait referencedocs/template-markers.md— Documented{{ awf_mounts }}markerdocs/runtimes.md— Updated Lean section to describe AWF mount behaviorHow it works
When Lean is enabled via
runtimes: lean: true, the compiled pipeline's AWF invocation now includes:When no extensions declare mounts, the marker expands to empty (no behavioral change to existing pipelines).