Error Producing PDF Version

[Ryan Mortensen]

I try to run the PDF producer on the toolbox that I just downloaded, but I get the following error:

TLATeX unrecoverable error: Tring to run command `pdflatex DieHard.tex` produced  the following error- Cannot run program 'pdflatex' in directory /my/dir/DieHard.toolbox.

error=2 

The system cannot find the file specified.

Is this because of a faulty installation on my part?

I read the other messages from 2013, which makes me wonder if I need to install Latex separately?

[Markus Kuppe]

Hi Ryan,

you have to install LaTeX and configure the path to pdflatex in the
Toolbox's preference [1][2]. By the way, the upcoming Toolbox release
will have a more descriptive error message when pdflatex cannot be not
found.

M.

[1] https://tla.msr-inria.inria.fr/tlatoolbox/doc/spec/pretty-printing.html
[2] https://github.com/tlaplus/tlaplus/issues/54#issuecomment-304531412

[burt]

I had the same problem. The toolbox generates a tex-file in the folder spec.toolbox, in your case DieHard.toolbox. But it seems that the pdflatex command is run in the current folder, the parent of DieHard.toolbox.

A work around that worked for me: 

I changed the command in preferences to "cd DieHard.toolbox; pdflatex"

Not quite convenient, because it must be changed for every new spec. But it works for me.

[loki der quaeler]

If you specify a full path to pdflatex, you could be "one and done" as opposed to updating the preferences.

[burt]

that's right, even if I don't understand why.

[loki der quaeler]

It's because Eclipse (on which the Toolbox is based) does not handle inheriting a user's PATH setting well, and so if a user's pdflatex is installed anywhere except for the most basic of places (like "/bin" on a *NIX based OS), pdflatex won't be found (and so the full path to it must be specified.)

[burt]

Hi Loki,

why I'm wondering:

- "pdflatex" in the preferences does not work, but

- "cd spec.toolbox; pdflatex" does.

Why does Eclpise find my pdflatex in the second case, but not in the first one.

(Not an important question, just being curious.)

[loki der quaeler]

That is an excellent question :- )

If i had to waive my hands furiously in the air - since 'cd' is a built in shell command, perhaps its invocation causes the user's shell .rc / aliases file to be loaded thereby picking up a full PATH with includes the directory containing pdflatex. ?

Buy that? :- )

[Clifford Heath]

Probably because "." is in the $PATH

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/38a1cfee-e1f1-44ca-ab06-ebeff070e362%40googlegroups.com.

[loki der quaeler]

I'm pretty sure he is saying that he changes the cd command per spec, not that he copies pdflatex into every toolbox.

On Saturday, March 14, 2020 at 7:29:48 PM UTC-7, Clifford Heath wrote:

Probably because "." is in the $PATH

On Sun., 15 Mar. 2020, 08:24 loki der quaeler, <qua...@gmail.com> wrote:

That is an excellent question :- )

If i had to waive my hands furiously in the air - since 'cd' is a built in shell command, perhaps its invocation causes the user's shell .rc / aliases file to be loaded thereby picking up a full PATH with includes the directory containing pdflatex. ?

Buy that? :- )

Hi Loki,

why I'm wondering:

- "pdflatex" in the preferences does not work, but

- "cd spec.toolbox; pdflatex" does.

Why does Eclpise find my pdflatex in the second case, but not in the first one.

(Not an important question, just being curious.)

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.