tlaplus: TLA+ Toolbox can't locate pdflatex

On macOS 10.12.5 and Version 1.5.3 of TLA Toolbox.

$ which pdflatex
/usr/local/bin/pdflatex

But when attempting to pretty print a module from TLA+ Toolbox, I get the following PDF Production error:

TLATeX unrecoverable error: —Trying to run the command pdflatex SimpleProgram.tex produced the following error  Cannot run program “pdflatex” (in directory “/Users/samhavens/tla test/ SimpleProgram.toolbox”): error=2, No such file or directory.

I have LaTex installed via MacTex and Texmaker. I have verified that from the command line I can run pdflatex on .tex files to produce pdfs.

About this issue

Original URL
State: closed
Created 7 years ago
Reactions: 3
Comments: 15 (4 by maintainers)

Most upvoted comments

Hi,

did you try with the pdflatex command set to the complete path “/usr/local/bin/pdflatex” in the Toolbox’s preference?

pdfviewerpref

+11

lemmy on May 28, 2017

Good man. I appreciate it！！！！！！！

ruthless-gunner on Jul 22, 2023

Thank you, @Calvin-L – good suggestions, and eventually they led me to what I think is the root cause of my problem.

From file I get this output:

cmsmcq@gemma:$ file /usr/bin/pdflatex /usr/bin/pdflatex: symbolic link to pdftex cmsmcq@gemma:$ file /usr/bin/pdftex /usr/bin/pdftex: ELF 64-bit LSB pie executable, x86-64, version 1 (SYSV), dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2, BuildID[sha1]=f18468448a5dcf0246969b0343dbdaa52fff2fbd, for GNU/Linux 3.2.0, stripped cmsmcq@gemma:$

So I don’t think pdftex is a text executable that needs an interpreter.

To try to see whether it’s a path problem, I tried deleting my path and running pdflatex with PATH set to the empty string. It works:

$ # Is it a PATH problem?  Trying with cleared path.
$ pwd
/home/cmsmcq/2023/etudes/tla/SimpleProgram.toolbox
$ echo $PATH

$ /usr/bin/ls -l
total 44
-rw-r--r-- 1 cmsmcq cmsmcq 42550 Jun 18 19:36 SimpleProgram.tex
$ /usr/bin/pdflatex SimpleProgram.tex 
This is pdfTeX, Version 3.141592653-2.6-1.40.22 (TeX Live 2022/dev/Debian) (preloaded format=pdflatex)
 restricted \write18 enabled.
entering extended mode
(./SimpleProgram.tex
LaTeX2e <2021-11-15> patch level 1
L3 programming layer <2022-01-21>
$ /usr/bin/ls -l
total 132
-rw-rw-r-- 1 cmsmcq cmsmcq    32 Jun 18 20:09 SimpleProgram.aux
-rw-rw-r-- 1 cmsmcq cmsmcq  5987 Jun 18 20:09 SimpleProgram.log
-rw-rw-r-- 1 cmsmcq cmsmcq 76135 Jun 18 20:09 SimpleProgram.pdf
-rw-r--r-- 1 cmsmcq cmsmcq 42550 Jun 18 19:36 SimpleProgram.tex

$

From this I infer that the problem is not the setting of $PATH, or at least not just the setting of $PATH.

Your mention of interpreted executables gave me an idea: in Preferences, I pointed the Toolbox not to pdflatex but to a shell script which invokes pdflatex, but first writes some debugging code to a file in my directory tree. When the Toolbox runs the script, and the script records the contents of /usr/bin, the contents are very unlike what I see when I look at /usr/bin from the shell. Every file is shown as owned by my userid, rather than by root, and the contents of the directory differ: the contents overlap and neither set of programs is a subset of the other. And – of course – pdflatex and pdftex are missing, in the /usr/bin seen by my shell script running from inside the Toolbox.

It looks as though the Flatpak version of TLA+ Toolbox is running in some kind of sandbox. Wikipedia confirms that that is part of the point of Flatpak as a distribution method. The problem is that the sandbox lacks any version of TeX.

So it looks as if I can either live without generating PDF from inside the Toolbox, or reinstall from a different source.

Thank you for your help.

cmsmcq on Jun 19, 2023