Run any Skill in Manus with one click

tlaplus-build-workflow

Stars0

Forks0

UpdatedJune 15, 2026 at 22:10

Build, package, test, and develop the TLA+ tools and Toolbox locally or in CI - Ant targets for tla2tools.jar, Maven/Tycho for the Toolbox, the test-set/test targets, the devcontainer, and the GitHub CI matrix. Use to compile the jar, run the test suite or a single test, set up a dev environment, or understand the CI pipeline. Owns every ant/mvn command line for the pack.

Installation

Install with Codex or Claude Copy this prompt, paste it into Codex, Claude, or another assistant, and let it review the skill page and install it for you.

Run Skill in Manus

Source

jackfoxy

jackfoxy/foxy-skills

View GitHub Repository View Creator Repositories

Download

Run Skill in Manus

Related occupationsSOC

Based on SOC occupation classification

Software DevelopersComputer and Mathematical Occupations·SOC 15-1252

File Explorer

4 files

SKILL.md

readonly

name	tlaplus-build-workflow
description	Build, package, test, and develop the TLA+ tools and Toolbox locally or in CI - Ant targets for tla2tools.jar, Maven/Tycho for the Toolbox, the test-set/test targets, the devcontainer, and the GitHub CI matrix. Use to compile the jar, run the test suite or a single test, set up a dev environment, or understand the CI pipeline. Owns every ant/mvn command line for the pack.
user-invocable	true
disable-model-invocation	false

Build & Test Workflow

Owns every ant/mvn command for the pack. Toolbox specifics: [[tlaplus-toolbox-eclipse]]; contribution process: [[tlaplus-contribution]]. Java 11+ required (CI uses 17 for tools; Toolbox needs JDK 11 — newer JDKs break it).

Build the CLI tools (Ant — primary)

cd tlatools/org.lamport.tlatools
ant -f customBuild.xml info compile compile-test dist    # -> dist/tla2tools.jar (validated, ~4.3 MB)
java -cp dist/tla2tools.jar tlc2.TLC test-model/pcal/Bakery.tla   # smoke test -> "No error has been found."

The output jar is identical in use to a release jar. Full target list, test-selection, the CI pipeline, and the devcontainer are in references/targets-and-ci.md.

Run tests

ant -f customBuild.xml test                       # full suite (all should pass)
ant -f customBuild.xml test -Dtest.halt=true      # stop on first failure (CI default)
ant -f customBuild.xml test-set -Dtest.testcases="tlc2/util/*Vec*"   # subset (validated); QUOTE the glob

Path in -Dtest.testcases is relative to the test/ dir. Reports land in target/surefire-reports/.

Build the Toolbox (Maven/Tycho)

mvn install -Dmaven.test.skip=true   # build Toolbox (from repo root)
mvn verify                           # build + run tests

Distributables: toolbox/org.lamport.tla.toolbox.product.product/target/products/. Needs JDK 11, Ant 1.9.8+, Maven 3.9.7+, Git. Detail: [[tlaplus-toolbox-eclipse]].

CI at a glance

pr.yml (PR validation, 3-OS matrix, JDK 17) and main.yml (master → v1.8.0 pre-release) run the same build/test; pr.yml also enforces a grammar/code sync check (generate then git status must be clean) and an examples-integration job. perf.yml → [[tlaplus-performance]]. Full breakdown: references/targets-and-ci.md.

Validation checklist (clean clone → working jar)

cd tlatools/org.lamport.tlatools && ant -f customBuild.xml info compile compile-test dist
java -cp dist/tla2tools.jar tlc2.TLC test-model/pcal/Bakery.tla → "No error has been found."
ant -f customBuild.xml test-set -Dtest.testcases="tlc2/util/*Vec*" → BUILD SUCCESSFUL.

References (local)

references/targets-and-ci.md — full target list, test-set usage, CI pipeline, devcontainer
DEVELOPING.md, tlatools/org.lamport.tlatools/README.md
tlatools/org.lamport.tlatools/customBuild.xml, root pom.xml, tlatools/org.lamport.tlatools/pom.xml
.github/workflows/{pr,main,perf}.yml, .devcontainer/

More from this repository

same repository

gviz-dot-syntax

jackfoxy/foxy-skills

Complete reference for the Graphviz DOT language — grammar, statements, identifiers, graph/node/edge/subgraph attributes, colors, ports, engines, and lexical edge cases — as accepted by the pure-Hoon %graph-viz renderer.

2026-07-100

gviz-gall-api

jackfoxy/foxy-skills

API reference for the %graph-viz Gall agent — the stateless subscribe-then-poke protocol, %gviz-command/%gviz-result marks, $command/$render-opts/$result/$err/$diag types, the run:lib gate, and the positioned-graph noun.

2026-07-100

gviz-patterns

jackfoxy/foxy-skills

Practical recipes and best practices for %graph-viz — rendering from Hoon, building graphs programmatically, worked diagram templates (org charts, dependency/architecture/state/data-flow/UML), styling and accessibility guidance, performance limits, pitfalls, integration (clay/caching), and debugging with verbose diagnostics.

2026-07-100

tlaplus-overview

jackfoxy/foxy-skills

High-level orientation to the tlaplus/tlaplus repository (TLA+ CLI tools + Eclipse Toolbox IDE), its tool entrypoints, and which sibling skill to use for a given task. Use when first interacting with the TLA+ toolchain repo, deciding between CLI/editor/build paths, or routing to the right tlaplus-* skill. Points to the shared external-link inventory and source-map for the whole pack.

2026-06-170

tlaplus-contribution

jackfoxy/foxy-skills

Follow the tlaplus/tlaplus contribution conventions - engage maintainers early, make surgical diffs, write tests first, split PRs, use commit categorization tags and DCO sign-off. Use before any edit or PR, when authoring tests/docs, or crafting commit messages for this repo. For the mechanics of building/running tests see tlaplus-build-workflow.

2026-06-150

tlaplus-debugging

jackfoxy/foxy-skills

Diagnose and recover from TLA+ failures - parse/level errors, config (.cfg) errors, TLC runtime errors, safety (invariant) and liveness violations, deadlock, and out-of-memory; analyze counterexample traces. Use for any SANY/TLC failure, opaque error, or trace/counterexample work. Owns the TLC/SANY error-code taxonomy for the pack.

2026-06-150

name	tlaplus-build-workflow
description	Build, package, test, and develop the TLA+ tools and Toolbox locally or in CI - Ant targets for tla2tools.jar, Maven/Tycho for the Toolbox, the test-set/test targets, the devcontainer, and the GitHub CI matrix. Use to compile the jar, run the test suite or a single test, set up a dev environment, or understand the CI pipeline. Owns every ant/mvn command line for the pack.
user-invocable	true
disable-model-invocation	false

Build & Test Workflow

Build the CLI tools (Ant — primary)

cd tlatools/org.lamport.tlatools
ant -f customBuild.xml info compile compile-test dist    # -> dist/tla2tools.jar (validated, ~4.3 MB)
java -cp dist/tla2tools.jar tlc2.TLC test-model/pcal/Bakery.tla   # smoke test -> "No error has been found."

The output jar is identical in use to a release jar. Full target list, test-selection, the CI pipeline, and the devcontainer are in references/targets-and-ci.md.

Run tests

ant -f customBuild.xml test                       # full suite (all should pass)
ant -f customBuild.xml test -Dtest.halt=true      # stop on first failure (CI default)
ant -f customBuild.xml test-set -Dtest.testcases="tlc2/util/*Vec*"   # subset (validated); QUOTE the glob

Path in -Dtest.testcases is relative to the test/ dir. Reports land in target/surefire-reports/.

Build the Toolbox (Maven/Tycho)

mvn install -Dmaven.test.skip=true   # build Toolbox (from repo root)
mvn verify                           # build + run tests

Distributables: toolbox/org.lamport.tla.toolbox.product.product/target/products/. Needs JDK 11, Ant 1.9.8+, Maven 3.9.7+, Git. Detail: [[tlaplus-toolbox-eclipse]].

CI at a glance

Validation checklist (clean clone → working jar)

cd tlatools/org.lamport.tlatools && ant -f customBuild.xml info compile compile-test dist
java -cp dist/tla2tools.jar tlc2.TLC test-model/pcal/Bakery.tla → "No error has been found."
ant -f customBuild.xml test-set -Dtest.testcases="tlc2/util/*Vec*" → BUILD SUCCESSFUL.

References (local)

references/targets-and-ci.md — full target list, test-set usage, CI pipeline, devcontainer
DEVELOPING.md, tlatools/org.lamport.tlatools/README.md
tlatools/org.lamport.tlatools/customBuild.xml, root pom.xml, tlatools/org.lamport.tlatools/pom.xml
.github/workflows/{pr,main,perf}.yml, .devcontainer/