Рендеринг PDF-доказательств с помощью Java (через LaTex?)

Question

В настоящее время я работаю над автоматическим средством проверки теорем в Java.

Я бы хотел представить эти доказательства в формате PDF. Предпочтительно, это будет происходить через что-то вроде LaTeX, используя proof.sty или qtree.sty Однако я читал, что рендеринг кода LaTeX из Java может быть немного проблематичным .

В Java доказательства представляются простыми деревьями, вдохновленными деревьями Хаскелла, такими как:

class Tree<A> {
  A       value;
  List<A> subForest;
}

У кого-нибудь есть идеи, как лучше всего это сделать?

В соответствующей заметке (т. Е. Решение "все остальное не удается"), каковы наилучшие практики для вызова исполняемого файла pdflatex из Java? (Что касается его нахождения, выяснения, существует ли он или нет ...)

Answer 1

Вы можете использовать jproc для запуска pdflatex.Он позволяет вам указать время ожидания и позаботится об обработке stdout и stderr, а также об интерпретации кода возврата.Убедитесь, что вы запускаете pdflatex с параметром -interaction = batchmode, чтобы он не останавливался на каждой ошибке.Кроме того, я бы порекомендовал использовать шаблонизатор, такой как speed или stringtemplate, для создания входных данных для латекса.В качестве альтернативы вы можете посмотреть на jlatexmath, который стремится предложить Java-API для латексных формул.