Dear Murali, could you please be a bit more explicit in describing what kinds of errors you encounter when trying to install the prover? I am running TLAPS on Mac OS 10.12.2 (Sierra) and Toolbox 1.5.2 and am not aware of specific installation problems – of course, developers tend to be blind to such issues because their system is set up in a way that it works. Also, I do not know what you mean by "Launching toolbox from any other user directory". One problem (as for any application not launched from a terminal) is to control the setting of your search PATH, needed for finding the proof manager and the various backend provers. The recommended way to set the search path globally (independently from your login shell) in newer versions of OS X / MacOS is to list necessary paths in text files in /etc/paths.d/. Thanks, Stephan
|