TLA CLI
=======

Command-line tool providing linting, formatting, and TLC invocation for TLA+ projects.

How to get the binary
---------------------
- Install into your cargo bin dir (recommended): `cargo install --path .` then run `tla ...`
- Or build once and run from the release target: `cargo build --release` then `./target/release/tla ...`
- Future (crates.io): `cargo install tla-cli` — it will still install the binary as `tla` (package name differs from bin name).

Prerequisites (Linux)
---------------------
- Rust (MSRV 1.79+)
- Java runtime (for TLC)
- `tlafmt` formatter: `cargo install tlafmt`
- `tlc` model checker: download `tla2tools.jar` and add a wrapper script on `PATH` (snap `tlaplus` ships only the Toolbox GUI, not `tlc`).

Install tlc (wrapper script, no hardcoded paths)
-----------------------------------------------
```
# inside your project (or any directory)
mkdir -p tools
curl -L -o tools/tla2tools.jar \
  https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar

# generate a wrapper that uses that jar
cargo run -- doctor \
  --write-tlc-wrapper tools/tlc \
  --jar tools/tla2tools.jar

# put it on PATH (add to your shell rc to persist)
export PATH="$PWD/tools:$PATH"

# verify
cargo run -- doctor

# Reminder: keep the tools directory on PATH in future shells (e.g., add the export line to ~/.zshrc).
```

You can also set `TLA_TOOLS_JAR=/path/to/tla2tools.jar` and run:
```
cargo run -- doctor --write-tlc-wrapper /some/bin/tlc
```

Usage
-----
```
# Lint TLA+ files (default .)
tla lint [PATH...]

# JSON diagnostics
tla lint path --json

# Format using tlafmt
tla fmt [PATH...]

# Model check with TLC
tla check --spec MySpec [--cfg MySpec.cfg]

# Environment check (tlafmt/tlc presence, optional wrapper creation)
tla doctor [--write-tlc-wrapper <PATH>] [--jar <tla2tools.jar>]
```

Exit codes: success 0; lint errors or formatter/check failures 1; unexpected internal errors non-zero.

Development & Tests
-------------------
```
cargo fmt
cargo clippy -- -D warnings
cargo test

# Smoke (examples)
tla lint fixtures/ok.tla
tla lint fixtures/unused.tla --json
tla check --spec Minimal   # requires tlc on PATH
```

Notes
-----
- Linting uses Tree-sitter and runs even without tlafmt/tlc installed.
- Formatting and checking require the external tools; doctor helps detect and set them up.
