search

flathub / org.lamport.tla.toolbox

https://flathub.org/apps/details/org.lamport.tla.toolbox
2 stars 2 forks source link

Flatpak app of TLA+ Toolbox cannot find pdflatex (not in sandbox) #29

Open cmsmcq opened 1 year ago

cmsmcq commented 1 year ago

Description

I recently installed TLA+ Toolbox from the Pop!_OS 'Pop!_Shop' app. It's nice to have installation be so convenient, so I am grateful to those who did the work of making the Flatpak package. But there is a flaw.

In that version of TLA+ Toolbox, invocations of the 'Produce PDF version' lead to an error message saying something like:

The following error was encountered while attempting to generate the PDF - perhaps you have not set a full path to pdflatex in the preferences?

TLATeX unrecoverable error: -- Trying to run the command `/usr/bin/pdflatex SimpleProgram.tex' produced the following error Cannot run program "/usr/bin/pdflatex" (in directory "/home/yadda/yadda/tla/SimpleProgram.toolbox"): error=2, No such file or directory.

Providing an absolute path for pdflatex in the Preferences interface does not solve the problem.

Investigation show that the /usr/bin directory seen by the TLA+ Toolbox code is not the /usr/bin directory I see; I surmise that the Toolbox is running inside a sandbox provided as part of the Flatpak package. Crucially, that sandbox contains neither the pdflatex and pdftex present in my local file system, nor any version of LaTeX it could use.

Steps to Reproduce

  1. Install TLA+ Toolbox from Flathub.org
  2. Create a module or open an existing module.
  3. Invoke the create-pdf-version action (via menu or keystroke).

Steps Taken to Fix

A summary of my efforts to diagnose and fix the problem are in the comments of issue #54 and issue #821 in the tlaplus/tlaplus directory.

Possible Fix

For me, the successful fix was to uninstall the Flatpak version of TLA+ Toolbox and install from the zip file in the Github page https://github.com/tlaplus/tlaplus/releases/tag/v1.7.1#latest-tla-files

A better fix, if it's possible, would be to change the Flatpak app of TLA+ Toolbox so that a working copy of pdflatex is inside the sandbox. I don't know enough about Flatpak to know how difficult or easy that would be.

From the developers of the TLA+ Toolbox I learn that they don't make the Flatpak package; the contributing guidelines in the repository flathub/flathub say that issues with a package should reported in the repo for the package, so I'm raising this issue here.

dimdin commented 2 months ago

To solve the cannot find pdflatex install the org.freedesktop.Sdk.Extension.texlive extension. To install, run:

flatpak install flathub org.freedesktop.Sdk.Extension.texlive

and select the same version with the toolbox platform (currently 22.08).

Best solution is to add this information in the metadata description:

NOTE: In order to be able to produce a PDF version via LaTeX you need to additionally install the extension org.freedesktop.Sdk.Extension.texlive