feat(compile): add awf_path_prepends for chroot PATH injection

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,30 @@ 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"
+    cat > "$AWF_PATH_FILE" << AWF_PATH_EOF
+    $HOME/.elan/bin
+    AWF_PATH_EOF
+    echo "##vso[task.setvariable variable=GITHUB_PATH]$AWF_PATH_FILE"
+  displayName: "Generate GITHUB_PATH file"
+```
+
+The heredoc uses an unquoted delimiter so shell variables like `$HOME` are expanded by bash at write time — AWF reads the file as literal resolved paths and does not perform shell expansion itself.
+
+The `GITHUB_PATH` pipeline variable is also explicitly passed through the AWF step's `env:` block (appended to `{{ engine_env }}`) as `GITHUB_PATH: $(GITHUB_PATH)` for robust environment passthrough.
+
 ## {{ 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,68 @@ 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(awf_paths: &[String]) -> String {
+    if awf_paths.is_empty() {
+        return String::new();
+    }
+
+    let path_lines = awf_paths
+        .iter()
+        .map(|p| format!("    {p}"))
+        .collect::<Vec<_>>()
+        .join("\n");
+
+    format!(
+        "\
+- bash: |
+    AWF_PATH_FILE=\"/tmp/awf-tools/ado-path-entries\"
+    cat > \"$AWF_PATH_FILE\" << AWF_PATH_EOF
+{path_lines}
+    AWF_PATH_EOF
+    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 path prepends exist, returns an empty string.
+pub fn generate_awf_path_env(has_awf_paths: bool) -> String {
+    if !has_awf_paths {
+        return String::new();
+    }
+
+    "GITHUB_PATH: $(GITHUB_PATH)".to_string()
+}
+
+/// Collects `awf_path_prepends()` from all extensions into a single `Vec`.
+pub fn collect_awf_path_prepends(extensions: &[super::extensions::Extension]) -> Vec<String> {
+    extensions
+        .iter()
+        .flat_map(|ext| ext.awf_path_prepends())
+        .collect()
+}
+
 // ==================== Shared compile flow ====================
 
 /// Target-specific overrides for the shared compile flow.
@@ -1719,6 +1781,10 @@ pub struct CompileConfig {
     /// backend probe step) are included in the generated pipeline.
     /// Gated behind `cfg(debug_assertions)` at the CLI level.
     pub debug_pipeline: bool,
+    /// Whether any extension declared AWF path prepends. Used by `compile_shared`
+    /// to append `GITHUB_PATH: $(GITHUB_PATH)` to the engine env block without
+    /// re-collecting path prepends from extensions.
+    pub has_awf_paths: bool,
 }
 
 /// Shared compilation flow used by both standalone and 1ES compilers.
@@ -1826,7 +1892,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(config.has_awf_paths);
+    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 +3847,59 @@ mod tests {
         assert!(!result.contains("            "), "should not contain hard-coded indent");
     }
 
+    // ─── generate_awf_path_step ──────────────────────────────────────────────
+
+    #[test]
+    fn test_generate_awf_path_step_no_paths() {
+        let result = generate_awf_path_step(&[]);
+        assert!(result.is_empty(), "no path prepends should produce empty string");
+    }
+
+    #[test]
+    fn test_generate_awf_path_step_with_lean() {
+        let paths = collect_awf_path_prepends(
+            &crate::compile::extensions::collect_extensions(
+                &parse_markdown("---\nname: test\ndescription: test\nruntimes:\n  lean: true\n---\n").unwrap().0,
+            ),
+        );
+        let result = generate_awf_path_step(&paths);
+        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");
+        assert!(result.contains("AWF_PATH_EOF"), "should use heredoc markers");
+    }
+
+    #[test]
+    fn test_generate_awf_path_step_multi_path_indentation() {
+        let paths = vec![
+            "$HOME/.elan/bin".to_string(),
+            "$HOME/.other-tool/bin".to_string(),
+        ];
+        let result = generate_awf_path_step(&paths);
+        // Every path line must have consistent 4-space indentation
+        for path in &paths {
+            assert!(
+                result.contains(&format!("    {path}")),
+                "path '{path}' should have 4-space indentation"
+            );
+        }
+    }
+
+    // ─── generate_awf_path_env ──────────────────────────────────────────────
+
+    #[test]
+    fn test_generate_awf_path_env_no_paths() {
+        let result = generate_awf_path_env(false);
+        assert!(result.is_empty(), "no path prepends should produce empty string");
+    }
+
+    #[test]
+    fn test_generate_awf_path_env_with_paths() {
+        let result = generate_awf_path_env(true);
+        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,8 @@ use super::common::{
     CompileConfig, compile_shared,
     generate_allowed_domains,
     generate_awf_mounts,
+    generate_awf_path_step,
+    collect_awf_path_prepends,
     generate_enabled_tools_args,
     generate_mcpg_config, generate_mcpg_docker_env, generate_mcpg_step_env,
     format_steps_yaml_indented,
@@ -51,6 +53,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 awf_paths = collect_awf_path_prepends(&extensions);
+        let awf_path_step = generate_awf_path_step(&awf_paths);
         let enabled_tools_args = generate_enabled_tools_args(front_matter);
 
         let mcpg_config = generate_mcpg_config(front_matter, &ctx, &extensions)?;
@@ -75,6 +79,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),
@@ -84,6 +89,7 @@ impl Compiler for OneESCompiler {
             ],
             skip_integrity,
             debug_pipeline,
+            has_awf_paths: !awf_paths.is_empty(),
         };
 
         compile_shared(input_path, output_path, front_matter, markdown_body, &extensions, &ctx, config).await

src/compile/standalone.rs

@@ -17,6 +17,8 @@ use super::common::{
     CompileConfig, compile_shared,
     generate_allowed_domains,
     generate_awf_mounts,
+    generate_awf_path_step,
+    collect_awf_path_prepends,
     generate_enabled_tools_args,
     generate_mcpg_config, generate_mcpg_docker_env, generate_mcpg_step_env,
 };
@@ -52,6 +54,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 awf_paths = collect_awf_path_prepends(&extensions);
+        let awf_path_step = generate_awf_path_step(&awf_paths);
         let enabled_tools_args = generate_enabled_tools_args(front_matter);
 
         let config_obj = generate_mcpg_config(front_matter, &ctx, &extensions)?;
@@ -70,13 +74,15 @@ 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),
                 ("{{ mcpg_step_env }}".into(), mcpg_step_env),
             ],
             skip_integrity,
             debug_pipeline,
+            has_awf_paths: !awf_paths.is_empty(),
         };
 
         compile_shared(input_path, output_path, front_matter, markdown_body, &extensions, &ctx, config).await

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();
 

tests/compiler_tests.rs

@@ -2764,6 +2764,22 @@ Prove theorems and build Lean 4 projects.
         "Compiled output should mount $HOME/.elan into the AWF sandbox"
     );
 
+    // The Lean runtime must inject $HOME/.elan/bin into the AWF chroot PATH via
+    // a dedicated "Generate GITHUB_PATH file" step and explicit GITHUB_PATH env
+    // passthrough on the AWF invocation step.
+    assert!(
+        compiled.contains("Generate GITHUB_PATH file"),
+        "Compiled output should include the Generate GITHUB_PATH file step"
+    );
+    assert!(
+        compiled.contains("$HOME/.elan/bin"),
+        "Compiled output should write $HOME/.elan/bin to the GITHUB_PATH file"
+    );
+    assert!(
+        compiled.contains("GITHUB_PATH: $(GITHUB_PATH)"),
+        "Compiled output should pass GITHUB_PATH through the AWF step env block"
+    );
+
     // Verify no unreplaced {{ markers }} remain
     for line in compiled.lines() {
         let stripped = line.replace("${{", "");