一键在 Manus 中运行任何 Skill

tlaplus-toolbox-eclipse

星标0

分支0

更新时间2026年6月15日 22:10

The Eclipse-RCP-based TLA+ Toolbox IDE - its ~30 OSGi plugins/features, the product definition, the Tycho/Maven build, update sites, Oomph dev setup, and its unmaintained status and JDK limitations. Use when working on or understanding the IDE surface, packaging Toolbox distributables, plugin development, or reproducing Toolbox-specific build/CI issues. For the tools jar build see tlaplus-build-workflow.

安装

用 Codex 或 Claude 帮你安装复制这段 Prompt，粘贴到 Codex、Claude 或其他助手里，让它检查 Skill 页面并帮你完成安装。

在 Manus 中运行

来源

jackfoxy

jackfoxy/foxy-skills

打开 GitHub 仓库查看创作者相关仓库

下载

在 Manus 中运行

TLA+ Toolbox (Eclipse RCP IDE)

The legacy graphical IDE under toolbox/. Currently unmaintained — the maintained GUI is the VS Code extension ([[tlaplus-overview]]). Tool-jar build commands: [[tlaplus-build-workflow]]; this skill owns the Eclipse/Tycho specifics.

Architecture (at a glance)

Eclipse RCP / OSGi: ~30 toolbox/org.lamport.tla.toolbox.* dirs — plugins (core + .tool.tlc, .tool.tlc.ui, .editor.basic, .tool.tla2tex, .tool.prover, .doc, …), features (feature.xml grouping plugins), packaging (.product.product, .p2repository), and tests (*.test/*.uitest). The product definition is toolbox/org.lamport.tla.toolbox.product.product/org.lamport.tla.toolbox.product.product.product (embeds tla2tools.jar). Full plugin/feature inventory + CI detail: references/plugins-and-build.md.

Build (Maven/Tycho)

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

Distributables (per-OS zips): toolbox/org.lamport.tla.toolbox.product.product/target/products/. Requires JDK 11 exactly (newer JDKs break the build — tlaplus/tlaplus#1162), Ant 1.9.8+, Maven 3.9.7+, Git. UI tests need a display → CI runs xvfb-run mvn ... verify on ubuntu.

Develop in Eclipse (Oomph)

general/ide/README.md + TLA.setup drive an Oomph setup: install the Oomph Installer, pick "Eclipse Platform" (pinned to 2020-12 if newer fails), select the "TLA+" GitHub project, let it provision, then open .product.product and launch. ⚠ Running Ant from the CLI while Eclipse is open can cause phantom compile errors — run Ant inside Eclipse or Refresh the project. Steps in the reference.

Known limitations

Unmaintained (prefer VS Code); JDK pinned to 11 for the build; platform-specific packaging quirks.

Validation checklist

mvn install -Dmaven.test.skip=true (JDK 11) from a clean state.
Confirm zips in .../product.product/target/products/.
For UI tests, reproduce CI with xvfb-run mvn ... verify.

References (local)

references/plugins-and-build.md — plugin/feature inventory, Tycho build, CI, Oomph steps
toolbox/org.lamport.tla.toolbox.product.product/org.lamport.tla.toolbox.product.product.product
toolbox/*/{pom.xml,feature.xml,plugin.xml,MANIFEST.MF}
general/ide/README.md, general/ide/TLA.setup
DEVELOPING.md (Toolbox + Eclipse sections), .github/workflows/{pr,main}.yml, root pom.xml

同仓库更多 Skills

同仓库

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-build-workflow

jackfoxy/foxy-skills

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.

2026-06-150

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

name	tlaplus-toolbox-eclipse
description	The Eclipse-RCP-based TLA+ Toolbox IDE - its ~30 OSGi plugins/features, the product definition, the Tycho/Maven build, update sites, Oomph dev setup, and its unmaintained status and JDK limitations. Use when working on or understanding the IDE surface, packaging Toolbox distributables, plugin development, or reproducing Toolbox-specific build/CI issues. For the tools jar build see tlaplus-build-workflow.
user-invocable	true
disable-model-invocation	false

TLA+ Toolbox (Eclipse RCP IDE)

Architecture (at a glance)

Build (Maven/Tycho)

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

Develop in Eclipse (Oomph)

Known limitations

Unmaintained (prefer VS Code); JDK pinned to 11 for the build; platform-specific packaging quirks.

Validation checklist

mvn install -Dmaven.test.skip=true (JDK 11) from a clean state.
Confirm zips in .../product.product/target/products/.
For UI tests, reproduce CI with xvfb-run mvn ... verify.

References (local)

references/plugins-and-build.md — plugin/feature inventory, Tycho build, CI, Oomph steps
toolbox/org.lamport.tla.toolbox.product.product/org.lamport.tla.toolbox.product.product.product
toolbox/*/{pom.xml,feature.xml,plugin.xml,MANIFEST.MF}
general/ide/README.md, general/ide/TLA.setup
DEVELOPING.md (Toolbox + Eclipse sections), .github/workflows/{pr,main}.yml, root pom.xml