From cfeb2e1c236ec77110b3d41b4fccb5d160f76f4b Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 26 Jun 2026 15:47:31 +0000 Subject: [PATCH 1/3] Initial plan From c652482bda5b7b5a57cf5db3426937e7fad8ef43 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 26 Jun 2026 15:58:01 +0000 Subject: [PATCH 2/3] feat(runtimes): add first-class TLA+/TLC runtime support Co-authored-by: jamesadevine <4742697+jamesadevine@users.noreply.github.com> --- docs/runtimes.md | 95 ++++++++++ prompts/create-ado-agentic-workflow.md | 11 +- src/compile/common.rs | 2 + src/compile/extensions/mod.rs | 7 + src/compile/standalone.rs | 2 + src/compile/types.rs | 11 ++ src/runtimes/mod.rs | 1 + src/runtimes/tla/extension.rs | 238 +++++++++++++++++++++++++ src/runtimes/tla/mod.rs | 198 ++++++++++++++++++++ 9 files changed, 563 insertions(+), 2 deletions(-) create mode 100644 src/runtimes/tla/extension.rs create mode 100644 src/runtimes/tla/mod.rs diff --git a/docs/runtimes.md b/docs/runtimes.md index f0922108..0588e9db 100644 --- a/docs/runtimes.md +++ b/docs/runtimes.md @@ -165,6 +165,99 @@ When enabled, the compiler: - **`config:` is functional, not a deferred warning.** AWF only overlays files in `$HOME` (e.g., `~/.npmrc` → `/dev/null`); workspace files such as `nuget.config` are preserved inside the agent sandbox, so a checked-in `nuget.config` works today. - **`NuGetAuthenticate@1` requires no `workingFile:` input.** It auto-discovers `nuget.config` files anywhere in the workspace, unlike `npmAuthenticate@0` which needs an explicit path. +### TLA+ (`tla:`) + +TLA+ / TLC formal model-checking runtime. Downloads a JRE from Eclipse Temurin (Adoptium) and `tla2tools.jar` from the TLA+ GitHub releases page, creates convenience shims (`tlc`, `pluscal`, `sany`), adds Java ecosystem domains to the AWF network allowlist, and extends the bash command allow-list. + +TLA+ is a natural complement to the `lean` runtime: **TLC discovers** liveness/safety gaps by exhaustively searching the state space and emitting counterexample traces, while **Lean proves** a fixed design. Agentic workflows that scan codebases for state-machine bugs — finding stuck states, deadlocks, and missing timeouts — are a primary use case. + +```yaml +# Simple enablement (latest tla2tools.jar, JDK 21 LTS) +runtimes: + tla: true + +# With options (pin tla2tools.jar and JDK versions) +runtimes: + tla: + version: "1.8.0" # tla2tools.jar version (omit for latest) + jdk: "21" # JRE major version (default: 21) +``` + +**Fields:** + +| Field | Type | Description | +|-------|------|-------------| +| `version` | string | `tla2tools.jar` version to download from the TLA+ GitHub releases (e.g., `"1.8.0"`, `"1.7.3"`). When omitted, the latest release is downloaded via GitHub's `releases/latest/download/` redirect. | +| `jdk` | string | JRE major version to download from Eclipse Temurin (Adoptium), e.g., `"21"`, `"17"`. Defaults to `"21"` (current LTS). A JRE (not a full JDK) is downloaded since TLC only requires a runtime. | + +When enabled, the compiler: +- Contributes a bash install step to `Declarations::agent_prepare_steps` that: + 1. Downloads a JRE from [Eclipse Temurin (Adoptium)](https://adoptium.net) into `$HOME/.tla/jre/` + 2. Downloads `tla2tools.jar` from [TLA+ GitHub releases](https://github.com/tlaplus/tlaplus/releases) into `$HOME/.tla/` + 3. Creates convenience shims (`tlc`, `pluscal`, `sany`) in `$HOME/.tla/bin/` +- Auto-adds `java`, `tlc`, `pluscal`, `sany` to the bash command allow-list +- Adds Java ecosystem domains to the network allowlist via the `java` ecosystem identifier (covers `api.adoptium.net` and related Temurin endpoints). GitHub is already in the built-in allowlist, so no extra entry is needed for `tla2tools.jar`. +- Mounts `$HOME/.tla` into the AWF container via `--mount` (read-only) so the toolchain is accessible inside the agent sandbox +- Prepends `$HOME/.tla/bin` to `PATH` inside the AWF sandbox +- Sets `TLA_JAR` and `TLA_JAVA_HOME` as pipeline variables so downstream steps can reference the jar and JRE paths +- Appends a prompt supplement informing the agent about TLA+ availability and invocation patterns + +**Shims:** + +| Command | Java main class | Description | +|---------|----------------|-------------| +| `tlc` | `tlc2.TLC` | Run the TLC model checker: `tlc -config M.cfg M.tla` | +| `pluscal` | `pcal.trans` | Translate PlusCal to TLA+: `pluscal -nocfg M.tla` | +| `sany` | `tla2sany.SANY` | Parse and syntax-check a spec: `sany M.tla` | + +You can also invoke the JVM directly: `java -XX:+UseParallelGC -cp "$TLA_JAR" tlc2.TLC -workers auto -config M.cfg M.tla` + +**Environment variables available inside the agent sandbox:** + +| Variable | Value | +|----------|-------| +| `TLA_JAR` | Absolute path to `tla2tools.jar` | +| `TLA_JAVA_HOME` | JRE home directory (`$HOME/.tla/jre`) | + +**Example: TLA+ model-checking workflow** + +```yaml +--- +name: tla-liveness-checker +description: | + Scans the codebase for event-driven state machines, builds TLA+ models, + runs TLC to find liveness gaps, and proposes findings via safe-outputs. +on: + schedule: "weekly on monday" +runtimes: + tla: true +tools: + bash: + - find + - grep + - tlc + - pluscal + - sany + - java +safe-outputs: + create-pull-request: {} + create-work-item: {} +--- + +Scan the repository for state machine implementations (look for enums with +state names, switch/match blocks on state, or explicit state transition maps). + +For each state machine found: +1. Build a TLA+ model in a temp file capturing the states and transitions. +2. Run `pluscal` to translate PlusCal if used, or write TLA+ directly. +3. Run `tlc -config .tla` to check for deadlocks and liveness. +4. If TLC finds a counterexample trace, record the violation. + +If violations are found, propose: +- A draft PR adding the TLA+ models under `formal/` in the repository. +- A work item per liveness gap with the TLC counterexample trace attached. +``` + ### Combining Runtimes Multiple runtimes can be enabled simultaneously: @@ -178,6 +271,8 @@ runtimes: dotnet: version: "8.0.x" lean: true + tla: + version: "1.8.0" ``` All runtime extensions are sorted into `ExtensionPhase::Runtime` and execute before tool extensions (`ExtensionPhase::Tool`), ensuring language toolchains are available before any tools that depend on them. diff --git a/prompts/create-ado-agentic-workflow.md b/prompts/create-ado-agentic-workflow.md index ddd527c9..0433c2dc 100644 --- a/prompts/create-ado-agentic-workflow.md +++ b/prompts/create-ado-agentic-workflow.md @@ -495,6 +495,13 @@ runtimes: # lean: # toolchain: "leanprover/lean4:v4.29.1" # pin a specific version +# TLA+ / TLC formal model checker +runtimes: + tla: true + # tla: + # version: "1.8.0" # pin tla2tools.jar version (omit for latest) + # jdk: "21" # JRE major version (default: 21) + # Python runtimes: python: true @@ -529,7 +536,7 @@ runtimes: version: "8.0.x" ``` -> Each enabled runtime auto-adds its ecosystem's bash commands (e.g., `dotnet`, `python`, `node`, `npm`, `lean`, `lake`) and network domains to the allowlist. See `docs/runtimes.md` for full configuration reference. +> Each enabled runtime auto-adds its ecosystem's bash commands (e.g., `dotnet`, `python`, `node`, `npm`, `lean`, `lake`, `tlc`, `java`) and network domains to the allowlist. See `docs/runtimes.md` for full configuration reference. ### Step 15 — Network (standalone target only) @@ -544,7 +551,7 @@ network: - "evil.example.com" ``` -`allowed` accepts raw domain patterns (wildcards supported) or ecosystem identifiers (`python`, `node`, `rust`, `dotnet`, `lean`) that expand to the full set of package registry domains for that ecosystem. The built-in allowlist includes: Azure DevOps, GitHub, Microsoft identity, Azure services, Application Insights, and MCP-specific endpoints for each enabled server. +`allowed` accepts raw domain patterns (wildcards supported) or ecosystem identifiers (`python`, `node`, `rust`, `dotnet`, `lean`, `java`) that expand to the full set of package registry domains for that ecosystem. The built-in allowlist includes: Azure DevOps, GitHub, Microsoft identity, Azure services, Application Insights, and MCP-specific endpoints for each enabled server. ### Step 16 — Parameters (optional) diff --git a/src/compile/common.rs b/src/compile/common.rs index 5ba09b7e..932fe57b 100644 --- a/src/compile/common.rs +++ b/src/compile/common.rs @@ -3224,6 +3224,7 @@ mod tests { python: None, node: None, dotnet: None, + tla: None, }); let params = engine_args_for(&fm).unwrap(); assert!( @@ -3259,6 +3260,7 @@ mod tests { python: None, node: None, dotnet: None, + tla: None, }); let params = engine_args_for(&fm).unwrap(); assert!( diff --git a/src/compile/extensions/mod.rs b/src/compile/extensions/mod.rs index eb84f326..7b8c1e49 100644 --- a/src/compile/extensions/mod.rs +++ b/src/compile/extensions/mod.rs @@ -571,6 +571,7 @@ pub use crate::runtimes::dotnet::DotnetExtension; pub use crate::runtimes::lean::LeanExtension; pub use crate::runtimes::node::NodeExtension; pub use crate::runtimes::python::PythonExtension; +pub use crate::runtimes::tla::TlaExtension; pub use crate::tools::azure_devops::AzureDevOpsExtension; pub use crate::tools::cache_memory::CacheMemoryExtension; pub use ado_aw_marker::AdoAwMarkerExtension; @@ -600,6 +601,7 @@ extension_enum! { Python(PythonExtension), Node(NodeExtension), Dotnet(DotnetExtension), + Tla(TlaExtension), AzureDevOps(AzureDevOpsExtension), CacheMemory(CacheMemoryExtension), AzureCli(AzureCliExtension), @@ -742,6 +744,11 @@ pub fn collect_extensions(front_matter: &FrontMatter) -> Vec { { extensions.push(Extension::Dotnet(DotnetExtension::new(dotnet.clone()))); } + if let Some(tla) = front_matter.runtimes.as_ref().and_then(|r| r.tla.as_ref()) + && tla.is_enabled() + { + extensions.push(Extension::Tla(TlaExtension::new(tla.clone()))); + } // ── First-party tools (ExtensionPhase::Tool) ── if let Some(tools) = front_matter.tools.as_ref() { diff --git a/src/compile/standalone.rs b/src/compile/standalone.rs index 56afdc41..a8da344e 100644 --- a/src/compile/standalone.rs +++ b/src/compile/standalone.rs @@ -176,6 +176,7 @@ mod tests { python: None, node: None, dotnet: None, + tla: None, }); let exts = super::super::extensions::collect_extensions(&fm); let domains = allowed_domains(&fm, &exts).unwrap(); @@ -201,6 +202,7 @@ mod tests { python: None, node: None, dotnet: None, + tla: None, }); let exts = super::super::extensions::collect_extensions(&fm); let domains = allowed_domains(&fm, &exts).unwrap(); diff --git a/src/compile/types.rs b/src/compile/types.rs index 9a832b92..0d7930f2 100644 --- a/src/compile/types.rs +++ b/src/compile/types.rs @@ -569,6 +569,14 @@ pub struct RuntimesConfig { /// equivalent for selecting a package source. #[serde(default)] pub dotnet: Option, + + /// TLA+ / TLC formal model-checking runtime. + /// Downloads a JRE from Eclipse Temurin (Adoptium) and `tla2tools.jar` + /// from the TLA+ GitHub releases page, creates convenience shims + /// (`tlc`, `pluscal`, `sany`), adds Java ecosystem domains to the AWF + /// network allowlist, and extends the bash command allow-list. + #[serde(default)] + pub tla: Option, } impl SanitizeConfigTrait for RuntimesConfig { @@ -585,6 +593,9 @@ impl SanitizeConfigTrait for RuntimesConfig { if let Some(ref mut dotnet) = self.dotnet { dotnet.sanitize_config_fields(); } + if let Some(ref mut tla) = self.tla { + tla.sanitize_config_fields(); + } } } diff --git a/src/runtimes/mod.rs b/src/runtimes/mod.rs index 17b4e582..b0ae7b94 100644 --- a/src/runtimes/mod.rs +++ b/src/runtimes/mod.rs @@ -13,3 +13,4 @@ pub mod dotnet; pub mod lean; pub mod node; pub mod python; +pub mod tla; diff --git a/src/runtimes/tla/extension.rs b/src/runtimes/tla/extension.rs new file mode 100644 index 00000000..ff8666c9 --- /dev/null +++ b/src/runtimes/tla/extension.rs @@ -0,0 +1,238 @@ +// ─── TLA+ ──────────────────────────────────────────────────────────── + +use super::{TLA_BASH_COMMANDS, TlaRuntimeConfig, generate_tla_install}; +use crate::compile::extensions::{ + AwfMount, AwfMountMode, CompileContext, CompilerExtension, Declarations, ExtensionPhase, +}; +use crate::compile::ir::step::{BashStep, Step}; +use crate::validate; +use anyhow::Result; + +/// TLA+ / TLC runtime extension. +/// +/// Injects: network hosts (`java` ecosystem — covers Adoptium domains), +/// bash commands (`java`, `tlc`, `pluscal`, `sany`), install steps +/// (JRE download + `tla2tools.jar` + shims), AWF mounts (`$HOME/.tla`), +/// PATH prepend (`$HOME/.tla/bin`), and a prompt supplement. +pub struct TlaExtension { + config: TlaRuntimeConfig, +} + +impl TlaExtension { + pub fn new(config: TlaRuntimeConfig) -> Self { + Self { config } + } +} + +impl CompilerExtension for TlaExtension { + fn name(&self) -> &str { + "TLA+" + } + + fn phase(&self) -> ExtensionPhase { + ExtensionPhase::Runtime + } + + /// Returns the TLA+ install step as a [`Step::Bash`] alongside all + /// static signals (hosts, bash commands, prompt supplement, AWF + /// mounts, PATH prepends). + fn declarations(&self, ctx: &CompileContext) -> Result { + let mut warnings = Vec::new(); + + let is_bash_disabled = ctx + .front_matter + .tools + .as_ref() + .and_then(|t| t.bash.as_ref()) + .is_some_and(|cmds| cmds.is_empty()); + + if is_bash_disabled { + warnings.push(format!( + "Agent '{}' has runtimes.tla enabled but tools.bash is empty. \ + TLA+ requires bash access (java, tlc, pluscal, sany commands).", + ctx.agent_name + )); + } + + // Validate version string (reject pipeline injection) + if let Some(version) = self.config.version() { + validate::reject_pipeline_injection(version, "runtimes.tla.version")?; + } + + // Validate jdk string (reject pipeline injection) + if let Some(jdk) = self.config.jdk() { + validate::reject_pipeline_injection(jdk, "runtimes.tla.jdk")?; + } + + Ok(Declarations { + agent_prepare_steps: vec![Step::Bash(tla_install_bash_step(&self.config))], + // The `java` ecosystem identifier expands to all Adoptium/Temurin domains + // (api.adoptium.net etc.). GitHub is already in the built-in allowlist so + // no extra entry is needed for tla2tools.jar. + network_hosts: vec!["java".to_string()], + bash_commands: TLA_BASH_COMMANDS + .iter() + .map(|c| (*c).to_string()) + .collect(), + prompt_supplement: Some( + "\n\ +---\n\ +\n\ +## TLA+ / TLC Formal Model Checking\n\ +\n\ +TLA+ is installed and available. The toolchain includes:\n\ +- `tlc` — run the TLC model checker: `tlc -config M.cfg M.tla`\n\ +- `pluscal` — translate PlusCal to TLA+: `pluscal -nocfg M.tla`\n\ +- `sany` — parse and syntax-check a TLA+ spec: `sany M.tla`\n\ +- `java` — direct JVM access: `java -cp \"$TLA_JAR\" tlc2.TLC ...`\n\ +\n\ +Environment variables available inside the agent sandbox:\n\ +- `TLA_JAR` — absolute path to `tla2tools.jar`\n\ +- `TLA_JAVA_HOME` — JRE home directory\n\ +\n\ +TLA+ spec files use the `.tla` extension; PlusCal sources are embedded in\n\ +`(*--algorithm ... *)` blocks inside `.tla` files.\n" + .to_string(), + ), + awf_mounts: vec![AwfMount::new( + "$HOME/.tla", + "$HOME/.tla", + AwfMountMode::ReadOnly, + )], + awf_path_prepends: vec!["$HOME/.tla/bin".to_string()], + warnings, + ..Declarations::default() + }) + } +} + +/// Build the typed [`BashStep`] for installing the TLA+ toolchain. +fn tla_install_bash_step(config: &TlaRuntimeConfig) -> BashStep { + BashStep::new("Install TLA+ toolchain (JRE + tla2tools.jar)", generate_tla_install(config)) +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::compile::parse_markdown; + + #[test] + fn test_validate_tla_bash_disabled_emits_warning() { + let (fm, _) = + parse_markdown("---\nname: test\ndescription: test\ntools:\n bash: []\n---\n") + .unwrap(); + let ext = TlaExtension::new(TlaRuntimeConfig::Enabled(true)); + let ctx = CompileContext::for_test(&fm); + let warnings = ext.declarations(&ctx).unwrap().warnings; + assert!(!warnings.is_empty()); + assert!(warnings[0].contains("tools.bash is empty")); + } + + /// Locks `declarations()`: must return a single typed `Step::Bash` install + /// step and all static signals (hosts, mounts, PATH prepends, prompt). + #[test] + fn declarations_returns_typed_bash_step_and_static_signals() { + let (fm, _) = parse_markdown("---\nname: t\ndescription: x\n---\n").unwrap(); + let ext = TlaExtension::new(TlaRuntimeConfig::Enabled(true)); + let ctx = CompileContext::for_test(&fm); + let decl = ext.declarations(&ctx).unwrap(); + assert_eq!(decl.agent_prepare_steps.len(), 1); + match &decl.agent_prepare_steps[0] { + Step::Bash(b) => { + assert_eq!(b.display_name, "Install TLA+ toolchain (JRE + tla2tools.jar)"); + assert!(b.script.contains("api.adoptium.net"), "should fetch JRE from Adoptium"); + assert!(b.script.contains("tla2tools.jar"), "should download tla2tools.jar"); + assert!(b.script.contains("tlc2.TLC"), "should create tlc shim"); + assert!(b.script.contains("pcal.trans"), "should create pluscal shim"); + assert!(b.script.contains("tla2sany.SANY"), "should create sany shim"); + } + other => panic!("expected Step::Bash, got {other:?}"), + } + assert_eq!(decl.network_hosts, vec!["java".to_string()]); + assert!(decl.bash_commands.contains(&"tlc".to_string())); + assert!(decl.bash_commands.contains(&"java".to_string())); + assert!(decl.bash_commands.contains(&"pluscal".to_string())); + assert!(decl.bash_commands.contains(&"sany".to_string())); + assert!(decl.prompt_supplement.is_some()); + assert_eq!(decl.awf_mounts.len(), 1); + assert_eq!(decl.awf_path_prepends, vec!["$HOME/.tla/bin".to_string()]); + // Slots TLA+ doesn't contribute to must be empty. + assert!(decl.setup_steps.is_empty()); + assert!(decl.mcpg_servers.is_empty()); + assert!(decl.copilot_allow_tools.is_empty()); + } + + #[test] + fn declarations_uses_default_jdk_and_latest_jar_when_unset() { + let (fm, _) = parse_markdown("---\nname: t\ndescription: x\n---\n").unwrap(); + let ext = TlaExtension::new(TlaRuntimeConfig::Enabled(true)); + let ctx = CompileContext::for_test(&fm); + let decl = ext.declarations(&ctx).unwrap(); + match &decl.agent_prepare_steps[0] { + Step::Bash(b) => { + assert!( + b.script.contains("/latest/21/"), + "default JDK should be 21: {}", + b.script + ); + assert!( + b.script.contains("releases/latest/download/tla2tools.jar"), + "default jar URL should use latest release redirect: {}", + b.script + ); + } + other => panic!("expected Step::Bash, got {other:?}"), + } + } + + #[test] + fn declarations_uses_pinned_versions_when_configured() { + let (fm, _) = parse_markdown( + "---\nname: t\ndescription: x\nruntimes:\n tla:\n version: '1.8.0'\n jdk: '17'\n---\n", + ) + .unwrap(); + let tla = fm.runtimes.as_ref().unwrap().tla.as_ref().unwrap(); + let ext = TlaExtension::new(tla.clone()); + let ctx = CompileContext::for_test(&fm); + let decl = ext.declarations(&ctx).unwrap(); + match &decl.agent_prepare_steps[0] { + Step::Bash(b) => { + assert!( + b.script.contains("/latest/17/"), + "should use JDK 17: {}", + b.script + ); + assert!( + b.script.contains("download/v1.8.0/tla2tools.jar"), + "should use pinned jar version 1.8.0: {}", + b.script + ); + } + other => panic!("expected Step::Bash, got {other:?}"), + } + } + + #[test] + fn declarations_rejects_injection_in_version() { + let (fm, _) = parse_markdown( + "---\nname: t\ndescription: x\nruntimes:\n tla:\n version: '$(SECRET)'\n---\n", + ) + .unwrap(); + let tla = fm.runtimes.as_ref().unwrap().tla.as_ref().unwrap(); + let ext = TlaExtension::new(tla.clone()); + let ctx = CompileContext::for_test(&fm); + assert!(ext.declarations(&ctx).is_err()); + } + + #[test] + fn declarations_rejects_injection_in_jdk() { + let (fm, _) = parse_markdown( + "---\nname: t\ndescription: x\nruntimes:\n tla:\n jdk: '$(SECRET)'\n---\n", + ) + .unwrap(); + let tla = fm.runtimes.as_ref().unwrap().tla.as_ref().unwrap(); + let ext = TlaExtension::new(tla.clone()); + let ctx = CompileContext::for_test(&fm); + assert!(ext.declarations(&ctx).is_err()); + } +} diff --git a/src/runtimes/tla/mod.rs b/src/runtimes/tla/mod.rs new file mode 100644 index 00000000..f1a1c27d --- /dev/null +++ b/src/runtimes/tla/mod.rs @@ -0,0 +1,198 @@ +//! TLA+ / TLC runtime support for the ado-aw compiler. +//! +//! When enabled via `runtimes: tla:`, the compiler auto-installs a JRE from +//! Eclipse Temurin (Adoptium) and the `tla2tools.jar` from the TLA+ GitHub +//! releases page, creates convenience shims (`tlc`, `pluscal`, `sany`), +//! adds Java ecosystem domains to the AWF network allowlist, extends the bash +//! command allow-list, and appends a prompt supplement informing the agent +//! that TLA+ is available. +//! +//! The toolchain is installed into `$HOME/.tla/`, which is mounted read-only +//! into the AWF chroot via the `required_awf_mounts()` mechanism (same pattern +//! as `runtimes: lean` using `$HOME/.elan/`). +//! +//! ## Network requirements +//! +//! - **JRE download**: `api.adoptium.net` — covered by the `java` ecosystem +//! identifier, which is automatically added to the AWF allowlist. +//! - **`tla2tools.jar` download**: GitHub releases — covered by the built-in +//! GitHub allowlist that every pipeline includes by default. +//! +//! ## Shims +//! +//! Three shims are created in `$HOME/.tla/bin/`: +//! - `tlc` — runs `tlc2.TLC` (the model checker) +//! - `pluscal` — runs `pcal.trans` (PlusCal → TLA+ translator) +//! - `sany` — runs `tla2sany.SANY` (the SANY parser) + +pub mod extension; + +pub use extension::TlaExtension; + +use ado_aw_derive::SanitizeConfig; +use serde::Deserialize; + +use crate::sanitize::SanitizeConfig as SanitizeConfigTrait; + +/// TLA+ runtime configuration — accepts both `true` and object formats. +/// +/// Examples: +/// ```yaml +/// # Simple enablement (installs latest tla2tools.jar with JDK 21) +/// runtimes: +/// tla: true +/// +/// # With options (pin versions) +/// runtimes: +/// tla: +/// version: "1.8.0" # tla2tools.jar version; omit for latest +/// jdk: "21" # JRE major version (default 21) +/// ``` +#[derive(Debug, Deserialize, Clone)] +#[serde(untagged)] +pub enum TlaRuntimeConfig { + /// Simple boolean enablement + Enabled(bool), + /// Full configuration with options + WithOptions(TlaOptions), +} + +impl TlaRuntimeConfig { + /// Whether TLA+ is enabled. + pub fn is_enabled(&self) -> bool { + match self { + TlaRuntimeConfig::Enabled(enabled) => *enabled, + TlaRuntimeConfig::WithOptions(_) => true, + } + } + + /// Get the `tla2tools.jar` version override (None = use latest from GitHub). + pub fn version(&self) -> Option<&str> { + match self { + TlaRuntimeConfig::Enabled(_) => None, + TlaRuntimeConfig::WithOptions(opts) => opts.version.as_deref(), + } + } + + /// Get the JDK major version (None = use default of `"21"`). + pub fn jdk(&self) -> Option<&str> { + match self { + TlaRuntimeConfig::Enabled(_) => None, + TlaRuntimeConfig::WithOptions(opts) => opts.jdk.as_deref(), + } + } +} + +impl SanitizeConfigTrait for TlaRuntimeConfig { + fn sanitize_config_fields(&mut self) { + match self { + TlaRuntimeConfig::Enabled(_) => {} + TlaRuntimeConfig::WithOptions(opts) => opts.sanitize_config_fields(), + } + } +} + +/// TLA+ runtime options. +#[derive(Debug, Deserialize, Clone, Default, SanitizeConfig)] +pub struct TlaOptions { + /// `tla2tools.jar` version to download from the TLA+ GitHub releases. + /// + /// Examples: `"1.8.0"`, `"1.7.3"`. + /// + /// When omitted the compiler downloads the latest GitHub release using + /// the `releases/latest/download/` redirect — no explicit version pinning + /// is required for most workflows. + #[serde(default)] + pub version: Option, + + /// JRE/JDK major version to download from Eclipse Temurin (Adoptium). + /// + /// Examples: `"21"`, `"17"`. Defaults to `"21"` (current LTS). + /// + /// The JRE (not a full JDK) is downloaded since TLC only needs a runtime. + #[serde(default)] + pub jdk: Option, +} + +/// Default JRE major version used when `jdk:` is not specified. +pub const DEFAULT_JDK_VERSION: &str = "21"; + +/// Bash commands that the TLA+ runtime adds to the allow-list. +/// +/// - `java` — direct JVM invocation (e.g. `java -cp $TLA_JAR tlc2.TLC`) +/// - `tlc` — convenience shim for running the TLC model checker +/// - `pluscal` — shim for the PlusCal → TLA+ translator +/// - `sany` — shim for the SANY parser / syntax checker +pub const TLA_BASH_COMMANDS: &[&str] = &["java", "tlc", "pluscal", "sany"]; + +/// Generate the TLA+ installation bash script body. +/// +/// Downloads and stages: +/// 1. A JRE from Eclipse Temurin (Adoptium) into `$HOME/.tla/jre/` +/// 2. `tla2tools.jar` from TLA+ GitHub releases into `$HOME/.tla/` +/// 3. Shim scripts (`tlc`, `pluscal`, `sany`) in `$HOME/.tla/bin/` +/// +/// Sets `TLA_JAR` and `TLA_JAVA_HOME` via `##vso[task.setvariable]` so +/// downstream steps can reference the jar and JRE paths. Also prepends +/// `$HOME/.tla/bin` to PATH via `##vso[task.prependpath]`. +pub fn generate_tla_install(config: &TlaRuntimeConfig) -> String { + let jdk_version = config.jdk().unwrap_or(DEFAULT_JDK_VERSION); + let jar_url = match config.version() { + Some(v) => format!( + "https://github.com/tlaplus/tlaplus/releases/download/v{v}/tla2tools.jar" + ), + None => { + "https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar" + .to_string() + } + }; + + format!( + "\ +set -eo pipefail +TLA_HOME=\"$HOME/.tla\" +JRE_DIR=\"$TLA_HOME/jre\" +BIN_DIR=\"$TLA_HOME/bin\" +mkdir -p \"$JRE_DIR\" \"$BIN_DIR\" + +# Download JRE from Eclipse Temurin (Adoptium) +JRE_URL=\"https://api.adoptium.net/v3/binary/latest/{jdk_version}/ga/linux/x64/jre/hotspot/normal/eclipse?project=jdk\" +echo \"Downloading Temurin JRE {jdk_version} from Adoptium...\" +curl -sSfL \"$JRE_URL\" -o \"$TLA_HOME/jre.tgz\" +tar -xzf \"$TLA_HOME/jre.tgz\" -C \"$JRE_DIR\" --strip-components=1 +rm -f \"$TLA_HOME/jre.tgz\" + +# Download tla2tools.jar +echo \"Downloading tla2tools.jar...\" +curl -sSfL \"{jar_url}\" -o \"$TLA_HOME/tla2tools.jar\" + +# Create shim: tlc (TLC model checker) +cat > \"$BIN_DIR/tlc\" << 'TLA_SHIM_EOF' +#!/usr/bin/env bash +exec \"$HOME/.tla/jre/bin/java\" -XX:+UseParallelGC -cp \"$HOME/.tla/tla2tools.jar\" tlc2.TLC \"$@\" +TLA_SHIM_EOF + +# Create shim: pluscal (PlusCal -> TLA+ translator) +cat > \"$BIN_DIR/pluscal\" << 'TLA_SHIM_EOF' +#!/usr/bin/env bash +exec \"$HOME/.tla/jre/bin/java\" -cp \"$HOME/.tla/tla2tools.jar\" pcal.trans \"$@\" +TLA_SHIM_EOF + +# Create shim: sany (SANY parser / syntax checker) +cat > \"$BIN_DIR/sany\" << 'TLA_SHIM_EOF' +#!/usr/bin/env bash +exec \"$HOME/.tla/jre/bin/java\" -cp \"$HOME/.tla/tla2tools.jar\" tla2sany.SANY \"$@\" +TLA_SHIM_EOF + +chmod +x \"$BIN_DIR/tlc\" \"$BIN_DIR/pluscal\" \"$BIN_DIR/sany\" + +# Expose environment +echo \"##vso[task.prependpath]$HOME/.tla/bin\" +echo \"##vso[task.setvariable variable=TLA_JAR]$HOME/.tla/tla2tools.jar\" +echo \"##vso[task.setvariable variable=TLA_JAVA_HOME]$HOME/.tla/jre\" +export PATH=\"$HOME/.tla/bin:$PATH\" +\"$HOME/.tla/jre/bin/java\" -version +echo \"TLA+ toolchain ready: $TLA_HOME\"\ +" + ) +} From f5958abd1ce3ac36ee58efa5d3b42225bf7b5989 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 26 Jun 2026 16:19:58 +0000 Subject: [PATCH 3/3] feat(runtimes): use JavaToolInstaller@0 IR task for TLA+ JDK installation MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replace the manual bash curl/tar JRE download from Eclipse Temurin (Adoptium) with the JavaToolInstaller@0 ADO task from the compiler IR (pre-installed mode), mirroring the pattern used by node/python/dotnet runtimes. - TlaExtension.declarations() now emits two prepare steps: 1. Step::Task(JavaToolInstaller@0, PreInstalled) — selects the pre-installed JDK matching runtimes.tla.jdk and sets JAVA_HOME 2. Step::Bash — downloads tla2tools.jar and creates tlc/pluscal/sany shims that delegate to `java` from PATH (set by the preceding task) - Removes the `java` network host (no Adoptium download needed) - Adds $(JAVA_HOME) to AWF mounts and $(JAVA_HOME)/bin to AWF path prepends so `java` is accessible inside the AWF chroot - Replaces TLA_JAVA_HOME pipeline variable with standard JAVA_HOME - Renames generate_tla_install -> generate_tla_tools_install - Updates docs and prompt snippets accordingly Co-authored-by: jamesadevine <4742697+jamesadevine@users.noreply.github.com> --- docs/runtimes.md | 24 ++-- prompts/create-ado-agentic-workflow.md | 4 +- src/runtimes/tla/extension.rs | 161 ++++++++++++++++++------- src/runtimes/tla/mod.rs | 64 +++++----- 4 files changed, 162 insertions(+), 91 deletions(-) diff --git a/docs/runtimes.md b/docs/runtimes.md index 0588e9db..03e399a5 100644 --- a/docs/runtimes.md +++ b/docs/runtimes.md @@ -167,7 +167,7 @@ When enabled, the compiler: ### TLA+ (`tla:`) -TLA+ / TLC formal model-checking runtime. Downloads a JRE from Eclipse Temurin (Adoptium) and `tla2tools.jar` from the TLA+ GitHub releases page, creates convenience shims (`tlc`, `pluscal`, `sany`), adds Java ecosystem domains to the AWF network allowlist, and extends the bash command allow-list. +TLA+ / TLC formal model-checking runtime. Uses `JavaToolInstaller@0` to select a pre-installed JDK and downloads `tla2tools.jar` from the TLA+ GitHub releases page, then creates convenience shims (`tlc`, `pluscal`, `sany`) and extends the bash command allow-list. TLA+ is a natural complement to the `lean` runtime: **TLC discovers** liveness/safety gaps by exhaustively searching the state space and emitting counterexample traces, while **Lean proves** a fixed design. Agentic workflows that scan codebases for state-machine bugs — finding stuck states, deadlocks, and missing timeouts — are a primary use case. @@ -180,7 +180,7 @@ runtimes: runtimes: tla: version: "1.8.0" # tla2tools.jar version (omit for latest) - jdk: "21" # JRE major version (default: 21) + jdk: "21" # JDK major version (default: 21) ``` **Fields:** @@ -188,18 +188,18 @@ runtimes: | Field | Type | Description | |-------|------|-------------| | `version` | string | `tla2tools.jar` version to download from the TLA+ GitHub releases (e.g., `"1.8.0"`, `"1.7.3"`). When omitted, the latest release is downloaded via GitHub's `releases/latest/download/` redirect. | -| `jdk` | string | JRE major version to download from Eclipse Temurin (Adoptium), e.g., `"21"`, `"17"`. Defaults to `"21"` (current LTS). A JRE (not a full JDK) is downloaded since TLC only requires a runtime. | +| `jdk` | string | JDK major version to pass to `JavaToolInstaller@0` (pre-installed on the build agent), e.g., `"21"`, `"17"`. Defaults to `"21"` (current LTS). | When enabled, the compiler: -- Contributes a bash install step to `Declarations::agent_prepare_steps` that: - 1. Downloads a JRE from [Eclipse Temurin (Adoptium)](https://adoptium.net) into `$HOME/.tla/jre/` - 2. Downloads `tla2tools.jar` from [TLA+ GitHub releases](https://github.com/tlaplus/tlaplus/releases) into `$HOME/.tla/` - 3. Creates convenience shims (`tlc`, `pluscal`, `sany`) in `$HOME/.tla/bin/` +- Contributes a `JavaToolInstaller@0` task step (pre-installed mode) that selects the JDK matching `jdk:` and sets `JAVA_HOME` +- Contributes a bash step to `Declarations::agent_prepare_steps` that: + 1. Downloads `tla2tools.jar` from [TLA+ GitHub releases](https://github.com/tlaplus/tlaplus/releases) into `$HOME/.tla/` + 2. Creates convenience shims (`tlc`, `pluscal`, `sany`) in `$HOME/.tla/bin/` that delegate to `java` from PATH - Auto-adds `java`, `tlc`, `pluscal`, `sany` to the bash command allow-list -- Adds Java ecosystem domains to the network allowlist via the `java` ecosystem identifier (covers `api.adoptium.net` and related Temurin endpoints). GitHub is already in the built-in allowlist, so no extra entry is needed for `tla2tools.jar`. -- Mounts `$HOME/.tla` into the AWF container via `--mount` (read-only) so the toolchain is accessible inside the agent sandbox -- Prepends `$HOME/.tla/bin` to `PATH` inside the AWF sandbox -- Sets `TLA_JAR` and `TLA_JAVA_HOME` as pipeline variables so downstream steps can reference the jar and JRE paths +- GitHub is already in the built-in allowlist so no extra network host entry is needed for `tla2tools.jar`. The JDK is provided by `JavaToolInstaller@0` (pre-installed on the build agent) so no additional network access is needed for the JDK either. +- Mounts `$HOME/.tla` and `$(JAVA_HOME)` into the AWF container via `--mount` (read-only) so the toolchain is accessible inside the agent sandbox +- Prepends `$HOME/.tla/bin` and `$(JAVA_HOME)/bin` to `PATH` inside the AWF sandbox +- Sets `TLA_JAR` as a pipeline variable so downstream steps can reference the jar path - Appends a prompt supplement informing the agent about TLA+ availability and invocation patterns **Shims:** @@ -217,7 +217,7 @@ You can also invoke the JVM directly: `java -XX:+UseParallelGC -cp "$TLA_JAR" tl | Variable | Value | |----------|-------| | `TLA_JAR` | Absolute path to `tla2tools.jar` | -| `TLA_JAVA_HOME` | JRE home directory (`$HOME/.tla/jre`) | +| `JAVA_HOME` | JDK home directory (set by `JavaToolInstaller@0`) | **Example: TLA+ model-checking workflow** diff --git a/prompts/create-ado-agentic-workflow.md b/prompts/create-ado-agentic-workflow.md index 0433c2dc..0dc4f57a 100644 --- a/prompts/create-ado-agentic-workflow.md +++ b/prompts/create-ado-agentic-workflow.md @@ -500,7 +500,7 @@ runtimes: tla: true # tla: # version: "1.8.0" # pin tla2tools.jar version (omit for latest) - # jdk: "21" # JRE major version (default: 21) + # jdk: "21" # JDK major version for JavaToolInstaller@0 (default: 21) # Python runtimes: @@ -536,7 +536,7 @@ runtimes: version: "8.0.x" ``` -> Each enabled runtime auto-adds its ecosystem's bash commands (e.g., `dotnet`, `python`, `node`, `npm`, `lean`, `lake`, `tlc`, `java`) and network domains to the allowlist. See `docs/runtimes.md` for full configuration reference. +> Each enabled runtime auto-adds its ecosystem's bash commands (e.g., `dotnet`, `python`, `node`, `npm`, `lean`, `lake`, `tlc`, `java`) and network domains to the allowlist. The `tla:` runtime uses `JavaToolInstaller@0` (pre-installed JDK) and the built-in GitHub allowlist, so it requires no extra network entries. See `docs/runtimes.md` for full configuration reference. ### Step 15 — Network (standalone target only) diff --git a/src/runtimes/tla/extension.rs b/src/runtimes/tla/extension.rs index ff8666c9..1d727b3e 100644 --- a/src/runtimes/tla/extension.rs +++ b/src/runtimes/tla/extension.rs @@ -1,19 +1,27 @@ // ─── TLA+ ──────────────────────────────────────────────────────────── -use super::{TLA_BASH_COMMANDS, TlaRuntimeConfig, generate_tla_install}; +use super::{TLA_BASH_COMMANDS, TlaRuntimeConfig, DEFAULT_JDK_VERSION, generate_tla_tools_install}; use crate::compile::extensions::{ AwfMount, AwfMountMode, CompileContext, CompilerExtension, Declarations, ExtensionPhase, }; use crate::compile::ir::step::{BashStep, Step}; +use crate::compile::ir::tasks::java_tool_installer::{JdkArchitecture, JavaToolInstaller}; use crate::validate; use anyhow::Result; /// TLA+ / TLC runtime extension. /// -/// Injects: network hosts (`java` ecosystem — covers Adoptium domains), -/// bash commands (`java`, `tlc`, `pluscal`, `sany`), install steps -/// (JRE download + `tla2tools.jar` + shims), AWF mounts (`$HOME/.tla`), -/// PATH prepend (`$HOME/.tla/bin`), and a prompt supplement. +/// Injects: bash commands (`java`, `tlc`, `pluscal`, `sany`), a +/// [`JavaToolInstaller@0`] task step (selects the pre-installed JDK and +/// sets `JAVA_HOME`), a bash step that downloads `tla2tools.jar` and +/// creates shims, AWF mounts (`$HOME/.tla` and `$(JAVA_HOME)`), +/// PATH prepends (`$HOME/.tla/bin` and `$(JAVA_HOME)/bin`), and a prompt +/// supplement. +/// +/// GitHub is already in the built-in allowlist so no extra network host +/// entry is needed for the `tla2tools.jar` download. +/// +/// [`JavaToolInstaller@0`]: crate::compile::ir::tasks::java_tool_installer::JavaToolInstaller pub struct TlaExtension { config: TlaRuntimeConfig, } @@ -33,9 +41,12 @@ impl CompilerExtension for TlaExtension { ExtensionPhase::Runtime } - /// Returns the TLA+ install step as a [`Step::Bash`] alongside all - /// static signals (hosts, bash commands, prompt supplement, AWF - /// mounts, PATH prepends). + /// Returns two typed prepare steps and all static signals: + /// + /// 1. [`Step::Task`] — `JavaToolInstaller@0` (`PreInstalled` mode): + /// selects the JDK matching `runtimes.tla.jdk` and sets `JAVA_HOME`. + /// 2. [`Step::Bash`] — downloads `tla2tools.jar` and creates shims + /// (`tlc`, `pluscal`, `sany`) that delegate to `java` from PATH. fn declarations(&self, ctx: &CompileContext) -> Result { let mut warnings = Vec::new(); @@ -65,11 +76,14 @@ impl CompilerExtension for TlaExtension { } Ok(Declarations { - agent_prepare_steps: vec![Step::Bash(tla_install_bash_step(&self.config))], - // The `java` ecosystem identifier expands to all Adoptium/Temurin domains - // (api.adoptium.net etc.). GitHub is already in the built-in allowlist so - // no extra entry is needed for tla2tools.jar. - network_hosts: vec!["java".to_string()], + agent_prepare_steps: vec![ + Step::Task(java_install_task_step(&self.config)), + Step::Bash(tla_tools_bash_step(&self.config)), + ], + // GitHub is already in the built-in allowlist — no extra entry + // is needed for tla2tools.jar. The JDK is provided by + // JavaToolInstaller@0 (pre-installed on the build agent). + network_hosts: vec![], bash_commands: TLA_BASH_COMMANDS .iter() .map(|c| (*c).to_string()) @@ -88,27 +102,44 @@ TLA+ is installed and available. The toolchain includes:\n\ \n\ Environment variables available inside the agent sandbox:\n\ - `TLA_JAR` — absolute path to `tla2tools.jar`\n\ -- `TLA_JAVA_HOME` — JRE home directory\n\ +- `JAVA_HOME` — JDK home directory (set by `JavaToolInstaller@0`)\n\ \n\ TLA+ spec files use the `.tla` extension; PlusCal sources are embedded in\n\ `(*--algorithm ... *)` blocks inside `.tla` files.\n" .to_string(), ), - awf_mounts: vec![AwfMount::new( - "$HOME/.tla", - "$HOME/.tla", - AwfMountMode::ReadOnly, - )], - awf_path_prepends: vec!["$HOME/.tla/bin".to_string()], + awf_mounts: vec![ + AwfMount::new("$HOME/.tla", "$HOME/.tla", AwfMountMode::ReadOnly), + // Mount the JDK installation (path set at runtime by JavaToolInstaller@0) + // into the AWF sandbox so `java` is accessible inside the chroot. + AwfMount::new("$(JAVA_HOME)", "$(JAVA_HOME)", AwfMountMode::ReadOnly), + ], + awf_path_prepends: vec![ + "$HOME/.tla/bin".to_string(), + // JavaToolInstaller@0 sets $(JAVA_HOME); expose its bin/ inside + // the AWF chroot so shims can call `java` directly. + "$(JAVA_HOME)/bin".to_string(), + ], warnings, ..Declarations::default() }) } } -/// Build the typed [`BashStep`] for installing the TLA+ toolchain. -fn tla_install_bash_step(config: &TlaRuntimeConfig) -> BashStep { - BashStep::new("Install TLA+ toolchain (JRE + tla2tools.jar)", generate_tla_install(config)) +/// Build the typed [`crate::compile::ir::step::TaskStep`] for installing the JDK via `JavaToolInstaller@0`. +fn java_install_task_step( + config: &TlaRuntimeConfig, +) -> crate::compile::ir::step::TaskStep { + let jdk_version = config.jdk().unwrap_or(DEFAULT_JDK_VERSION); + JavaToolInstaller::pre_installed(jdk_version, JdkArchitecture::X64).into_step() +} + +/// Build the typed [`BashStep`] for downloading `tla2tools.jar` and creating shims. +fn tla_tools_bash_step(config: &TlaRuntimeConfig) -> BashStep { + BashStep::new( + "Install TLA+ toolchain (tla2tools.jar + shims)", + generate_tla_tools_install(config), + ) } #[cfg(test)] @@ -128,19 +159,43 @@ mod tests { assert!(warnings[0].contains("tools.bash is empty")); } - /// Locks `declarations()`: must return a single typed `Step::Bash` install - /// step and all static signals (hosts, mounts, PATH prepends, prompt). + /// Locks `declarations()`: must return a typed `Step::Task` (`JavaToolInstaller@0`) + /// followed by a `Step::Bash` (tla2tools.jar + shims), plus all static signals + /// (bash commands, mounts, PATH prepends, prompt). #[test] - fn declarations_returns_typed_bash_step_and_static_signals() { + fn declarations_returns_typed_task_then_bash_step_and_static_signals() { let (fm, _) = parse_markdown("---\nname: t\ndescription: x\n---\n").unwrap(); let ext = TlaExtension::new(TlaRuntimeConfig::Enabled(true)); let ctx = CompileContext::for_test(&fm); let decl = ext.declarations(&ctx).unwrap(); - assert_eq!(decl.agent_prepare_steps.len(), 1); + assert_eq!(decl.agent_prepare_steps.len(), 2); + // Step 1: JavaToolInstaller@0 match &decl.agent_prepare_steps[0] { + Step::Task(t) => { + assert_eq!(t.task, "JavaToolInstaller@0"); + assert_eq!( + t.inputs.get("versionSpec").map(String::as_str), + Some("21"), + "default JDK version should be 21" + ); + assert_eq!( + t.inputs.get("jdkSourceOption").map(String::as_str), + Some("PreInstalled") + ); + } + other => panic!("expected Step::Task(JavaToolInstaller@0), got {other:?}"), + } + // Step 2: tla2tools.jar + shims bash step + match &decl.agent_prepare_steps[1] { Step::Bash(b) => { - assert_eq!(b.display_name, "Install TLA+ toolchain (JRE + tla2tools.jar)"); - assert!(b.script.contains("api.adoptium.net"), "should fetch JRE from Adoptium"); + assert_eq!( + b.display_name, + "Install TLA+ toolchain (tla2tools.jar + shims)" + ); + assert!( + !b.script.contains("api.adoptium.net"), + "should NOT fetch JRE from Adoptium (JavaToolInstaller handles it)" + ); assert!(b.script.contains("tla2tools.jar"), "should download tla2tools.jar"); assert!(b.script.contains("tlc2.TLC"), "should create tlc shim"); assert!(b.script.contains("pcal.trans"), "should create pluscal shim"); @@ -148,14 +203,22 @@ mod tests { } other => panic!("expected Step::Bash, got {other:?}"), } - assert_eq!(decl.network_hosts, vec!["java".to_string()]); + assert!( + decl.network_hosts.is_empty(), + "no extra network hosts needed: GitHub is built-in, JDK is pre-installed" + ); assert!(decl.bash_commands.contains(&"tlc".to_string())); assert!(decl.bash_commands.contains(&"java".to_string())); assert!(decl.bash_commands.contains(&"pluscal".to_string())); assert!(decl.bash_commands.contains(&"sany".to_string())); assert!(decl.prompt_supplement.is_some()); - assert_eq!(decl.awf_mounts.len(), 1); - assert_eq!(decl.awf_path_prepends, vec!["$HOME/.tla/bin".to_string()]); + assert_eq!(decl.awf_mounts.len(), 2); + assert_eq!(decl.awf_mounts[0].host_path, "$HOME/.tla"); + assert_eq!(decl.awf_mounts[1].host_path, "$(JAVA_HOME)"); + assert_eq!( + decl.awf_path_prepends, + vec!["$HOME/.tla/bin".to_string(), "$(JAVA_HOME)/bin".to_string()] + ); // Slots TLA+ doesn't contribute to must be empty. assert!(decl.setup_steps.is_empty()); assert!(decl.mcpg_servers.is_empty()); @@ -168,13 +231,20 @@ mod tests { let ext = TlaExtension::new(TlaRuntimeConfig::Enabled(true)); let ctx = CompileContext::for_test(&fm); let decl = ext.declarations(&ctx).unwrap(); + // Step 1: JavaToolInstaller with default JDK version match &decl.agent_prepare_steps[0] { - Step::Bash(b) => { - assert!( - b.script.contains("/latest/21/"), - "default JDK should be 21: {}", - b.script + Step::Task(t) => { + assert_eq!( + t.inputs.get("versionSpec").map(String::as_str), + Some("21"), + "default JDK should be 21" ); + } + other => panic!("expected Step::Task, got {other:?}"), + } + // Step 2: bash step with latest jar URL + match &decl.agent_prepare_steps[1] { + Step::Bash(b) => { assert!( b.script.contains("releases/latest/download/tla2tools.jar"), "default jar URL should use latest release redirect: {}", @@ -195,13 +265,20 @@ mod tests { let ext = TlaExtension::new(tla.clone()); let ctx = CompileContext::for_test(&fm); let decl = ext.declarations(&ctx).unwrap(); + // Step 1: JavaToolInstaller with pinned JDK version match &decl.agent_prepare_steps[0] { - Step::Bash(b) => { - assert!( - b.script.contains("/latest/17/"), - "should use JDK 17: {}", - b.script + Step::Task(t) => { + assert_eq!( + t.inputs.get("versionSpec").map(String::as_str), + Some("17"), + "should use JDK 17" ); + } + other => panic!("expected Step::Task, got {other:?}"), + } + // Step 2: bash step with pinned jar version + match &decl.agent_prepare_steps[1] { + Step::Bash(b) => { assert!( b.script.contains("download/v1.8.0/tla2tools.jar"), "should use pinned jar version 1.8.0: {}", diff --git a/src/runtimes/tla/mod.rs b/src/runtimes/tla/mod.rs index f1a1c27d..2383b389 100644 --- a/src/runtimes/tla/mod.rs +++ b/src/runtimes/tla/mod.rs @@ -1,20 +1,21 @@ //! TLA+ / TLC runtime support for the ado-aw compiler. //! -//! When enabled via `runtimes: tla:`, the compiler auto-installs a JRE from -//! Eclipse Temurin (Adoptium) and the `tla2tools.jar` from the TLA+ GitHub -//! releases page, creates convenience shims (`tlc`, `pluscal`, `sany`), -//! adds Java ecosystem domains to the AWF network allowlist, extends the bash -//! command allow-list, and appends a prompt supplement informing the agent -//! that TLA+ is available. +//! When enabled via `runtimes: tla:`, the compiler emits a +//! [`JavaToolInstaller@0`] task step (selecting a pre-installed JDK) followed +//! by a bash step that downloads `tla2tools.jar` from the TLA+ GitHub releases +//! page and creates convenience shims (`tlc`, `pluscal`, `sany`). //! -//! The toolchain is installed into `$HOME/.tla/`, which is mounted read-only -//! into the AWF chroot via the `required_awf_mounts()` mechanism (same pattern -//! as `runtimes: lean` using `$HOME/.elan/`). +//! [`JavaToolInstaller@0`]: crate::compile::ir::tasks::java_tool_installer::JavaToolInstaller +//! +//! The `tla2tools.jar` and shims are installed into `$HOME/.tla/`, which is +//! mounted read-only into the AWF chroot via the `required_awf_mounts()` +//! mechanism. The JDK itself is mounted via the `$(JAVA_HOME)` pipeline +//! variable that `JavaToolInstaller@0` sets. //! //! ## Network requirements //! -//! - **JRE download**: `api.adoptium.net` — covered by the `java` ecosystem -//! identifier, which is automatically added to the AWF allowlist. +//! - **JDK**: provided by `JavaToolInstaller@0` (pre-installed on the build +//! agent — no network download required). //! - **`tla2tools.jar` download**: GitHub releases — covered by the built-in //! GitHub allowlist that every pipeline includes by default. //! @@ -125,18 +126,22 @@ pub const DEFAULT_JDK_VERSION: &str = "21"; /// - `sany` — shim for the SANY parser / syntax checker pub const TLA_BASH_COMMANDS: &[&str] = &["java", "tlc", "pluscal", "sany"]; -/// Generate the TLA+ installation bash script body. +/// Generate the TLA+ tools installation bash script body. /// /// Downloads and stages: -/// 1. A JRE from Eclipse Temurin (Adoptium) into `$HOME/.tla/jre/` -/// 2. `tla2tools.jar` from TLA+ GitHub releases into `$HOME/.tla/` -/// 3. Shim scripts (`tlc`, `pluscal`, `sany`) in `$HOME/.tla/bin/` +/// 1. `tla2tools.jar` from TLA+ GitHub releases into `$HOME/.tla/` +/// 2. Shim scripts (`tlc`, `pluscal`, `sany`) in `$HOME/.tla/bin/` +/// +/// The JDK is provided by a preceding [`JavaToolInstaller@0`] task step, +/// which sets `JAVA_HOME` and adds it to `PATH`. The shims therefore invoke +/// `java` directly from `PATH`. /// -/// Sets `TLA_JAR` and `TLA_JAVA_HOME` via `##vso[task.setvariable]` so -/// downstream steps can reference the jar and JRE paths. Also prepends -/// `$HOME/.tla/bin` to PATH via `##vso[task.prependpath]`. -pub fn generate_tla_install(config: &TlaRuntimeConfig) -> String { - let jdk_version = config.jdk().unwrap_or(DEFAULT_JDK_VERSION); +/// Sets `TLA_JAR` via `##vso[task.setvariable]` so downstream steps can +/// reference the jar path. Also prepends `$HOME/.tla/bin` to PATH via +/// `##vso[task.prependpath]`. +/// +/// [`JavaToolInstaller@0`]: crate::compile::ir::tasks::java_tool_installer::JavaToolInstaller +pub fn generate_tla_tools_install(config: &TlaRuntimeConfig) -> String { let jar_url = match config.version() { Some(v) => format!( "https://github.com/tlaplus/tlaplus/releases/download/v{v}/tla2tools.jar" @@ -151,16 +156,8 @@ pub fn generate_tla_install(config: &TlaRuntimeConfig) -> String { "\ set -eo pipefail TLA_HOME=\"$HOME/.tla\" -JRE_DIR=\"$TLA_HOME/jre\" BIN_DIR=\"$TLA_HOME/bin\" -mkdir -p \"$JRE_DIR\" \"$BIN_DIR\" - -# Download JRE from Eclipse Temurin (Adoptium) -JRE_URL=\"https://api.adoptium.net/v3/binary/latest/{jdk_version}/ga/linux/x64/jre/hotspot/normal/eclipse?project=jdk\" -echo \"Downloading Temurin JRE {jdk_version} from Adoptium...\" -curl -sSfL \"$JRE_URL\" -o \"$TLA_HOME/jre.tgz\" -tar -xzf \"$TLA_HOME/jre.tgz\" -C \"$JRE_DIR\" --strip-components=1 -rm -f \"$TLA_HOME/jre.tgz\" +mkdir -p \"$TLA_HOME\" \"$BIN_DIR\" # Download tla2tools.jar echo \"Downloading tla2tools.jar...\" @@ -169,19 +166,19 @@ curl -sSfL \"{jar_url}\" -o \"$TLA_HOME/tla2tools.jar\" # Create shim: tlc (TLC model checker) cat > \"$BIN_DIR/tlc\" << 'TLA_SHIM_EOF' #!/usr/bin/env bash -exec \"$HOME/.tla/jre/bin/java\" -XX:+UseParallelGC -cp \"$HOME/.tla/tla2tools.jar\" tlc2.TLC \"$@\" +exec java -XX:+UseParallelGC -cp \"$HOME/.tla/tla2tools.jar\" tlc2.TLC \"$@\" TLA_SHIM_EOF # Create shim: pluscal (PlusCal -> TLA+ translator) cat > \"$BIN_DIR/pluscal\" << 'TLA_SHIM_EOF' #!/usr/bin/env bash -exec \"$HOME/.tla/jre/bin/java\" -cp \"$HOME/.tla/tla2tools.jar\" pcal.trans \"$@\" +exec java -cp \"$HOME/.tla/tla2tools.jar\" pcal.trans \"$@\" TLA_SHIM_EOF # Create shim: sany (SANY parser / syntax checker) cat > \"$BIN_DIR/sany\" << 'TLA_SHIM_EOF' #!/usr/bin/env bash -exec \"$HOME/.tla/jre/bin/java\" -cp \"$HOME/.tla/tla2tools.jar\" tla2sany.SANY \"$@\" +exec java -cp \"$HOME/.tla/tla2tools.jar\" tla2sany.SANY \"$@\" TLA_SHIM_EOF chmod +x \"$BIN_DIR/tlc\" \"$BIN_DIR/pluscal\" \"$BIN_DIR/sany\" @@ -189,9 +186,6 @@ chmod +x \"$BIN_DIR/tlc\" \"$BIN_DIR/pluscal\" \"$BIN_DIR/sany\" # Expose environment echo \"##vso[task.prependpath]$HOME/.tla/bin\" echo \"##vso[task.setvariable variable=TLA_JAR]$HOME/.tla/tla2tools.jar\" -echo \"##vso[task.setvariable variable=TLA_JAVA_HOME]$HOME/.tla/jre\" -export PATH=\"$HOME/.tla/bin:$PATH\" -\"$HOME/.tla/jre/bin/java\" -version echo \"TLA+ toolchain ready: $TLA_HOME\"\ " )