Re: [isabelle] Passing pdflatex options to isabelle build



On 21/03/2019 15:20, Diego Machado Dias wrote:
> 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?

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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.