feat(runtimes): add first-class TLA+/TLC runtime support

[Copilot]

Adds runtimes: tla: — a first-class TLA+/TLC runtime mirroring the existing lean, python, node, and dotnet runtimes. Closes the gap for agentic workflows that want to run formal model checking (TLC is the counterpart to Lean: it discovers liveness/safety violations exhaustively rather than proving a fixed design).

What runtimes: tla: does

runtimes:
  tla: true          # latest tla2tools.jar, JDK 21

  # or pin versions:
  tla:
    version: "1.8.0" # tla2tools.jar GitHub release tag
    jdk: "21"        # JDK major version for JavaToolInstaller@0 (default: 21)

• Installs JDK via JavaToolInstaller@0 (pre-installed mode) — selects the JDK matching runtimes.tla.jdk and sets JAVA_HOME
• Installs tla2tools.jar from TLA+ GitHub releases → $HOME/.tla/
• Creates shims tlc (tlc2.TLC), pluscal (pcal.trans), sany (tla2sany.SANY) in $HOME/.tla/bin/ — shims delegate to java from PATH
• Network: GitHub is already in the built-in allowlist; the JDK is pre-installed so no additional network entries needed
• AWF mounts: $HOME/.tla and $(JAVA_HOME) read-only into the AWF sandbox
• AWF PATH: prepends $HOME/.tla/bin and $(JAVA_HOME)/bin inside the AWF chroot
• Bash allow-list: auto-adds java, tlc, pluscal, sany
• Env vars: sets TLA_JAR pipeline variable; JAVA_HOME is set by JavaToolInstaller@0
• Prompt supplement: informs the agent of available commands and invocation patterns

Changes

• src/runtimes/tla/ — new module: TlaRuntimeConfig/TlaOptions config types, generate_tla_tools_install() bash script builder (tla2tools.jar + shims only), TlaExtension implementing CompilerExtension with two prepare steps: Step::Task(JavaToolInstaller@0) + Step::Bash
• src/runtimes/mod.rs — pub mod tla
• src/compile/types.rs — tla field in RuntimesConfig
• src/compile/extensions/mod.rs — Tla(TlaExtension) variant, re-export, collect_extensions wiring
• src/compile/common.rs + standalone.rs — tla: None in existing test RuntimesConfig struct literals
• docs/runtimes.md — full TLA+ section: field reference, shim table, env vars, example model-checking workflow
• prompts/create-ado-agentic-workflow.md — tla: snippet; updated runtime notes

Test plan

cargo test — all 2292 tests pass. TLA+ unit tests cover: default JDK task step (JavaToolInstaller@0 versionSpec "21"), pinned versions, latest jar URL, injection rejection for version: and jdk:, and the bash-disabled warning.

[jamesadevine]

@copilot we should be using JavaToolInstall from the compiler IR. Hook it up to the TLA frontmatter.

[Copilot]

@copilot we should be using JavaToolInstall from the compiler IR. Hook it up to the TLA frontmatter.

Done in the latest commit. TlaExtension.declarations() now emits two steps in order:

1. Step::Task(JavaToolInstaller@0, PreInstalled) — selects the pre-installed JDK matching runtimes.tla.jdk (default "21") and sets JAVA_HOME
2. Step::Bash — downloads tla2tools.jar and creates the tlc/pluscal/sany shims that delegate to java from PATH

The manual Adoptium curl/tar download is removed. Since JavaToolInstaller@0 uses the pre-installed JDK, the java network host entry is no longer needed. The $(JAVA_HOME) ADO macro is added to both the AWF mounts and path prepends so java is accessible inside the AWF chroot.