[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Error Producing PDF Version

On 11.02.20 21:09, Ryan Mortensen wrote:
> 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?

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


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

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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/0071fe99-cecb-598f-7444-8bd12652558b%40lemmster.de.