diff --git a/docs/extending.md b/docs/extending.md index 63709b8e..2ee87b6e 100644 --- a/docs/extending.md +++ b/docs/extending.md @@ -38,6 +38,8 @@ pub trait CompilerExtension: Send { fn prompt_supplement(&self) -> Option; // Agent prompt markdown fn prepare_steps(&self) -> Vec; // Pipeline steps (install, etc.) fn mcpg_servers(&self, ctx) -> Result>; // MCPG entries + fn required_awf_mounts(&self) -> Vec; // AWF Docker volume mounts + fn awf_path_prepends(&self) -> Vec; // Directories to add to chroot PATH fn validate(&self, ctx) -> Result>; // Compile-time warnings } ``` diff --git a/docs/runtimes.md b/docs/runtimes.md index 3c69db09..47d78463 100644 --- a/docs/runtimes.md +++ b/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) diff --git a/docs/template-markers.md b/docs/template-markers.md index 09193a52..296d6b9a 100644 --- a/docs/template-markers.md +++ b/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 ` 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`). diff --git a/src/compile/common.rs b/src/compile/common.rs index 7cb8f0ab..49178a33 100644 --- a/src/compile/common.rs +++ b/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 = 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::>() + .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 = 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::>() + .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 // ═══════════════════════════════════════════════════════════════════════ diff --git a/src/compile/extensions/mod.rs b/src/compile/extensions/mod.rs index bb48ebfd..79de6d3f 100644 --- a/src/compile/extensions/mod.rs +++ b/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 { 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 { + 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 { + 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 { + 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(&self, serializer: S) -> std::result::Result { + serializer.serialize_str(&self.to_string()) + } +} + +impl<'de> serde::Deserialize<'de> for AwfMountMode { + fn deserialize>(deserializer: D) -> std::result::Result { + 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, + container_path: impl Into, + 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 { + 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(&self, serializer: S) -> std::result::Result { + serializer.serialize_str(&self.to_string()) + } +} + +impl<'de> serde::Deserialize<'de> for AwfMount { + fn deserialize>(deserializer: D) -> std::result::Result { + 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 { match self { $( $Enum::$Variant(e) => e.required_pipeline_vars(), )+ } } + fn required_awf_mounts(&self) -> Vec { + match self { $( $Enum::$Variant(e) => e.required_awf_mounts(), )+ } + } + fn awf_path_prepends(&self) -> Vec { + match self { $( $Enum::$Variant(e) => e.awf_path_prepends(), )+ } + } } }; } diff --git a/src/compile/extensions/tests.rs b/src/compile/extensions/tests.rs index a7a87714..903b78d4 100644 --- a/src/compile/extensions/tests.rs +++ b/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::().unwrap(), AwfMountMode::ReadOnly); + assert_eq!("rw".parse::().unwrap(), AwfMountMode::ReadWrite); + assert!("invalid".parse::().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::(); + assert!(result.is_err()); +} + +#[test] +fn test_awf_mount_parse_single_segment_errors() { + let result = "elan".parse::(); + 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,38 @@ 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_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, _) = diff --git a/src/compile/onees.rs b/src/compile/onees.rs index aa898764..f7463f5e 100644 --- a/src/compile/onees.rs +++ b/src/compile/onees.rs @@ -14,6 +14,8 @@ use super::common::{ AWF_VERSION, MCPG_VERSION, MCPG_IMAGE, MCPG_PORT, MCPG_DOMAIN, 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, @@ -49,6 +51,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_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)?; @@ -72,6 +76,8 @@ 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), + ("{{ 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), diff --git a/src/compile/standalone.rs b/src/compile/standalone.rs index bc941fd9..edd17dc1 100644 --- a/src/compile/standalone.rs +++ b/src/compile/standalone.rs @@ -16,6 +16,8 @@ use super::common::{ AWF_VERSION, MCPG_VERSION, MCPG_IMAGE, MCPG_PORT, MCPG_DOMAIN, 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, }; @@ -50,6 +52,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_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)?; @@ -67,6 +71,8 @@ impl Compiler for StandaloneCompiler { ("{{ mcpg_port }}".into(), MCPG_PORT.to_string()), ("{{ 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), diff --git a/src/data/1es-base.yml b/src/data/1es-base.yml index 3545c5f5..7b0af5ca 100644 --- a/src/data/1es-base.yml +++ b/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 @@ -339,6 +341,7 @@ extends: --skip-pull \ --env-all \ --enable-host-access \ + {{ awf_mounts }} --container-workdir "{{ working_directory }}" \ --log-level info \ --proxy-logs-dir "$(Agent.TempDirectory)/staging/logs/firewall" \ diff --git a/src/data/base.yml b/src/data/base.yml index fa6d0848..b3437792 100644 --- a/src/data/base.yml +++ b/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 @@ -310,6 +312,7 @@ jobs: --skip-pull \ --env-all \ --enable-host-access \ + {{ awf_mounts }} --container-workdir "{{ working_directory }}" \ --log-level info \ --proxy-logs-dir "$(Agent.TempDirectory)/staging/logs/firewall" \ diff --git a/src/runtimes/lean/extension.rs b/src/runtimes/lean/extension.rs index f510c19e..e1e0ab10 100644 --- a/src/runtimes/lean/extension.rs +++ b/src/runtimes/lean/extension.rs @@ -1,6 +1,6 @@ // ─── Lean 4 ────────────────────────────────────────────────────────── -use crate::compile::extensions::{CompileContext, CompilerExtension, ExtensionPhase}; +use crate::compile::extensions::{AwfMount, AwfMountMode, CompileContext, CompilerExtension, ExtensionPhase}; use super::{LEAN_BASH_COMMANDS, LeanRuntimeConfig, generate_lean_install}; use anyhow::Result; @@ -56,6 +56,14 @@ the toolchain. Lean files use the `.lean` extension.\n" vec![generate_lean_install(&self.config)] } + fn required_awf_mounts(&self) -> Vec { + vec![AwfMount::new("$HOME/.elan", "$HOME/.elan", AwfMountMode::ReadOnly)] + } + + fn awf_path_prepends(&self) -> Vec { + vec!["$HOME/.elan/bin".to_string()] + } + fn validate(&self, ctx: &CompileContext) -> Result> { let mut warnings = Vec::new(); diff --git a/src/runtimes/lean/mod.rs b/src/runtimes/lean/mod.rs index 9c37e62c..fb070195 100644 --- a/src/runtimes/lean/mod.rs +++ b/src/runtimes/lean/mod.rs @@ -6,7 +6,7 @@ //! supplement informing the agent that Lean is available. //! //! Lean is installed via elan (the Lean toolchain manager) into `$HOME/.elan/bin`, -//! then symlinked into `/tmp/awf-tools/` for AWF chroot compatibility. +//! which is mounted read-only into the AWF chroot via the `required_awf_mounts()` mechanism. pub mod extension; @@ -83,7 +83,10 @@ pub const LEAN_BASH_COMMANDS: &[&str] = &["lean", "lake", "elan"]; /// /// Installs elan (Lean toolchain manager) and the specified toolchain. /// Defaults to "stable" if no toolchain is specified in the front matter. -/// Symlinks lean tools into `/tmp/awf-tools/` for AWF chroot compatibility. +/// +/// AWF chroot access is provided by the `--mount` flag declared via +/// `LeanExtension::required_awf_mounts()`, which mounts `$HOME/.elan` +/// read-only into the container. pub fn generate_lean_install(config: &LeanRuntimeConfig) -> String { let toolchain = config.toolchain().unwrap_or("stable"); let script = format!( @@ -92,16 +95,7 @@ curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolch echo \"##vso[task.prependpath]$HOME/.elan/bin\" export PATH=\"$HOME/.elan/bin:$PATH\" lean --version || echo \"Lean installed via elan\" -lake --version || echo \"Lake installed via elan\" -# Symlink lean tools into /tmp/awf-tools/ so they are accessible -# inside the AWF chroot (AWF mounts /tmp but reconstructs PATH -# from standard system locations, excluding $HOME/.elan/bin). -for cmd in lean lake elan; do - if command -v \"$cmd\" >/dev/null 2>&1; then - ln -sf \"$(command -v \"$cmd\")\" \"/tmp/awf-tools/$cmd\" - fi -done -echo \"Lean tools symlinked to /tmp/awf-tools/\"" +lake --version || echo \"Lake installed via elan\"" ); // Indent each line of the script body by 4 spaces for YAML block scalar let indented: String = script