Skip to content

Commit f6f437b

Browse files
jamesadevineCopilotCopilot
authored
feat(compile): add required_awf_mounts to CompilerExtension for Lean runtime (#354)
* feat(compile): add required_awf_mounts to CompilerExtension for Lean 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> * fix(runtimes): remove symlinks from lean install script 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> * chore: remove accidentally committed file Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> * feat(compile): formalize AwfMount struct, fix mount line placement, remove 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> * feat(compile): replace AwfMount mode string with AwfMountMode enum 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> * refactor(compile): remove indent parameter from generate_awf_mounts 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> * refactor(compile): make AwfMount.mode non-optional 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> * fix(docs): remove stale symlink reference from runtimes.md, add parse 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> --------- Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
1 parent dff681b commit f6f437b

12 files changed

Lines changed: 319 additions & 14 deletions

File tree

docs/extending.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,7 @@ pub trait CompilerExtension: Send {
3838
fn prompt_supplement(&self) -> Option<String>; // Agent prompt markdown
3939
fn prepare_steps(&self) -> Vec<String>; // Pipeline steps (install, etc.)
4040
fn mcpg_servers(&self, ctx) -> Result<Vec<(String, McpgServerConfig)>>; // MCPG entries
41+
fn required_awf_mounts(&self) -> Vec<AwfMount>; // AWF Docker volume mounts
4142
fn validate(&self, ctx) -> Result<Vec<String>>; // Compile-time warnings
4243
}
4344
```

docs/runtimes.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ When enabled, the compiler:
2828
- Defaults to the `stable` toolchain; if a `lean-toolchain` file exists in the repo, elan overrides to that version automatically
2929
- Auto-adds `lean`, `lake`, and `elan` to the bash command allow-list
3030
- Adds Lean-specific domains to the network allowlist: `elan.lean-lang.org`, `leanprover.github.io`, `lean-lang.org`
31-
- Symlinks lean tools into `/tmp/awf-tools/` for AWF chroot compatibility
31+
- 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)
3232
- Appends a prompt supplement informing the agent about Lean 4 availability and basic commands
3333
- Emits a compile-time warning if `tools.bash` is empty (Lean requires bash access)
3434

docs/template-markers.md

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -365,6 +365,14 @@ Should be replaced with the comma-separated domain list for AWF's `--allow-domai
365365

366366
The output is formatted as a comma-separated string (e.g., `github.com,*.dev.azure.com,api.github.com`).
367367

368+
## {{ awf_mounts }}
369+
370+
Replaced with `--mount` flags for the **agent job** AWF invocation only (not the detection job), collected from `CompilerExtension::required_awf_mounts()`. Each extension can declare volume mounts needed inside the AWF chroot as [`AwfMount`][AwfMount] values (e.g., the Lean runtime mounts `$HOME/.elan` so the elan toolchain is accessible).
371+
372+
When no extensions declare mounts, this is replaced with `\` (a bare bash continuation marker) so the surrounding `\`-continuation chain is preserved. When mounts are present, each is formatted as `--mount "spec" \` on its own line; indentation is handled by `replace_with_indent` at the call site.
373+
374+
AWF replaces `$HOME` with an empty directory overlay for security; only explicitly mounted subdirectories are accessible inside the chroot. Shell variables like `$HOME` are expanded at runtime by bash.
375+
368376
## {{ enabled_tools_args }}
369377

370378
Should be replaced with `--enabled-tools <name>` CLI arguments for the SafeOutputs MCP HTTP server. The tool list is derived from `safe-outputs:` front matter keys plus always-on diagnostic tools (`noop`, `missing-data`, `missing-tool`, `report-incomplete`).

src/compile/common.rs

Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1670,6 +1670,36 @@ pub fn generate_allowed_domains(
16701670
Ok(allowlist.join(","))
16711671
}
16721672

1673+
/// Generate AWF `--mount` flags from extension-declared volume mounts.
1674+
///
1675+
/// Collects `required_awf_mounts()` from all extensions and formats them
1676+
/// as `--mount "spec"` CLI flags for the AWF invocation.
1677+
///
1678+
/// Each mount spec is rendered using its [`Display`][std::fmt::Display] impl
1679+
/// (Docker bind-mount format: `host_path:container_path[:mode]`).
1680+
///
1681+
/// When no extensions require mounts, returns `\` (a bare bash continuation
1682+
/// marker) so the surrounding `\`-continuation chain in the template is
1683+
/// preserved. When mounts are present, each flag occupies its own line
1684+
/// (`--mount "spec" \`); indentation is handled by [`replace_with_indent`]
1685+
/// at the call site.
1686+
pub fn generate_awf_mounts(extensions: &[super::extensions::Extension]) -> String {
1687+
let mounts: Vec<super::extensions::AwfMount> = extensions
1688+
.iter()
1689+
.flat_map(|ext| ext.required_awf_mounts())
1690+
.collect();
1691+
1692+
if mounts.is_empty() {
1693+
return "\\".to_string();
1694+
}
1695+
1696+
mounts
1697+
.iter()
1698+
.map(|m| format!("--mount \"{}\" \\", m))
1699+
.collect::<Vec<_>>()
1700+
.join("\n")
1701+
}
1702+
16731703
// ==================== Shared compile flow ====================
16741704

16751705
/// Target-specific overrides for the shared compile flow.
@@ -3719,6 +3749,32 @@ mod tests {
37193749
assert!(result.contains("Lean 4"), "lean prompt present");
37203750
}
37213751

3752+
// ─── generate_awf_mounts ──────────────────────────────────────────────
3753+
3754+
#[test]
3755+
fn test_generate_awf_mounts_no_extensions() {
3756+
let fm = minimal_front_matter();
3757+
let exts = crate::compile::extensions::collect_extensions(&fm);
3758+
let result = generate_awf_mounts(&exts);
3759+
assert_eq!(result, "\\", "no mounts should produce bare continuation");
3760+
}
3761+
3762+
#[test]
3763+
fn test_generate_awf_mounts_with_lean() {
3764+
let (fm, _) = parse_markdown(
3765+
"---\nname: test\ndescription: test\nruntimes:\n lean: true\n---\n",
3766+
).unwrap();
3767+
let exts = crate::compile::extensions::collect_extensions(&fm);
3768+
let result = generate_awf_mounts(&exts);
3769+
assert!(result.contains("--mount"), "should contain --mount flag");
3770+
assert!(result.contains(".elan"), "should reference .elan directory");
3771+
assert!(result.contains(":ro"), "should be read-only");
3772+
// Each mount line ends with ` \` continuation
3773+
assert!(result.ends_with(" \\"), "last mount should end with continuation");
3774+
// No embedded indent — replace_with_indent handles indentation
3775+
assert!(!result.contains(" "), "should not contain hard-coded indent");
3776+
}
3777+
37223778
// ═══════════════════════════════════════════════════════════════════════
37233779
// Tests moved from standalone.rs — MCPG config, docker env, validation
37243780
// ═══════════════════════════════════════════════════════════════════════

src/compile/extensions/mod.rs

Lines changed: 146 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,8 @@
1717
use anyhow::Result;
1818
use serde::Serialize;
1919
use std::collections::BTreeMap;
20+
use std::fmt;
21+
use std::str::FromStr;
2022

2123
use super::types::FrontMatter;
2224

@@ -284,6 +286,147 @@ pub trait CompilerExtension {
284286
fn required_pipeline_vars(&self) -> Vec<PipelineEnvMapping> {
285287
vec![]
286288
}
289+
290+
/// AWF volume mounts this extension requires inside the chroot.
291+
///
292+
/// AWF replaces `$HOME` with an empty directory overlay for security,
293+
/// only mounting specific known subdirectories. Extensions that install
294+
/// toolchains under `$HOME` (e.g., elan for Lean 4) must declare mounts
295+
/// here so the toolchain is accessible inside the chroot.
296+
///
297+
/// Shell variables like `$HOME` are expanded at runtime by bash, not at
298+
/// compile time. AWF auto-adjusts container paths for chroot by prefixing
299+
/// `/host`.
300+
fn required_awf_mounts(&self) -> Vec<AwfMount> {
301+
vec![]
302+
}
303+
}
304+
305+
/// Mount access mode for an AWF bind mount.
306+
///
307+
/// Maps to the Docker bind-mount mode string: `ro` (read-only) or `rw`
308+
/// (read-write, the Docker default when no mode is specified).
309+
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
310+
pub enum AwfMountMode {
311+
/// Read-only mount (`ro`). The process inside the container cannot write
312+
/// to this path.
313+
ReadOnly,
314+
/// Read-write mount (`rw`). The container can write to this path.
315+
ReadWrite,
316+
}
317+
318+
impl fmt::Display for AwfMountMode {
319+
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
320+
match self {
321+
Self::ReadOnly => f.write_str("ro"),
322+
Self::ReadWrite => f.write_str("rw"),
323+
}
324+
}
325+
}
326+
327+
impl FromStr for AwfMountMode {
328+
type Err = anyhow::Error;
329+
330+
fn from_str(s: &str) -> Result<Self, Self::Err> {
331+
match s {
332+
"ro" => Ok(Self::ReadOnly),
333+
"rw" => Ok(Self::ReadWrite),
334+
other => anyhow::bail!(
335+
"Unknown AWF mount mode '{}': expected 'ro' or 'rw'",
336+
other
337+
),
338+
}
339+
}
340+
}
341+
342+
impl serde::Serialize for AwfMountMode {
343+
fn serialize<S: serde::Serializer>(&self, serializer: S) -> std::result::Result<S::Ok, S::Error> {
344+
serializer.serialize_str(&self.to_string())
345+
}
346+
}
347+
348+
impl<'de> serde::Deserialize<'de> for AwfMountMode {
349+
fn deserialize<D: serde::Deserializer<'de>>(deserializer: D) -> std::result::Result<Self, D::Error> {
350+
let s = String::deserialize(deserializer)?;
351+
s.parse().map_err(serde::de::Error::custom)
352+
}
353+
}
354+
355+
/// An AWF `--mount` specification in Docker bind-mount format.
356+
///
357+
/// The format is `host_path:container_path[:mode]`
358+
/// (e.g. `"$HOME/.elan:$HOME/.elan:ro"`).
359+
///
360+
/// Serializes and deserializes as the Docker format string so it round-trips
361+
/// cleanly through YAML/JSON configuration.
362+
#[derive(Debug, Clone, PartialEq, Eq)]
363+
pub struct AwfMount {
364+
/// Host path to bind-mount into the container.
365+
pub host_path: String,
366+
/// Corresponding path inside the container.
367+
pub container_path: String,
368+
/// Mount access mode. Defaults to [`AwfMountMode::ReadOnly`] when not
369+
/// specified in the input — the secure default for AWF chroot mounts.
370+
pub mode: AwfMountMode,
371+
}
372+
373+
impl AwfMount {
374+
/// Creates an `AwfMount` with the given host path, container path, and
375+
/// access mode.
376+
pub fn new(
377+
host_path: impl Into<String>,
378+
container_path: impl Into<String>,
379+
mode: AwfMountMode,
380+
) -> Self {
381+
Self {
382+
host_path: host_path.into(),
383+
container_path: container_path.into(),
384+
mode,
385+
}
386+
}
387+
}
388+
389+
impl fmt::Display for AwfMount {
390+
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
391+
write!(f, "{}:{}:{}", self.host_path, self.container_path, self.mode)
392+
}
393+
}
394+
395+
impl FromStr for AwfMount {
396+
type Err = anyhow::Error;
397+
398+
fn from_str(s: &str) -> Result<Self, Self::Err> {
399+
let parts: Vec<&str> = s.splitn(3, ':').collect();
400+
match parts.as_slice() {
401+
[host, container] => Ok(Self {
402+
host_path: (*host).to_string(),
403+
container_path: (*container).to_string(),
404+
mode: AwfMountMode::ReadOnly,
405+
}),
406+
[host, container, mode_str] => Ok(Self {
407+
host_path: (*host).to_string(),
408+
container_path: (*container).to_string(),
409+
mode: mode_str.parse()?,
410+
}),
411+
_ => anyhow::bail!(
412+
"Invalid AWF mount spec '{}': expected 'host:container[:mode]'",
413+
s
414+
),
415+
}
416+
}
417+
}
418+
419+
impl serde::Serialize for AwfMount {
420+
fn serialize<S: serde::Serializer>(&self, serializer: S) -> std::result::Result<S::Ok, S::Error> {
421+
serializer.serialize_str(&self.to_string())
422+
}
423+
}
424+
425+
impl<'de> serde::Deserialize<'de> for AwfMount {
426+
fn deserialize<D: serde::Deserializer<'de>>(deserializer: D) -> std::result::Result<Self, D::Error> {
427+
let s = String::deserialize(deserializer)?;
428+
s.parse().map_err(serde::de::Error::custom)
429+
}
287430
}
288431

289432
/// Maps a container environment variable to a pipeline variable.
@@ -358,6 +501,9 @@ macro_rules! extension_enum {
358501
fn required_pipeline_vars(&self) -> Vec<PipelineEnvMapping> {
359502
match self { $( $Enum::$Variant(e) => e.required_pipeline_vars(), )+ }
360503
}
504+
fn required_awf_mounts(&self) -> Vec<AwfMount> {
505+
match self { $( $Enum::$Variant(e) => e.required_awf_mounts(), )+ }
506+
}
361507
}
362508
};
363509
}

src/compile/extensions/tests.rs

Lines changed: 88 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,76 @@ fn ctx_from(fm: &FrontMatter) -> CompileContext<'_> {
1212
CompileContext::for_test(fm)
1313
}
1414

15+
// ── AwfMount ────────────────────────────────────────────────────
16+
17+
#[test]
18+
fn test_awf_mount_mode_display() {
19+
assert_eq!(AwfMountMode::ReadOnly.to_string(), "ro");
20+
assert_eq!(AwfMountMode::ReadWrite.to_string(), "rw");
21+
}
22+
23+
#[test]
24+
fn test_awf_mount_mode_parse() {
25+
assert_eq!("ro".parse::<AwfMountMode>().unwrap(), AwfMountMode::ReadOnly);
26+
assert_eq!("rw".parse::<AwfMountMode>().unwrap(), AwfMountMode::ReadWrite);
27+
assert!("invalid".parse::<AwfMountMode>().is_err());
28+
}
29+
30+
#[test]
31+
fn test_awf_mount_display_with_mode() {
32+
let m = AwfMount::new("$HOME/.elan", "$HOME/.elan", AwfMountMode::ReadOnly);
33+
assert_eq!(m.to_string(), "$HOME/.elan:$HOME/.elan:ro");
34+
}
35+
36+
#[test]
37+
fn test_awf_mount_display_no_mode() {
38+
let m = AwfMount::new("/tmp/foo", "/tmp/foo", AwfMountMode::ReadOnly);
39+
assert_eq!(m.to_string(), "/tmp/foo:/tmp/foo:ro");
40+
}
41+
42+
#[test]
43+
fn test_awf_mount_parse_with_mode() {
44+
let m: AwfMount = "$HOME/.elan:$HOME/.elan:ro".parse().unwrap();
45+
assert_eq!(m.host_path, "$HOME/.elan");
46+
assert_eq!(m.container_path, "$HOME/.elan");
47+
assert_eq!(m.mode, AwfMountMode::ReadOnly);
48+
}
49+
50+
#[test]
51+
fn test_awf_mount_parse_rw_mode() {
52+
let m: AwfMount = "/tmp/work:/tmp/work:rw".parse().unwrap();
53+
assert_eq!(m.mode, AwfMountMode::ReadWrite);
54+
}
55+
56+
#[test]
57+
fn test_awf_mount_parse_no_mode() {
58+
let m: AwfMount = "/tmp/foo:/tmp/foo".parse().unwrap();
59+
assert_eq!(m.host_path, "/tmp/foo");
60+
assert_eq!(m.container_path, "/tmp/foo");
61+
assert_eq!(m.mode, AwfMountMode::ReadOnly);
62+
}
63+
64+
#[test]
65+
fn test_awf_mount_parse_invalid_mode_errors() {
66+
let result = "/tmp/foo:/tmp/foo:invalid".parse::<AwfMount>();
67+
assert!(result.is_err());
68+
}
69+
70+
#[test]
71+
fn test_awf_mount_parse_single_segment_errors() {
72+
let result = "elan".parse::<AwfMount>();
73+
assert!(result.is_err());
74+
}
75+
76+
#[test]
77+
fn test_awf_mount_serde_roundtrip() {
78+
let m = AwfMount::new("$HOME/.elan", "$HOME/.elan", AwfMountMode::ReadOnly);
79+
let json = serde_json::to_string(&m).unwrap();
80+
assert_eq!(json, r#""$HOME/.elan:$HOME/.elan:ro""#);
81+
let parsed: AwfMount = serde_json::from_str(&json).unwrap();
82+
assert_eq!(parsed, m);
83+
}
84+
1585
// ── collect_extensions ──────────────────────────────────────────
1686

1787
#[test]
@@ -141,6 +211,24 @@ fn test_lean_prepare_steps() {
141211
assert!(steps[0].contains("elan-init.sh"));
142212
}
143213

214+
#[test]
215+
fn test_lean_required_awf_mounts() {
216+
let ext = LeanExtension::new(LeanRuntimeConfig::Enabled(true));
217+
let mounts = ext.required_awf_mounts();
218+
assert_eq!(mounts.len(), 1);
219+
assert_eq!(mounts[0].host_path, "$HOME/.elan");
220+
assert_eq!(mounts[0].container_path, "$HOME/.elan");
221+
assert_eq!(mounts[0].mode, AwfMountMode::ReadOnly);
222+
// Round-trips to Docker format string
223+
assert_eq!(mounts[0].to_string(), "$HOME/.elan:$HOME/.elan:ro");
224+
}
225+
226+
#[test]
227+
fn test_default_required_awf_mounts_empty() {
228+
let ext = GitHubExtension;
229+
assert!(ext.required_awf_mounts().is_empty());
230+
}
231+
144232
#[test]
145233
fn test_lean_validate_bash_disabled_warning() {
146234
let (fm, _) =

src/compile/onees.rs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ use super::common::{
1414
AWF_VERSION, MCPG_VERSION, MCPG_IMAGE, MCPG_PORT, MCPG_DOMAIN,
1515
CompileConfig, compile_shared,
1616
generate_allowed_domains,
17+
generate_awf_mounts,
1718
generate_enabled_tools_args,
1819
generate_mcpg_config, generate_mcpg_docker_env, generate_mcpg_step_env,
1920
format_steps_yaml_indented,
@@ -49,6 +50,7 @@ impl Compiler for OneESCompiler {
4950

5051
// Generate values shared with standalone that are passed as extra replacements
5152
let allowed_domains = generate_allowed_domains(front_matter, &extensions)?;
53+
let awf_mounts = generate_awf_mounts(&extensions);
5254
let enabled_tools_args = generate_enabled_tools_args(front_matter);
5355

5456
let mcpg_config = generate_mcpg_config(front_matter, &ctx, &extensions)?;
@@ -72,6 +74,7 @@ impl Compiler for OneESCompiler {
7274
("{{ mcpg_port }}".into(), MCPG_PORT.to_string()),
7375
("{{ mcpg_domain }}".into(), MCPG_DOMAIN.into()),
7476
("{{ allowed_domains }}".into(), allowed_domains),
77+
("{{ awf_mounts }}".into(), awf_mounts),
7578
("{{ enabled_tools_args }}".into(), enabled_tools_args),
7679
("{{ mcpg_config }}".into(), mcpg_config_json),
7780
("{{ mcpg_docker_env }}".into(), mcpg_docker_env),

0 commit comments

Comments
 (0)