tlaplus
TLAPM fails to run with error code -1073741515
Using tlaps 1.4.5 with toolbox 1.7.1 on Windows 10, and cygwin 3.2.0-1
I installed TLAPS according to the instructions at https://tla.msr-inria.inria.fr/tlaps/content/Download/Binaries/Windows.html
tlapm.exe runs fine in the cygwin window.
I added the tlapm.exe path in the toolbox at File > Preferences > TLAPS, but when I run it with CTRL+G+G the following error occurs:
Error running tlapm. Report a bug with the error code to the developers at https://github.com/tlaplus/tlapm/issues.
Error code: -1073741515
I'm running it on the following simple file:
------------------------------- MODULE Proofs -------------------------------
EXTENDS Naturals
THEOREM OnePlusOne == 1 + 1 = 2
PROOF
OBVIOUS
=============================================================================
Thank you for reporting this issue. Based on discussions on the website Stack Overflow about the error code -1073741515 in Windows, when this signed decimal integer value is interpreted as an unsigned integer value, the last 8 digits of its hexadecimal representation are c0000135, which when interpreted as an NTSTATUS code according to the Windows documentation means STATUS_DLL_NOT_FOUND with description "{Unable To Locate Component} This application has failed to start because %hs was not found. Reinstalling the application might fix this problem." (the string %hs would be replaced by text at runtime) (another mention of this exit code in Windows documentation).
The message "Error running tlapm ... tlapm/issues." is returned by the TLA+ Toolbox: https://github.com/tlaplus/tlaplus/blob/8dccb409a437ff7a9c556150ee147fad5c44526a/toolbox/org.lamport.tla.toolbox.tool.prover/src/org/lamport/tla/toolbox/tool/prover/job/ProverJob.java#L500-L501, and the integer value printed is returned in Java code by proverProcess.getExitValue().
Since tlapm.exe runs without issues within Cygwin's environment, it appears that comparing the environment paths within and outside of Cygwin could indicate what the differences are. A simple experiment would then be to add to the Windows path environment variable value those directories that are absent from it and present in the Cygwin path environment variable. The command echo %PATH% will show the value of the environment variable PATH in a Windows command line, and the command echo $PATH will show the value of the environment variable PATH in a Cygwin command line. (Perhaps another possibility would be to launch the TLA+ Toolbox from a Cygwin command line, so that it will probably use Cygwin's environment variables.) Relevant information about setting the path can be found in Cygwin's documentaton (which prepends the paths /usr/local/bin, /usr/bin, and /bin to the Windows system path (also relevant is Cygwin's documentation about environment variables).
About finding which DLL is not found during invocation of tlapm, two possibilities could be to attempt launching tlapm within a Windows environment (i.e., not Cygwin), and try to use Process Monitor or the command gflags /i tlapm +sls to find information about DLLs. Another possibility is suggested by Cygwin's documentation: objdump -p or cygcheck.
Other comments:
- The given TLA+ module
Proofsis proved by (a development version of)tlapmon my machine, using the SMT backend. - Trailing whitespace exists after the keyword
PROOF. - GitHub's
linguistincludes TLA+ in the languages recognized for syntax highlighting in fenced code blocks. TLA+ highlighting can be activated in Markdown as follows:```tla A == x = 1 /\ x' = 2 ```
Thanks, @johnyf! Adding /usr/bin and /bin to my Windows path in addition to /usr/local/bin fixed the issue. After running the TLAPS installer it says to add /usr/local/bin to your path, but not the others; perhaps adding these instructions to the installer output as well as the instructions up above would help.
@johnyf Running TLAPS in WSL/WSL2 has been reliable for Leslie and me. With yesterday's WSL2 announcement about support for GUI apps, you could consider deprecating the Cygwin installer in favor of easy-to-install TLAPS and Toolbox Debian/Ubuntu packages (latter already exists).
Thank you @ahelwer for suggesting documenting this information in the installer's messages. Thank you @lemmy for noting that TLAPS is known to reliably work on WSL/WSL2, suggesting transitioning to WSL2, and deprecating support for Cygwin.
I think that deprecating the Cygwin installer will make the packaging of tlapm easier, because building in Cygwin all the dependencies of tlapm that are packaged in the installer is nontrivial:
https://github.com/tlaplus/tlapm/blob/0402a4ccd331ddea0acfd6949a7faf6d3e42d861/tools/installer/tlaps-release.sh.in#L129
A Debian package of tlapm or the Linux installer of tlapm can be used instead of the Cygwin installer.
For now, the Cygwin-related parts of the script tools/installer/tlaps-release.sh.in (which builds the installer) can remain, and not be unused. When the branch isabelle2020 is merged, those parts will become outdated, and if not updated would need to be removed.
For posterity, a message could be added to the installer after:
https://github.com/tlaplus/tlapm/blob/0402a4ccd331ddea0acfd6949a7faf6d3e42d861/tools/installer/tlaps-release.sh.in#L619-L620
(which prints the installer message about adding /usr/local/bin to the environment's path--where the prefix/usr/local might differ depending on what the user selected when installing tlapm) that gets printed when the installer runs in Cygwin, and informs that for running tlapm from outside Cygwin, the Cygwin paths /usr/bin and /bin may also need to be added to the (non-Cygwin) path. Including links to the Cygwin documentation seems relevant here, specifically:
- https://cygwin.com/cygwin-ug-net/setup-env.html
- https://cygwin.com/faq.html#faq.using.path
because these Cygwin paths will need to be translated to whatever path representation is used outside Cygwin, in order to add them to that environment. So linking also to the tool cygpath:
https://cygwin.com/cygwin-ug-net/cygpath.html
will probably be helpful.
Also, the webpage that describes installation on Windows (the TLAPS website is part of the tlapm repository) could be updated with the information about updating the environment's path outside of Cygwin. Namely, the pages:
- https://github.com/tlaplus/tlapm/blob/0402a4ccd331ddea0acfd6949a7faf6d3e42d861/doc/web/content/Download/Source.html
- https://github.com/tlaplus/tlapm/blob/0402a4ccd331ddea0acfd6949a7faf6d3e42d861/doc/web/content/Download/Binaries/Windows.html
When Cygwin installers are no longer distributed for the latest version of tlapm, the webpage about installation from binaries on Windows could be updated to describe how to install in WSL2, and keep the old Cygwin instructions for anyone interested to run the Cygwin installer for an older version of tlapm:
https://github.com/tlaplus/tlapm/blob/0402a4ccd331ddea0acfd6949a7faf6d3e42d861/doc/web/content/Download/Binaries/Windows.html
After Cygwin support has been removed from the packaging script, the webpage about building from source could be updated to leave unspecified whether tlapm is known to build and work on Cygwin:
https://github.com/tlaplus/tlapm/blob/0402a4ccd331ddea0acfd6949a7faf6d3e42d861/doc/web/content/Download/Source.html#L28-L29
Mention of Cygwin may need to be removed also from:
https://github.com/tlaplus/tlapm/blob/0402a4ccd331ddea0acfd6949a7faf6d3e42d861/INSTALL#L9-L13
when it will no longer be known whether building tlapm on Cygwin works.
