Re: [tlaplus] Error Producing PDF Version

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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
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

-- 
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.