feat(compile): add awf_path_prepends for chroot PATH injection

docs/extending.md

@@ -38,6 +38,8 @@ 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 awf_path_prepends(&self) -> Vec<String>;                // Directories to add to chroot PATH
     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,32 @@ 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.
+
+## {{ awf_path_step }}
+
+Replaced with a dedicated pipeline step that generates a `GITHUB_PATH` file for AWF chroot PATH discovery. The step is collected from `CompilerExtension::awf_path_prepends()` — each extension can declare directories that should be on PATH inside the AWF chroot (e.g., the Lean runtime declares `$HOME/.elan/bin`).
+
+AWF reads the `$GITHUB_PATH` environment variable (a path to a file) at startup, reads path entries from it (one per line), and merges them into `AWF_HOST_PATH` which becomes the chroot PATH. This bypasses the `sudo` `secure_path` reset that strips custom PATH entries.
+
+When no extensions declare path prepends, this is replaced with an empty string and the step is omitted.
+
+Example generated step (with Lean enabled):
+
+```yaml
+- bash: |
+    AWF_PATH_FILE="/tmp/awf-tools/ado-path-entries"
+    echo "$HOME/.elan/bin" >> "$AWF_PATH_FILE"
+    echo "##vso[task.setvariable variable=GITHUB_PATH]$AWF_PATH_FILE"
+  displayName: "Generate GITHUB_PATH file"
+```
+
 ## {{ 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,77 @@ 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")
+}
+
+/// Generates a dedicated pipeline step that writes a `GITHUB_PATH` file
+/// containing directories collected from `CompilerExtension::awf_path_prepends()`.
+///
+/// AWF reads the `$GITHUB_PATH` environment variable (a path to a file) at
+/// startup and merges its entries into the chroot PATH. This mechanism was
+/// designed for GitHub Actions `setup-*` actions but works identically on
+/// ADO when we compose the file ourselves.
+///
+/// The generated step uses `##vso[task.setvariable]` to set `GITHUB_PATH`
+/// as a pipeline variable visible to subsequent steps (including the AWF
+/// invocation step that runs under `sudo`). This bypasses the `sudo`
+/// `secure_path` reset that strips custom PATH entries.
+///
+/// When no extensions declare path prepends, returns an empty string and
+/// the step is omitted from the pipeline.
+pub fn generate_awf_path_step(extensions: &[super::extensions::Extension]) -> String {
+    let paths: Vec<String> = extensions
+        .iter()
+        .flat_map(|ext| ext.awf_path_prepends())
+        .collect();
+
+    if paths.is_empty() {
+        return String::new();
+    }
+
+    let echo_lines: String = paths
+        .iter()
+        .map(|p| format!("    echo \"{}\" >> \"$AWF_PATH_FILE\"", p))
+        .collect::<Vec<_>>()
+        .join("\n");
+
+    format!(
+        "\
+- bash: |
+    AWF_PATH_FILE=\"/tmp/awf-tools/ado-path-entries\"
+{echo_lines}
+    echo \"##vso[task.setvariable variable=GITHUB_PATH]$AWF_PATH_FILE\"
+  displayName: \"Generate GITHUB_PATH file\""
+    )
+}
+
 // ==================== Shared compile flow ====================
 
 /// Target-specific overrides for the shared compile flow.
@@ -3719,6 +3790,55 @@ 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");
+    }
+
+    // ─── generate_awf_path_step ──────────────────────────────────────────────
+
+    #[test]
+    fn test_generate_awf_path_step_no_extensions() {
+        let fm = minimal_front_matter();
+        let exts = crate::compile::extensions::collect_extensions(&fm);
+        let result = generate_awf_path_step(&exts);
+        assert!(result.is_empty(), "no path prepends should produce empty string");
+    }
+
+    #[test]
+    fn test_generate_awf_path_step_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_path_step(&exts);
+        assert!(result.contains("ado-path-entries"), "should reference path entries file");
+        assert!(result.contains(".elan/bin"), "should include elan bin path");
+        assert!(result.contains("GITHUB_PATH"), "should set GITHUB_PATH variable");
+        assert!(result.contains("displayName"), "should be a complete pipeline step");
+    }
+
     // ═══════════════════════════════════════════════════════════════════════
     // 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,161 @@ 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![]
+    }
+
+    /// Directories to prepend to `PATH` inside the AWF chroot.
+    ///
+    /// Extensions that install toolchains outside standard system paths
+    /// (e.g., elan installs Lean to `$HOME/.elan/bin`) should declare their
+    /// bin directories here. The compiler collects these and generates a
+    /// `GITHUB_PATH` file that AWF reads at startup to merge into the chroot
+    /// PATH — bypassing the `sudo` PATH reset.
+    ///
+    /// Shell variables like `$HOME` are expanded at runtime by bash, not at
+    /// compile time.
+    fn awf_path_prepends(&self) -> Vec<String> {
+        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 +515,12 @@ 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(), )+ }
+            }
+            fn awf_path_prepends(&self) -> Vec<String> {
+                match self { $( $Enum::$Variant(e) => e.awf_path_prepends(), )+ }
+            }
         }
     };
 }