TLA+ on Mac questions:

[sgl...@sglaser.com]

1. Home-brew seems to be broken. It complains about a SHA256 mismatch (see below)
2. Version confusion:
1. Home-brew wants to download 1.8.0
2. https://tla.msr-inria.inria.fr/tlatoolbox/ (alternate download site from TLA+ page) shows 1.7.1 as the latest.
1. No mention of 1.7.2 either
3. https://github.com/tlaplus/tlaplus (main download site) only has tlatools.jar, not the platform specific versions. It also doesn’t show any version numbers.
4. https://github.com/tlaplus/tlaplus/releases/tag/v1.8.0 shows a Mac version at the bottom but shows TBD in the checksums table.
1. The downloaded file has SHA256 81cd2276215ceda37ca629f30886c82bdce5987133d585d3fcadd47cd3df861e which matches the actual from home-brew.
2. Note that the checksum table on this page uses sha1 while home-brew uses sha256. No big deal unless you miss difference that and get confused.
3. This page shows the Clarke release (a.k.a. 1.8.0) as pre-release and 1.7.2 (Theano) as being the latest, but that tag doesn’t have platform specific releases.
3. None of the versions support Apple Silicon (M1/Arm). I’m thinking this is just a matter of bundling with the correct JVM right?

Home-brew output:

% brew install tla-plus-toolbox

==> Downloading https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/TLAToolbox-1.8.0-mac

==> Downloading from https://objects.githubusercontent.com/github-production-release-asset-2e65b

######################################################################## 100.0%

Error: SHA256 mismatch

Expected: 0353bd93f318b90608f1d1bc0c7bc6b43f4631476f22b90d30be793e156bdb03

  Actual: 81cd2276215ceda37ca629f30886c82bdce5987133d585d3fcadd47cd3df861e

    File: /Users/sglaser/Library/Caches/Homebrew/downloads/6a2e007976e09956fad76e5c32ac2af20327dd95deef5a83b62ef1d8c28bcdbd--TLAToolbox-1.8.0-macosx.cocoa.x86_64.zip

To retry an incomplete download, remove the file above.

Steve Glaser
sgl...@sglaser.com

[Alex Weisberger]

Not sure what the issue is here, but I always download the toolbox from the Github release: https://github.com/tlaplus/tlaplus/releases/tag/v1.7.2. I run that on a Mac ok.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a6374f09-e635-488b-88b2-477b950e8976%40Spark.

[tlaplus-go...@lemmster.de]

The 1.7.1 release was deleted from Github for unknown reasons, and the homebrew cask subsequently changed to 1.8.0 [1].  I now re-created the 1.7.1 release on Github [2].  Note that the two changes in the 1.7.2 release are also part of the upcoming 1.8.0 release.  Thus, please download 1.8.0 if you are a Toolbox user and need those two changes.

We would have to upgrade the Toolbox's Eclipse foundation and add another platform to our build for the next release to work natively on Apple Silicon (without Rosetta).  Please reach out to me if you can help.

Markus

[1] https://github.com/Homebrew/homebrew-cask/commits/79e4771698684aba3b270e9f03df10bc89fd4f14/Casks/tla-plus-toolbox.rb

[2] https://github.com/tlaplus/tlaplus/releases/tag/v1.7.1

[sgl...@sglaser.com]

Thanks.

The 1.8.0 version seems to work on my M1 Mac.

I mostly care about running TLC as efficient as possible. Toolbox appears to run reasonable well (Mac mini 16MB, 5K display).

Even if the Eclipse stuff uses Rosetta, is are the TLC subprocess(s) going to use the platform native JVM? That would reduce the need to fully support Apple Silicon (for a while at least).

Steve Glaser
sgl...@sglaser.com

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/022DE3F7-CD7A-4DBA-9C76-A8F1BC2C0622%40lemmster.de.

[tlaplus-go...@lemmster.de]

No, the Toolbox spawns the TLC process with its (Rosetta) JVM.  How big is the difference between running TLC on a native JVM compared to a JVM running on Rosetta?

Markus

[sgl...@sglaser.com]

Don’t know the perf delta. So far it’s not been a concern. I’m not running anything big right now.

Steve Glaser
sgl...@sglaser.com

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/47C2B83F-6746-48F2-9E72-DD0DC486995C%40lemmster.de.