Skip to content

feat(compile): add awf_path_prepends for chroot PATH injection#358

Closed
jamesadevine wants to merge 9 commits intomainfrom
feat/awf-mounts-lean-runtime
Closed

feat(compile): add awf_path_prepends for chroot PATH injection#358
jamesadevine wants to merge 9 commits intomainfrom
feat/awf-mounts-lean-runtime

Conversation

@jamesadevine
Copy link
Copy Markdown
Collaborator

Summary

Adds awf_path_prepends() to the CompilerExtension trait so extensions can declare directories that should be on PATH inside the AWF chroot. The Lean runtime uses this to make lean, lake, and elan discoverable without absolute paths.

Problem

After PR #354 added the $HOME/.elan AWF mount, the agent could access Lean binaries at ~/.elan/bin/lean — but lean wasn't on PATH. The agent had to do an extra step (which lean fails → ~/.elan/bin/lean -h works) before it could use Lean.

Root cause: sudo resets PATH via secure_path. AWF reconstructs PATH internally from process.env.PATH (post-sudo, missing elan). On GitHub Actions, AWF reads the $GITHUB_PATH file to recover lost paths, but no equivalent existed for ADO.

Solution

  • New CompilerExtension::awf_path_prepends() trait method — extensions declare bin directories to inject into the chroot PATH
  • LeanExtension returns ["$HOME/.elan/bin"]
  • New generate_awf_path_step() generates a dedicated pipeline step ("Generate GITHUB_PATH file") that writes path entries to a file and sets GITHUB_PATH via ##vso[task.setvariable]
  • AWF natively reads $GITHUB_PATH at startup and merges entries into the chroot PATH

Generated step (when Lean is enabled):

- 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"

Changes

File Change
src/compile/extensions/mod.rs awf_path_prepends() trait method + macro dispatch
src/runtimes/lean/extension.rs Returns ["$HOME/.elan/bin"]
src/compile/common.rs generate_awf_path_step() + tests
src/compile/standalone.rs Wire up replacement
src/compile/onees.rs Wire up replacement
src/data/base.yml {{ awf_path_step }} marker
src/data/1es-base.yml {{ awf_path_step }} marker
src/compile/extensions/tests.rs Trait + Lean tests
docs/extending.md Add method to trait listing
docs/template-markers.md Document {{ awf_path_step }}

Testing

  • All 1012 tests pass
  • Clippy clean (no new warnings)
  • New tests for awf_path_prepends() default + Lean impl, and generate_awf_path_step() with/without Lean

jamesadevine and others added 9 commits April 29, 2026 14:42
…runtime

AWF replaces $HOME with an empty directory overlay for security,
only mounting specific known subdirectories (.cargo, .rustup, etc.).
The Lean toolchain installed at $HOME/.elan/ was not mounted,
causing lean/lake/elan binaries to be missing inside the chroot.

Add 
equired_awf_mounts() to the CompilerExtension trait so
extensions can declare Docker volume mounts needed inside the AWF
chroot. The Lean extension returns $HOME/.elan:C:\Users\devinejames/.elan:ro
to mount the elan toolchain read-only.

The compiler collects mounts from all extensions via
generate_awf_mounts() and injects them as --mount flags on
the AWF invocation through a new {{ awf_mounts }} template
marker in both standalone and 1ES base templates.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Agent-Logs-Url: https://github.com/githubnext/ado-aw/sessions/3352a7f0-905a-491f-a9df-3aefb8ffec4b

Co-authored-by: jamesadevine <4742697+jamesadevine@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…emove from detection job

Agent-Logs-Url: https://github.com/githubnext/ado-aw/sessions/5651c5dd-be03-4f3b-86d5-4f925a895a21

Co-authored-by: jamesadevine <4742697+jamesadevine@users.noreply.github.com>
Move {{ awf_mounts }} to its own template line so replace_with_indent
handles indentation automatically. When no mounts exist, emit a bare
bash continuation marker (\) to preserve the surrounding \-chain.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Always store an explicit AwfMountMode instead of Option<AwfMountMode>.
Parsing 'host:container' without a mode suffix now defaults to ReadOnly
(secure default). Display/Serialize always emit the mode suffix so
generated AWF flags are self-documenting.

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

The symlink loop was removed from generate_lean_install() but the doc
still referenced it. Also adds a test for single-segment AwfMount parse
input to lock the error contract.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…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>
@jamesadevine
Copy link
Copy Markdown
Collaborator Author

Replaced with a clean branch cherry-picked from latest main.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants