add halt-on-error option to pdflatex
modify make-image
modify to output rule names
split proof tree