Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Passing pdflatex options to isabelle build

Email Gateway (Aug 22 2022 at 19:22):

From: Diego Machado Dias <diegodias.m@gmail.com>
Dear all,

I would like to use the latex package minted in the documentation of a
theory file, but the PDF generation requires pdflatex to be called passing
the --shell-escape option.

How can I configure isabelle build to pass the option --shell-escape when
calling the latex compiler?

Best regards,
Diego

Email Gateway (Aug 22 2022 at 19:22):

From: Diego Machado Dias <diegodias.m@gmail.com>
I've just figured out an adhoc solution: to edit the etc/settings file in
the Isabelle directory.

ISABELLE_LATEX="latex -file-line-error --shell-escape"
ISABELLE_PDFLATEX="pdflatex -file-line-error --shell-escape"

Is there a way of changing these variables without overwriting this
configuration file?

Best regards,
Diego

Email Gateway (Aug 22 2022 at 19:23):

From: Makarius <makarius@sketis.net>
See the top of this file:

Important notes:

* See the "system" manual for explanations on Isabelle settings

* User settings go into $ISABELLE_HOME_USER/etc/settings

* DO NOT EDIT the repository copy of this file!

* DO NOT COPY this file into the $ISABELLE_HOME_USER directory!

Anyway, I did not quite understand the purpose of --shell-escape.
Instead of odd shell hacking there are at least two official possibilities:

* Use of document/build scripts (see examples in the Isabelle
distribution in src/Doc/...).

* Use of Isabelle/ML to generate required latex sources (via document
antiquotations). (You can use the Prover IDE with control-hover-click on
existing antiquotations to get to example implementations).

Makarius

Last updated: May 06 2024 at 20:16 UTC