feat(compile): add awf_path_prepends to CompilerExtension for chroot PATH injection

Add a new CompilerExtension trait method awf_path_prepends() that lets
extensions declare directories to prepend to PATH inside the AWF chroot.

The compiler collects these paths and generates a dedicated pipeline step
(Generate GITHUB_PATH file) that writes them to a file and sets the
GITHUB_PATH env var via ##vso[task.setvariable]. AWF natively reads this
file at startup and merges entries into the chroot PATH, bypassing the
sudo secure_path reset that strips custom PATH entries.

LeanExtension declares \C:\Users\devinejames/.elan/bin so lean, lake, and elan are
discoverable by the agent without requiring absolute paths.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Author: jamesadevine

docs/extending.md

@@ -39,6 +39,7 @@ pub trait CompilerExtension: Send {
     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/template-markers.md

@@ -373,6 +373,24 @@ When no extensions declare mounts, this is replaced with `\` (a bare bash contin
 
 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

@@ -1700,6 +1700,65 @@ pub fn generate_awf_mounts(extensions: &[super::extensions::Extension]) -> Strin
         .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\""
+    )
+}
+
+/// Generates the `env:` block entry that passes `GITHUB_PATH` to the AWF
+/// invocation step.
+///
+/// ADO pipeline variables set via `##vso[task.setvariable]` are auto-mapped
+/// as environment variables in subsequent steps, but we explicitly pass
+/// `GITHUB_PATH` via the `env:` block for clarity and robustness.
+///
+/// When no extensions declare path prepends, returns an empty string.
+pub fn generate_awf_path_env(extensions: &[super::extensions::Extension]) -> String {
+    let has_paths = extensions.iter().any(|ext| !ext.awf_path_prepends().is_empty());
+
+    if !has_paths {
+        return String::new();
+    }
+
+    "GITHUB_PATH: $(GITHUB_PATH)".to_string()
+}
+
 // ==================== Shared compile flow ====================
 
 /// Target-specific overrides for the shared compile flow.
@@ -1826,7 +1885,13 @@ pub async fn compile_shared(
             .and_then(|p| p.read.as_deref()),
         "SC_READ_TOKEN",
     );
-    let engine_env = ctx.engine.env(&front_matter.engine)?;
+    let mut engine_env = ctx.engine.env(&front_matter.engine)?;
+
+    // Append GITHUB_PATH env mapping when extensions declare path prepends
+    let awf_path_env = generate_awf_path_env(extensions);
+    if !awf_path_env.is_empty() {
+        engine_env = format!("{engine_env}\n{awf_path_env}");
+    }
     let engine_log_dir = ctx.engine.log_dir();
     let acquire_write_token = generate_acquire_ado_token(
         front_matter
@@ -3775,6 +3840,49 @@ mod tests {
         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");
+    }
+
+    // ─── generate_awf_path_env ──────────────────────────────────────────────
+
+    #[test]
+    fn test_generate_awf_path_env_no_extensions() {
+        let fm = minimal_front_matter();
+        let exts = crate::compile::extensions::collect_extensions(&fm);
+        let result = generate_awf_path_env(&exts);
+        assert!(result.is_empty(), "no path prepends should produce empty string");
+    }
+
+    #[test]
+    fn test_generate_awf_path_env_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_env(&exts);
+        assert_eq!(result, "GITHUB_PATH: $(GITHUB_PATH)");
+    }
+
     // ═══════════════════════════════════════════════════════════════════════
     // Tests moved from standalone.rs — MCPG config, docker env, validation
     // ═══════════════════════════════════════════════════════════════════════

src/compile/extensions/mod.rs

@@ -300,6 +300,20 @@ pub trait CompilerExtension {
     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.
@@ -504,6 +518,9 @@ macro_rules! extension_enum {
             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(), )+ }
+            }
         }
     };
 }

src/compile/extensions/tests.rs

@@ -229,6 +229,20 @@ fn test_default_required_awf_mounts_empty() {
     assert!(ext.required_awf_mounts().is_empty());
 }
 
+#[test]
+fn test_lean_awf_path_prepends() {
+    let ext = LeanExtension::new(LeanRuntimeConfig::Enabled(true));
+    let paths = ext.awf_path_prepends();
+    assert_eq!(paths.len(), 1);
+    assert_eq!(paths[0], "$HOME/.elan/bin");
+}
+
+#[test]
+fn test_default_awf_path_prepends_empty() {
+    let ext = GitHubExtension;
+    assert!(ext.awf_path_prepends().is_empty());
+}
+
 #[test]
 fn test_lean_validate_bash_disabled_warning() {
     let (fm, _) =

src/compile/onees.rs

@@ -15,6 +15,7 @@ use super::common::{
     CompileConfig, compile_shared,
     generate_allowed_domains,
     generate_awf_mounts,
+    generate_awf_path_step,
     generate_enabled_tools_args,
     generate_mcpg_config, generate_mcpg_docker_env, generate_mcpg_step_env,
     format_steps_yaml_indented,
@@ -51,7 +52,8 @@ 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 awf_path_step = generate_awf_path_step(&extensions);
+        let enabled_tools_args= generate_enabled_tools_args(front_matter);
 
         let mcpg_config = generate_mcpg_config(front_matter, &ctx, &extensions)?;
         let mcpg_config_json = serde_json::to_string_pretty(&mcpg_config)
@@ -75,6 +77,7 @@ impl Compiler for OneESCompiler {
                 ("{{ mcpg_domain }}".into(), MCPG_DOMAIN.into()),
                 ("{{ allowed_domains }}".into(), allowed_domains),
                 ("{{ awf_mounts }}".into(), awf_mounts),
+                ("{{ awf_path_step }}".into(), awf_path_step),
                 ("{{ enabled_tools_args }}".into(), enabled_tools_args),
                 ("{{ mcpg_config }}".into(), mcpg_config_json),
                 ("{{ mcpg_docker_env }}".into(), mcpg_docker_env),

src/compile/standalone.rs

@@ -17,6 +17,7 @@ use super::common::{
     CompileConfig, compile_shared,
     generate_allowed_domains,
     generate_awf_mounts,
+    generate_awf_path_step,
     generate_enabled_tools_args,
     generate_mcpg_config, generate_mcpg_docker_env, generate_mcpg_step_env,
 };
@@ -52,7 +53,8 @@ impl Compiler for StandaloneCompiler {
         // Standalone-specific values
         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 awf_path_step = generate_awf_path_step(&extensions);
+        let enabled_tools_args= generate_enabled_tools_args(front_matter);
 
         let config_obj = generate_mcpg_config(front_matter, &ctx, &extensions)?;
         let mcpg_config_json =
@@ -70,6 +72,7 @@ impl Compiler for StandaloneCompiler {
                 ("{{ mcpg_domain }}".into(), MCPG_DOMAIN.into()),
                 ("{{ allowed_domains }}".into(), allowed_domains),
                 ("{{ awf_mounts }}".into(), awf_mounts),
+                ("{{ awf_path_step }}".into(), awf_path_step),
                 ("{{ enabled_tools_args }}".into(), enabled_tools_args),
                 ("{{ mcpg_config }}".into(), mcpg_config_json),
                 ("{{ mcpg_docker_env }}".into(), mcpg_docker_env),

src/data/1es-base.yml

@@ -172,6 +172,8 @@ extends:
 
                 {{ prepare_steps }}
 
+                {{ awf_path_step }}
+
                 # Start SafeOutputs HTTP server on host (MCPG proxies to it)
                 - bash: |
                     SAFE_OUTPUTS_PORT=8100

src/data/base.yml

@@ -143,6 +143,8 @@ jobs:
 
       {{ prepare_steps }}
 
+      {{ awf_path_step }}
+
       # Start SafeOutputs HTTP server on host (MCPG proxies to it)
       - bash: |
           SAFE_OUTPUTS_PORT=8100

src/runtimes/lean/extension.rs

@@ -60,6 +60,10 @@ the toolchain. Lean files use the `.lean` extension.\n"
         vec![AwfMount::new("$HOME/.elan", "$HOME/.elan", AwfMountMode::ReadOnly)]
     }
 
+    fn awf_path_prepends(&self) -> Vec<String> {
+        vec!["$HOME/.elan/bin".to_string()]
+    }
+
     fn validate(&self, ctx: &CompileContext) -> Result<Vec<String>> {
         let mut warnings = Vec::new();