원클릭으로 Manus에서 모든 스킬 실행

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 저장소 열기 Creator 저장소 보기

다운로드

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