need better instructions and error behavior for when pdflatex is missing

[dwrensha]

I wanted to build the blueprint of the Equational Theories project.

I followed the leanblueprint README instructions:

$ sudo apt install graphviz libgraphviz-dev
$ pip install leanblueprint

Then I did

$ leanblueprint web

which seemed to succeed (return code was 0). However, when I looked at the generated html files, they were just stubs.

Then I looked in the full console output of the leanblueprint web call, and I found these lines:

INFO: Using the imager "gspdfpng".
/bin/sh: 1: pdflatex: not found
/bin/sh: 1: dvisvgm: not found

Aha, so I needed to install pdflatex. So then I did

$ sudo apt install texlive

and after that, leanblueprint web actually succeeded in building the full web blueprint.

---

There are two problems here:

1. the README should mention that I need to install texlive or similar
2. leanblueprint web should fail (not just log a message) if pdflatex (or whatever other needed tool) is not found.