Skip to content

tla-toolbox@1.7.4: Use stable version, internal java & persist config#16803

Draft
goyalyashpal wants to merge 5 commits into
ScoopInstaller:masterfrom
goyalyashpal:enhance-tla-tool
Draft

tla-toolbox@1.7.4: Use stable version, internal java & persist config#16803
goyalyashpal wants to merge 5 commits into
ScoopInstaller:masterfrom
goyalyashpal:enhance-tla-tool

Conversation

@goyalyashpal

@goyalyashpal goyalyashpal commented Dec 17, 2025

Copy link
Copy Markdown
Contributor

Fix #16802

  • rename manifest file: tla{plus ->}-toolbox.json
  • downgrade to stable version
  • persist the configuration
  • use pre_install script to run the tla2tools.jar with the bundled-in java
  • use the order of fields as specified in the contribution guidelines

Also see:

Please do not squash.

  • Use conventional PR title: <manifest-name[@version]|chore>: <general summary of the pull request>
  • I have read the Contributing Guide

Summary by CodeRabbit

  • New Features

    • Windows installer manifest added, enabling native installation, bundled launcher and a "TLA+ Toolbox" shortcut.
  • Improvements

    • Configuration now persists across runs.
    • Integrated GitHub-based version checking and auto-update for smoother updates.
  • Notes

    • Includes a known-issue reminder, suggested auxiliary tools, and installation guidance.

✏️ Tip: You can customize this high-level summary in your review settings.

@coderabbitai

coderabbitai Bot commented Dec 17, 2025

Copy link
Copy Markdown

Walkthrough

Added a new Scoop manifest bucket/tla-toolbox.json for TLA+ Toolbox v1.7.4 (Windows) containing metadata, resource URL and hash, extract_dir, a pre_install PowerShell script, bin and shortcut entries, persisted configuration, checkver pointing to GitHub releases, and autoupdate metadata using GitHub release tags.

Changes

Cohort / File(s) Change Summary
New manifest
bucket/tla-toolbox.json
Added a JSON Scoop manifest for TLA+ Toolbox v1.7.4 including: metadata (description, homepage, license, notes, suggested tools), resource URL and SHA1 hash, extract_dir, pre_install PowerShell script, bin entries (toolbox.exe, tla2tools.cmd), a shortcut (TLA+ Toolbox), persist: "configuration", checkver (GitHub releases), and autoupdate using GitHub releases/tags with regex-based hash lookup.

Estimated code review effort

🎯 2 (Simple) | ⏱️ ~10 minutes

Suggested reviewers

  • z-Fng
  • niheaven

"I’m a rabbit with a tiny drum,
I hopped to pack the Toolbox hum—
v1.7.4 neat and tidy,
Configs saved and shortcuts ready.
A little hop, a tiny thrum! 🥕🐇"

Pre-merge checks and finishing touches

✅ Passed checks (5 passed)
Check name Status Explanation
Title check ✅ Passed The title clearly describes the main changes: renaming to stable version 1.7.4, using internal Java, and persisting configuration, matching the PR objectives.
Linked Issues check ✅ Passed The PR directly addresses all coding requirements from issue #16802: adds manifest for v1.7.4, renames file to tla-toolbox.json, implements configuration persistence, adds pre_install script for bundled Java, and uses proper field ordering.
Out of Scope Changes check ✅ Passed All changes in the manifest file directly support the linked issue requirements; no unrelated or out-of-scope modifications are present.
Docstring Coverage ✅ Passed No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check.
Description check ✅ Passed PR description contains required checklist items and links to relevant issue, but lacks conventional title format in description body.
✨ Finishing touches
  • 📝 Generate docstrings

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

Comment @coderabbitai help to get the list of available commands and usage tips.

@github-actions

Copy link
Copy Markdown
Contributor

All changes look good.

Wait for review from human collaborators.

tla-toolbox

  • Lint
  • Description
  • License
  • Hashes
  • Checkver
  • Autoupdate
  • Autoupdate Hash Extraction

Check the full log for details.

@goyalyashpal goyalyashpal marked this pull request as draft December 18, 2025 17:47
@goyalyashpal goyalyashpal changed the title tla-toolbox@1.7.4: Use stable version & persist config tla-toolbox@1.7.4: Use stable version, internal java & persist config Dec 23, 2025
@goyalyashpal

goyalyashpal commented Dec 24, 2025

Copy link
Copy Markdown
Contributor Author

@goyalyashpal

Copy link
Copy Markdown
Contributor Author

/verify

@github-actions

Copy link
Copy Markdown
Contributor

All changes look good.

Wait for review from human collaborators.

tla-toolbox

  • Lint
  • Description
  • License
  • Hashes
  • Checkver
  • Autoupdate
  • Autoupdate Hash Extraction

Check the full log for details.

@goyalyashpal goyalyashpal marked this pull request as ready for review December 25, 2025 08:41

@coderabbitai coderabbitai Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actionable comments posted: 2

📜 Review details

Configuration used: Organization UI

Review profile: CHILL

Plan: Pro

📥 Commits

Reviewing files that changed from the base of the PR and between 03f91b7 and d61a0cf.

📒 Files selected for processing (1)
  • bucket/tla-toolbox.json
🧰 Additional context used
🧠 Learnings (1)
📓 Common learnings
Learnt from: o-l-a-v
Repo: ScoopInstaller/Extras PR: 16378
File: bucket/compactgui.json:20-22
Timestamp: 2025-10-19T13:58:23.389Z
Learning: In the ScoopInstaller/Extras repository, the CompactGUI manifest removed hash verification from the autoupdate block because the hash verification mechanism (scraping SHA-256 from release page HTML) is no longer available in newer CompactGUI releases. GitHub asset digests exist in beta releases but not in v3.8.0, and Scoop doesn't have built-in support for extracting from GitHub API asset digests.
Learnt from: Gitoffthelawn
Repo: ScoopInstaller/Extras PR: 16106
File: bucket/czkawka-gui.json:25-25
Timestamp: 2025-09-05T09:41:52.653Z
Learning: For czkawka-gui manifests in Scoop Extras, the correct upstream filename pattern for Windows GUI builds in recent versions uses "gtk46" (without underscore), not "gtk_46" (with underscore). The autoupdate URL should use "windows_czkawka_gui_gtk46.zip" format. This was confirmed by a working 10.0.0 update with valid hash.
Learnt from: Gitoffthelawn
Repo: ScoopInstaller/Extras PR: 16106
File: bucket/czkawka-gui.json:25-25
Timestamp: 2025-09-05T09:41:52.653Z
Learning: For czkawka-gui manifests in Scoop Extras, the correct upstream filename pattern for Windows GUI builds uses "gtk46" (without underscore), not "gtk_46" (with underscore). The autoupdate URL should use "windows_czkawka_gui_gtk46.zip" format.
Learnt from: haussmann
Repo: ScoopInstaller/Extras PR: 16863
File: bucket/browseros.json:15-17
Timestamp: 2025-12-21T13:49:44.001Z
Learning: In Scoop manifests, when a URL uses a fragment like `#/dl.7z`, Scoop automatically extracts the archive after download. For nested archives (like BrowserOS), the downloaded installer may contain another archive (e.g., `chrome.7z`) that requires explicit extraction via the installer script using `Expand-7zipArchive`. The installer script should reference the inner archive name, not the outer `dl.7z`.

Comment thread bucket/tla-toolbox.json
Comment thread bucket/tla-toolbox.json
@goyalyashpal goyalyashpal marked this pull request as draft December 31, 2025 14:41
Problem: Tools usage was unclear due to constricted aliasing
Solution: Align aliases according to original usage intent as do-
        cumented upstream in following file:
        https://github.com/tlaplus/tlaplus/blob/c8a59811fc/README.md#L16-L30
@goyalyashpal goyalyashpal marked this pull request as ready for review December 31, 2025 20:39

@coderabbitai coderabbitai Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actionable comments posted: 2

♻️ Duplicate comments (1)
bucket/tla-toolbox.json (1)

69-72: This issue was already flagged in previous reviews.

The autoupdate hash regex $sha1\|$basename uses invalid syntax. As noted in previous reviews, either remove the hash block or fix the regex to properly capture the 40-character SHA1 hash (e.g., ([0-9a-f]{40})\|$basename).

📜 Review details

Configuration used: Organization UI

Review profile: CHILL

Plan: Pro

📥 Commits

Reviewing files that changed from the base of the PR and between c268ce5 and 9a7fe3a.

📒 Files selected for processing (1)
  • bucket/tla-toolbox.json
🧰 Additional context used
🧠 Learnings (7)
📓 Common learnings
Learnt from: o-l-a-v
Repo: ScoopInstaller/Extras PR: 16378
File: bucket/compactgui.json:20-22
Timestamp: 2025-10-19T13:58:23.389Z
Learning: In the ScoopInstaller/Extras repository, the CompactGUI manifest removed hash verification from the autoupdate block because the hash verification mechanism (scraping SHA-256 from release page HTML) is no longer available in newer CompactGUI releases. GitHub asset digests exist in beta releases but not in v3.8.0, and Scoop doesn't have built-in support for extracting from GitHub API asset digests.
Learnt from: Gitoffthelawn
Repo: ScoopInstaller/Extras PR: 16106
File: bucket/czkawka-gui.json:25-25
Timestamp: 2025-09-05T09:41:52.653Z
Learning: For czkawka-gui manifests in Scoop Extras, the correct upstream filename pattern for Windows GUI builds in recent versions uses "gtk46" (without underscore), not "gtk_46" (with underscore). The autoupdate URL should use "windows_czkawka_gui_gtk46.zip" format. This was confirmed by a working 10.0.0 update with valid hash.
Learnt from: haussmann
Repo: ScoopInstaller/Extras PR: 16863
File: bucket/browseros.json:15-17
Timestamp: 2025-12-21T13:49:44.001Z
Learning: In Scoop manifests, when a URL uses a fragment like `#/dl.7z`, Scoop automatically extracts the archive after download. For nested archives (like BrowserOS), the downloaded installer may contain another archive (e.g., `chrome.7z`) that requires explicit extraction via the installer script using `Expand-7zipArchive`. The installer script should reference the inner archive name, not the outer `dl.7z`.
Learnt from: Gitoffthelawn
Repo: ScoopInstaller/Extras PR: 16106
File: bucket/czkawka-gui.json:25-25
Timestamp: 2025-09-05T09:41:52.653Z
Learning: For czkawka-gui manifests in Scoop Extras, the correct upstream filename pattern for Windows GUI builds uses "gtk46" (without underscore), not "gtk_46" (with underscore). The autoupdate URL should use "windows_czkawka_gui_gtk46.zip" format.
Learnt from: mokosiy
Repo: ScoopInstaller/Extras PR: 16428
File: bucket/multidrive.json:8-8
Timestamp: 2025-10-27T13:19:16.982Z
Learning: For MultiDrive manifests in the ScoopInstaller/Extras repository: the direct download URL at dl.atola.com causes 403 errors due to Cloudflare Bot Fight Mode blocking the Scoop bot, so GitHub Releases URLs should be used instead (e.g., https://github.com/atola-technology/multidrive/releases/download/...).
Learnt from: o-l-a-v
Repo: ScoopInstaller/Extras PR: 16349
File: bucket/fvim.json:45-49
Timestamp: 2025-10-16T15:59:21.258Z
Learning: In Scoop manifests, the `autoupdate.url` and `autoupdate.architecture.<arch>.url` fields must be valid URIs according to the JSON schema (defined with `"format": "uri"`). Variables like `$matchUrlx64` that contain only path segments must be combined with a base URL (e.g., `https://github.com/.../releases/download/`) to form a complete valid URI.
📚 Learning: 2025-10-19T13:58:23.389Z
Learnt from: o-l-a-v
Repo: ScoopInstaller/Extras PR: 16378
File: bucket/compactgui.json:20-22
Timestamp: 2025-10-19T13:58:23.389Z
Learning: In the ScoopInstaller/Extras repository, the CompactGUI manifest removed hash verification from the autoupdate block because the hash verification mechanism (scraping SHA-256 from release page HTML) is no longer available in newer CompactGUI releases. GitHub asset digests exist in beta releases but not in v3.8.0, and Scoop doesn't have built-in support for extracting from GitHub API asset digests.

Applied to files:

  • bucket/tla-toolbox.json
📚 Learning: 2025-09-05T09:41:52.653Z
Learnt from: Gitoffthelawn
Repo: ScoopInstaller/Extras PR: 16106
File: bucket/czkawka-gui.json:25-25
Timestamp: 2025-09-05T09:41:52.653Z
Learning: For czkawka-gui manifests in Scoop Extras, the correct upstream filename pattern for Windows GUI builds in recent versions uses "gtk46" (without underscore), not "gtk_46" (with underscore). The autoupdate URL should use "windows_czkawka_gui_gtk46.zip" format. This was confirmed by a working 10.0.0 update with valid hash.

Applied to files:

  • bucket/tla-toolbox.json
📚 Learning: 2025-10-16T15:59:21.258Z
Learnt from: o-l-a-v
Repo: ScoopInstaller/Extras PR: 16349
File: bucket/fvim.json:45-49
Timestamp: 2025-10-16T15:59:21.258Z
Learning: In Scoop manifests, the `autoupdate.url` and `autoupdate.architecture.<arch>.url` fields must be valid URIs according to the JSON schema (defined with `"format": "uri"`). Variables like `$matchUrlx64` that contain only path segments must be combined with a base URL (e.g., `https://github.com/.../releases/download/`) to form a complete valid URI.

Applied to files:

  • bucket/tla-toolbox.json
📚 Learning: 2025-10-13T09:37:06.093Z
Learnt from: o-l-a-v
Repo: ScoopInstaller/Extras PR: 16328
File: bucket/winutil.json:0-0
Timestamp: 2025-10-13T09:37:06.093Z
Learning: When reviewing code in Scoop manifests, always verify the actual file content if the diff appears incomplete or unusual, as diff context can be truncated or displayed incorrectly. The pattern `[string[]](...).ForEach{...}` is commonly used in post_uninstall scripts across the Extras repository.

Applied to files:

  • bucket/tla-toolbox.json
📚 Learning: 2025-09-05T09:41:52.653Z
Learnt from: Gitoffthelawn
Repo: ScoopInstaller/Extras PR: 16106
File: bucket/czkawka-gui.json:25-25
Timestamp: 2025-09-05T09:41:52.653Z
Learning: For czkawka-gui manifests in Scoop Extras, the correct upstream filename pattern for Windows GUI builds uses "gtk46" (without underscore), not "gtk_46" (with underscore). The autoupdate URL should use "windows_czkawka_gui_gtk46.zip" format.

Applied to files:

  • bucket/tla-toolbox.json
📚 Learning: 2025-12-21T13:49:44.001Z
Learnt from: haussmann
Repo: ScoopInstaller/Extras PR: 16863
File: bucket/browseros.json:15-17
Timestamp: 2025-12-21T13:49:44.001Z
Learning: In Scoop manifests, when a URL uses a fragment like `#/dl.7z`, Scoop automatically extracts the archive after download. For nested archives (like BrowserOS), the downloaded installer may contain another archive (e.g., `chrome.7z`) that requires explicit extraction via the installer script using `Expand-7zipArchive`. The installer script should reference the inner archive name, not the outer `dl.7z`.

Applied to files:

  • bucket/tla-toolbox.json
🔇 Additional comments (4)
bucket/tla-toolbox.json (4)

33-56: LGTM: Bin entries are well-structured.

The bin configuration correctly defines:

  • Direct executables (toolbox.exe, tla2tools.cmd)
  • Aliases with class module arguments that align with the modules verified in the pre_install script (lines 27-31)

The structure follows Scoop conventions properly.


63-63: LGTM: Configuration persistence aligns with PR objectives.

The persist field correctly ensures user settings survive updates and reinstalls, which was a key objective from issue #16802.


67-68: LGTM: Autoupdate URL structure is correct.

The autoupdate URL template properly uses the $version variable and matches the structure of the main download URL.


74-77: LGTM: Helpful documentation references for maintainers.

The comment section provides useful links to PowerShell quoting rules and upstream documentation, which aids future maintenance.

Comment thread bucket/tla-toolbox.json
Comment on lines +20 to +24
" \"@pushd `\"$dir`\"\"",
" '@set TOOLS_JAR=.\\tla2tools.jar'",
" \"@set THISJAVA=`\"${JDKDIR}\\jre\\bin\\java`\"\"",
" '@%THISJAVA% -cp %TOOLS_JAR% %*'",
" '@popd'",

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Potential issue | 🟠 Major

Consider avoiding directory changes in the wrapper script to improve usability.

The @pushd/@popd pattern changes the working directory to the install directory, which breaks relative paths from the user's perspective. This is why line 6 notes that users must "specify full path for the spec inputfile when running tlc".

A better design would use absolute paths for the Java executable and JAR file without changing directories, allowing users to work with relative paths naturally.

🔎 Alternative implementation without directory changes
 "@(",
-"  \"@pushd `\"$dir`\"\"",
-"  '@set TOOLS_JAR=.\\tla2tools.jar'",
+"  \"@set TOOLS_JAR=`\"$dir\\tla2tools.jar`\"\"",
 "  \"@set THISJAVA=`\"${JDKDIR}\\jre\\bin\\java`\"\"",
 "  '@%THISJAVA% -cp %TOOLS_JAR%  %*'",
-"  '@popd'",
 ")  | Set-Content \"$dir\\tla2tools.cmd\" -Encoding ASCII",

Note: This still depends on fixing $JDKDIR (lines 17-18), but once that's corrected to produce an absolute path like $dir\plugins\jdk.openjdk..., this approach would:

  1. Use absolute paths for both THISJAVA and TOOLS_JAR
  2. Preserve the user's working directory
  3. Allow users to work with relative paths for their spec files
  4. Make the note on line 6 unnecessary

Committable suggestion skipped: line range outside the PR's diff.

🤖 Prompt for AI Agents
In bucket/tla-toolbox.json around lines 20 to 24, the wrapper script uses
@pushd/@popd which changes the process working directory and forces users to
supply absolute paths; remove the directory change and instead compute absolute
paths for THISJAVA and TOOLS_JAR from the installer $dir (ensure $JDKDIR is
resolved to an absolute path under $dir\plugins\...), then invoke the Java
executable with an absolute path and -cp to the absolute JAR while leaving the
current working directory untouched so users can supply relative spec paths;
also remove or update the note about requiring full paths.

Comment thread bucket/tla-toolbox.json
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

[Bug]: tla-toolbox: v1.8.0 is dev / prerelease

1 participant