Installation on macOS needs better instructions

ghost commented 4 years ago

I'm trying to install TLAPS on macOS following the instructions provided at https://tla.msr-inria.inria.fr/tlaps/content/Download/Binaries/MacOS.html

I successfully installed the binary in the default location. I'm stuck with the last part:

You will need to add the location of the TLAPS.tla file to the list of libraries used by the Toolbox. 
To do this, open the Toolbox and go to "File > Preferences > TLA+ Preferences". 
Add the directory where TLAPS.tla is located to the list of library path locations. 
If you have the default installation, this directory is /usr/local/lib/tlaps/.

At this point, the "add directory" doesn't show usr as a valid choice, thus making impossible to add it to TLA Toolbox:

Searching for TLAPS.tla or tlaps path, doesn't work.

System Information

macOS Catalina 10.15.4 (19E287) TLAPS: 1.4.5 TLA Toolbox. This is Version 1.6.0 of 10 July 2019 and includes:

SANY Version 2.1 of 23 July 2017
TLC Version 2.14 of 10 July 2019
PlusCal Version 1.9 of 10 July 2019
TLATeX Version 1.0 of 20 September 2017

TLAPS installation details

/usr/local/bin is in PATH.

> cd /usr/local/lib/tlaps
> ls -lsa
total 2896
drwxr-xr-x   36 502   wheel   1.1K Apr 18 15:30 .
drwxr-xr-x  494 502   wheel    15K Apr 18 15:30 ..
-rw-r--r--    1 502   wheel   7.4K Feb 28 16:26 Bags.tla
-rw-r--r--    1 502   wheel   9.3K Feb 28 16:26 BagsTheorems.tla
-rw-r--r--    1 502   wheel    11K Feb 28 16:26 BagsTheorems_proofs.tla
drwxr-x---    6 root  wheel   192B Apr 18 15:30 Cantor1.tlaps
-rw-r--r--    1 502   wheel    19K Feb 28 16:26 FiniteSetTheorems.tla
-rw-r--r--    1 502   wheel    41K Feb 28 16:26 FiniteSetTheorems_proofs.tla
-rw-r--r--    1 502   wheel   1.3K Feb 28 16:26 FiniteSets.tla
-rw-r--r--    1 502   wheel    28K Feb 28 16:26 FunctionTheorems.tla
-rw-r--r--    1 502   wheel    45K Feb 28 16:26 FunctionTheorems_proofs.tla
-rw-r--r--    1 502   wheel   3.3K Feb 28 16:26 Functions.tla
lrwxr-xr-x    1 502   wheel    14B Feb 28 16:25 Isabelle -> Isabelle2011-1
drwxr-xr-x   16 502   staff   512B Feb 28 16:25 Isabelle2011-1
-rw-r--r--    1 502   wheel   8.8K Feb 28 16:26 NaturalsInduction.tla
-rw-r--r--    1 502   wheel    20K Feb 28 16:26 NaturalsInduction_proofs.tla
-rw-r--r--    1 502   wheel   848B Feb 28 16:26 RealTime.tla
-rw-r--r--    1 502   wheel    18K Feb 28 16:26 SequenceOpTheorems.tla
-rw-r--r--    1 502   wheel    34K Feb 28 16:26 SequenceOpTheorems_proofs.tla
-rw-r--r--    1 502   wheel   2.4K Feb 28 16:26 SequenceOps.tla
-rw-r--r--    1 502   wheel   9.1K Feb 28 16:26 SequenceTheorems.tla
-rw-r--r--    1 502   wheel    11K Feb 28 16:26 SequenceTheorems_proofs.tla
drwxr-xr-x   23 502   wheel   736B Dec 11  2017 TLA+
-rw-r--r--    1 502   wheel    21K Feb 28 16:26 TLAPS.tla
-rw-r--r--    1 502   wheel    16K Feb 28 16:26 WellFoundedInduction.tla
-rw-r--r--    1 502   wheel    31K Feb 28 16:26 WellFoundedInduction_proofs.tla
drwxr-xr-x    9 502   wheel   288B Feb 28 16:26 bin
drwxr-xr-x    3 502   wheel    96B Feb 28 16:26 emacs
drwxr-xr-x   20 502   wheel   640B Feb 28 16:22 examples
drwxr-x---    3 root  wheel    96B Apr 18 15:30 heaps
-rwxr-xr-x    1 502   wheel   996K Feb 28 16:26 un-inst
-rw-r--r--    1 502   wheel   4.9K Feb 28 16:26 zenon.v
-rw-r--r--    1 502   wheel   6.0K Feb 28 16:26 zenon_coqbool.v
-rw-r--r--    1 502   wheel    47K Feb 28 16:26 zenon_equiv.v
-rw-r--r--    1 502   wheel   7.9K Feb 28 16:26 zenon_focal.v
-rw-r--r--    1 502   wheel   1.3K Feb 28 16:26 zenon_induct.v

ghost commented 4 years ago

Workaround

Add a symbolic link for /usr/local/lib/tlaps in a known location visible from TLA Toolbox, such as your home directory.

> cd ~
> ln -s /usr/local/lib/tlaps tlaps

muenchnerkindl commented 4 years ago

A perhaps more "Mac-native" way to achieve this is to reveal the directory in the Finder (Go -> Go to Folder ... then enter /usr/local) and add that directory to your Favorites in the sidebar. It is then accessible whenever a file browser shows up. I find it frequently useful to be able to access /usr/local and similar Unixish directories that MacOS tries to hide from you.

Stephan

On 18 Apr 2020, at 16:05, Nicholas Fiorentini notifications@github.com wrote:

Workaround

Add a symbolic link for /usr/local/lib/tlaps in a known location visible from TLA Toolbox, such as your home directory.

cd ~ ln -s /usr/local/lib/tlaps tlaps https://user-images.githubusercontent.com/45690027/79639812-43241a00-818e-11ea-80e0-c0f38f1ffe7c.png — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/tlaplus/tlapm/issues/7#issuecomment-615877229, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABZCW5NMY3F4CK5GGDLCPBLRNGXQ7ANCNFSM4MLLOBKA.

damiendoligez commented 4 years ago

In fact, when you are in the Select the library path location dialog, you can simply hit the / key and it will open a text box where you can type any path you want, including /usr/local/lib/tlaps:

ScreenShot

This is a general feature of MacOS "open file" dialogs.

ghost commented 4 years ago

In fact, when you are in the Select the library path location dialog, you can simply hit the / key and it will open a text box where you can type any path you want, including /usr/local/lib/tlaps

Thanks! Didn't know this feature.

tlaplus / tlapm