feat(compile): add required_awf_mounts to CompilerExtension for Lean runtime

docs/extending.md

@@ -38,6 +38,7 @@ pub trait CompilerExtension: Send {
     fn prompt_supplement(&self) -> Option<String>;              // Agent prompt markdown
     fn prepare_steps(&self) -> Vec<String>;                    // Pipeline steps (install, etc.)
     fn mcpg_servers(&self, ctx) -> Result<Vec<(String, McpgServerConfig)>>; // MCPG entries
+    fn required_awf_mounts(&self) -> Vec<AwfMount>;            // AWF Docker volume mounts
     fn validate(&self, ctx) -> Result<Vec<String>>;            // Compile-time warnings
 }
 ```

docs/runtimes.md

@@ -28,7 +28,7 @@ When enabled, the compiler:
 - Defaults to the `stable` toolchain; if a `lean-toolchain` file exists in the repo, elan overrides to that version automatically
 - Auto-adds `lean`, `lake`, and `elan` to the bash command allow-list
 - 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)
 - Appends a prompt supplement informing the agent about Lean 4 availability and basic commands
 - Emits a compile-time warning if `tools.bash` is empty (Lean requires bash access)
 

docs/template-markers.md

@@ -365,6 +365,14 @@ Should be replaced with the comma-separated domain list for AWF's `--allow-domai
 
 The output is formatted as a comma-separated string (e.g., `github.com,*.dev.azure.com,api.github.com`).
 
+## {{ awf_mounts }}
+
+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).
+
+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.
+
+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.
+
 ## {{ enabled_tools_args }}
 
 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

@@ -1670,6 +1670,36 @@ pub fn generate_allowed_domains(
     Ok(allowlist.join(","))
 }
 
+/// Generate AWF `--mount` flags from extension-declared volume mounts.
+///
+/// Collects `required_awf_mounts()` from all extensions and formats them
+/// as `--mount "spec"` CLI flags for the AWF invocation.
+///
+/// Each mount spec is rendered using its [`Display`][std::fmt::Display] impl
+/// (Docker bind-mount format: `host_path:container_path[:mode]`).
+///
+/// When no extensions require mounts, returns `\` (a bare bash continuation
+/// marker) so the surrounding `\`-continuation chain in the template is
+/// preserved.  When mounts are present, each flag occupies its own line
+/// (`--mount "spec" \`); indentation is handled by [`replace_with_indent`]
+/// at the call site.
+pub fn generate_awf_mounts(extensions: &[super::extensions::Extension]) -> String {
+    let mounts: Vec<super::extensions::AwfMount> = extensions
+        .iter()
+        .flat_map(|ext| ext.required_awf_mounts())
+        .collect();
+
+    if mounts.is_empty() {
+        return "\\".to_string();
+    }
+
+    mounts
+        .iter()
+        .map(|m| format!("--mount \"{}\" \\", m))
+        .collect::<Vec<_>>()
+        .join("\n")
+}
+
 // ==================== Shared compile flow ====================
 
 /// Target-specific overrides for the shared compile flow.
@@ -3719,6 +3749,32 @@ mod tests {
         assert!(result.contains("Lean 4"), "lean prompt present");
     }
 
+    // ─── generate_awf_mounts ──────────────────────────────────────────────
+
+    #[test]
+    fn test_generate_awf_mounts_no_extensions() {
+        let fm = minimal_front_matter();
+        let exts = crate::compile::extensions::collect_extensions(&fm);
+        let result = generate_awf_mounts(&exts);
+        assert_eq!(result, "\\", "no mounts should produce bare continuation");
+    }
+
+    #[test]
+    fn test_generate_awf_mounts_with_lean() {
+        let (fm, _) = parse_markdown(
+            "---\nname: test\ndescription: test\nruntimes:\n  lean: true\n---\n",
+        ).unwrap();
+        let exts = crate::compile::extensions::collect_extensions(&fm);
+        let result = generate_awf_mounts(&exts);
+        assert!(result.contains("--mount"), "should contain --mount flag");
+        assert!(result.contains(".elan"), "should reference .elan directory");
+        assert!(result.contains(":ro"), "should be read-only");
+        // Each mount line ends with ` \` continuation
+        assert!(result.ends_with(" \\"), "last mount should end with continuation");
+        // No embedded indent — replace_with_indent handles indentation
+        assert!(!result.contains("            "), "should not contain hard-coded indent");
+    }
+
     // ═══════════════════════════════════════════════════════════════════════
     // Tests moved from standalone.rs — MCPG config, docker env, validation
     // ═══════════════════════════════════════════════════════════════════════

src/compile/extensions/mod.rs

@@ -17,6 +17,8 @@
 use anyhow::Result;
 use serde::Serialize;
 use std::collections::BTreeMap;
+use std::fmt;
+use std::str::FromStr;
 
 use super::types::FrontMatter;
 
@@ -284,6 +286,147 @@ pub trait CompilerExtension {
     fn required_pipeline_vars(&self) -> Vec<PipelineEnvMapping> {
         vec![]
     }
+
+    /// AWF volume mounts this extension requires inside the chroot.
+    ///
+    /// AWF replaces `$HOME` with an empty directory overlay for security,
+    /// only mounting specific known subdirectories. Extensions that install
+    /// toolchains under `$HOME` (e.g., elan for Lean 4) must declare mounts
+    /// here so the toolchain is accessible inside the chroot.
+    ///
+    /// Shell variables like `$HOME` are expanded at runtime by bash, not at
+    /// compile time. AWF auto-adjusts container paths for chroot by prefixing
+    /// `/host`.
+    fn required_awf_mounts(&self) -> Vec<AwfMount> {
+        vec![]
+    }
+}
+
+/// Mount access mode for an AWF bind mount.
+///
+/// Maps to the Docker bind-mount mode string: `ro` (read-only) or `rw`
+/// (read-write, the Docker default when no mode is specified).
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub enum AwfMountMode {
+    /// Read-only mount (`ro`). The process inside the container cannot write
+    /// to this path.
+    ReadOnly,
+    /// Read-write mount (`rw`). The container can write to this path.
+    ReadWrite,
+}
+
+impl fmt::Display for AwfMountMode {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        match self {
+            Self::ReadOnly => f.write_str("ro"),
+            Self::ReadWrite => f.write_str("rw"),
+        }
+    }
+}
+
+impl FromStr for AwfMountMode {
+    type Err = anyhow::Error;
+
+    fn from_str(s: &str) -> Result<Self, Self::Err> {
+        match s {
+            "ro" => Ok(Self::ReadOnly),
+            "rw" => Ok(Self::ReadWrite),
+            other => anyhow::bail!(
+                "Unknown AWF mount mode '{}': expected 'ro' or 'rw'",
+                other
+            ),
+        }
+    }
+}
+
+impl serde::Serialize for AwfMountMode {
+    fn serialize<S: serde::Serializer>(&self, serializer: S) -> std::result::Result<S::Ok, S::Error> {
+        serializer.serialize_str(&self.to_string())
+    }
+}
+
+impl<'de> serde::Deserialize<'de> for AwfMountMode {
+    fn deserialize<D: serde::Deserializer<'de>>(deserializer: D) -> std::result::Result<Self, D::Error> {
+        let s = String::deserialize(deserializer)?;
+        s.parse().map_err(serde::de::Error::custom)
+    }
+}
+
+/// An AWF `--mount` specification in Docker bind-mount format.
+///
+/// The format is `host_path:container_path[:mode]`
+/// (e.g. `"$HOME/.elan:$HOME/.elan:ro"`).
+///
+/// Serializes and deserializes as the Docker format string so it round-trips
+/// cleanly through YAML/JSON configuration.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub struct AwfMount {
+    /// Host path to bind-mount into the container.
+    pub host_path: String,
+    /// Corresponding path inside the container.
+    pub container_path: String,
+    /// Mount access mode. Defaults to [`AwfMountMode::ReadOnly`] when not
+    /// specified in the input — the secure default for AWF chroot mounts.
+    pub mode: AwfMountMode,
+}
+
+impl AwfMount {
+    /// Creates an `AwfMount` with the given host path, container path, and
+    /// access mode.
+    pub fn new(
+        host_path: impl Into<String>,
+        container_path: impl Into<String>,
+        mode: AwfMountMode,
+    ) -> Self {
+        Self {
+            host_path: host_path.into(),
+            container_path: container_path.into(),
+            mode,
+        }
+    }
+}
+
+impl fmt::Display for AwfMount {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        write!(f, "{}:{}:{}", self.host_path, self.container_path, self.mode)
+    }
+}
+
+impl FromStr for AwfMount {
+    type Err = anyhow::Error;
+
+    fn from_str(s: &str) -> Result<Self, Self::Err> {
+        let parts: Vec<&str> = s.splitn(3, ':').collect();
+        match parts.as_slice() {
+            [host, container] => Ok(Self {
+                host_path: (*host).to_string(),
+                container_path: (*container).to_string(),
+                mode: AwfMountMode::ReadOnly,
+            }),
+            [host, container, mode_str] => Ok(Self {
+                host_path: (*host).to_string(),
+                container_path: (*container).to_string(),
+                mode: mode_str.parse()?,
+            }),
+            _ => anyhow::bail!(
+                "Invalid AWF mount spec '{}': expected 'host:container[:mode]'",
+                s
+            ),
+        }
+    }
+}
+
+impl serde::Serialize for AwfMount {
+    fn serialize<S: serde::Serializer>(&self, serializer: S) -> std::result::Result<S::Ok, S::Error> {
+        serializer.serialize_str(&self.to_string())
+    }
+}
+
+impl<'de> serde::Deserialize<'de> for AwfMount {
+    fn deserialize<D: serde::Deserializer<'de>>(deserializer: D) -> std::result::Result<Self, D::Error> {
+        let s = String::deserialize(deserializer)?;
+        s.parse().map_err(serde::de::Error::custom)
+    }
 }
 
 /// Maps a container environment variable to a pipeline variable.
@@ -358,6 +501,9 @@ macro_rules! extension_enum {
             fn required_pipeline_vars(&self) -> Vec<PipelineEnvMapping> {
                 match self { $( $Enum::$Variant(e) => e.required_pipeline_vars(), )+ }
             }
+            fn required_awf_mounts(&self) -> Vec<AwfMount> {
+                match self { $( $Enum::$Variant(e) => e.required_awf_mounts(), )+ }
+            }
         }
     };
 }

src/compile/extensions/tests.rs

@@ -12,6 +12,76 @@ fn ctx_from(fm: &FrontMatter) -> CompileContext<'_> {
     CompileContext::for_test(fm)
 }
 
+// ── AwfMount ────────────────────────────────────────────────────
+
+#[test]
+fn test_awf_mount_mode_display() {
+    assert_eq!(AwfMountMode::ReadOnly.to_string(), "ro");
+    assert_eq!(AwfMountMode::ReadWrite.to_string(), "rw");
+}
+
+#[test]
+fn test_awf_mount_mode_parse() {
+    assert_eq!("ro".parse::<AwfMountMode>().unwrap(), AwfMountMode::ReadOnly);
+    assert_eq!("rw".parse::<AwfMountMode>().unwrap(), AwfMountMode::ReadWrite);
+    assert!("invalid".parse::<AwfMountMode>().is_err());
+}
+
+#[test]
+fn test_awf_mount_display_with_mode() {
+    let m = AwfMount::new("$HOME/.elan", "$HOME/.elan", AwfMountMode::ReadOnly);
+    assert_eq!(m.to_string(), "$HOME/.elan:$HOME/.elan:ro");
+}
+
+#[test]
+fn test_awf_mount_display_no_mode() {
+    let m = AwfMount::new("/tmp/foo", "/tmp/foo", AwfMountMode::ReadOnly);
+    assert_eq!(m.to_string(), "/tmp/foo:/tmp/foo:ro");
+}
+
+#[test]
+fn test_awf_mount_parse_with_mode() {
+    let m: AwfMount = "$HOME/.elan:$HOME/.elan:ro".parse().unwrap();
+    assert_eq!(m.host_path, "$HOME/.elan");
+    assert_eq!(m.container_path, "$HOME/.elan");
+    assert_eq!(m.mode, AwfMountMode::ReadOnly);
+}
+
+#[test]
+fn test_awf_mount_parse_rw_mode() {
+    let m: AwfMount = "/tmp/work:/tmp/work:rw".parse().unwrap();
+    assert_eq!(m.mode, AwfMountMode::ReadWrite);
+}
+
+#[test]
+fn test_awf_mount_parse_no_mode() {
+    let m: AwfMount = "/tmp/foo:/tmp/foo".parse().unwrap();
+    assert_eq!(m.host_path, "/tmp/foo");
+    assert_eq!(m.container_path, "/tmp/foo");
+    assert_eq!(m.mode, AwfMountMode::ReadOnly);
+}
+
+#[test]
+fn test_awf_mount_parse_invalid_mode_errors() {
+    let result = "/tmp/foo:/tmp/foo:invalid".parse::<AwfMount>();
+    assert!(result.is_err());
+}
+
+#[test]
+fn test_awf_mount_parse_single_segment_errors() {
+    let result = "elan".parse::<AwfMount>();
+    assert!(result.is_err());
+}
+
+#[test]
+fn test_awf_mount_serde_roundtrip() {
+    let m = AwfMount::new("$HOME/.elan", "$HOME/.elan", AwfMountMode::ReadOnly);
+    let json = serde_json::to_string(&m).unwrap();
+    assert_eq!(json, r#""$HOME/.elan:$HOME/.elan:ro""#);
+    let parsed: AwfMount = serde_json::from_str(&json).unwrap();
+    assert_eq!(parsed, m);
+}
+
 // ── collect_extensions ──────────────────────────────────────────
 
 #[test]
@@ -141,6 +211,24 @@ fn test_lean_prepare_steps() {
     assert!(steps[0].contains("elan-init.sh"));
 }
 
+#[test]
+fn test_lean_required_awf_mounts() {
+    let ext = LeanExtension::new(LeanRuntimeConfig::Enabled(true));
+    let mounts = ext.required_awf_mounts();
+    assert_eq!(mounts.len(), 1);
+    assert_eq!(mounts[0].host_path, "$HOME/.elan");
+    assert_eq!(mounts[0].container_path, "$HOME/.elan");
+    assert_eq!(mounts[0].mode, AwfMountMode::ReadOnly);
+    // Round-trips to Docker format string
+    assert_eq!(mounts[0].to_string(), "$HOME/.elan:$HOME/.elan:ro");
+}
+
+#[test]
+fn test_default_required_awf_mounts_empty() {
+    let ext = GitHubExtension;
+    assert!(ext.required_awf_mounts().is_empty());
+}
+
 #[test]
 fn test_lean_validate_bash_disabled_warning() {
     let (fm, _) =

src/compile/onees.rs

@@ -14,6 +14,7 @@ use super::common::{
     AWF_VERSION, MCPG_VERSION, MCPG_IMAGE, MCPG_PORT, MCPG_DOMAIN,
     CompileConfig, compile_shared,
     generate_allowed_domains,
+    generate_awf_mounts,
     generate_enabled_tools_args,
     generate_mcpg_config, generate_mcpg_docker_env, generate_mcpg_step_env,
     format_steps_yaml_indented,
@@ -49,6 +50,7 @@ impl Compiler for OneESCompiler {
 
         // Generate values shared with standalone that are passed as extra replacements
         let allowed_domains = generate_allowed_domains(front_matter, &extensions)?;
+        let awf_mounts = generate_awf_mounts(&extensions);
         let enabled_tools_args = generate_enabled_tools_args(front_matter);
 
         let mcpg_config = generate_mcpg_config(front_matter, &ctx, &extensions)?;
@@ -72,6 +74,7 @@ impl Compiler for OneESCompiler {
                 ("{{ mcpg_port }}".into(), MCPG_PORT.to_string()),
                 ("{{ mcpg_domain }}".into(), MCPG_DOMAIN.into()),
                 ("{{ allowed_domains }}".into(), allowed_domains),
+                ("{{ awf_mounts }}".into(), awf_mounts),
                 ("{{ enabled_tools_args }}".into(), enabled_tools_args),
                 ("{{ mcpg_config }}".into(), mcpg_config_json),
                 ("{{ mcpg_docker_env }}".into(), mcpg_docker_env),