Email Gateway (Aug 22 2022 at 20:59): Email Gateway (Aug 22 2022 at 20:59):From: João Rafael Nicola <joaoraf@gmail.com>
Hi,
I would like to do some post-processing on the LaTeX code generated from
my theory files prior to
running pdflatex. However I have not found a way to either (1) intervene in
the middle of the build
process to insert a call to some extenal tool that rewrites the LaTeX files
(e.g. sed) just before
isabelle starts running pdflatex; or (2) stop the build process after the
the LaTeX files have been
generated, so that I can post-process them and call latexmk -pdf by hand.
Would you have any idea on how to achieve this?
Thanks,
João Rafael
Email Gateway (Aug 22 2022 at 20:59):From: Tobias Nipkow <nipkow@in.tum.de>
You can instruct Isabelle to dump all the generated files in a separate
directory for post-processing. In the ROOT file, add to your session
options [document_output = "generated"]
where "generated" is some name of your choice.
See The Isabelle System Manual.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 20:59):From: Makarius <makarius@sketis.net>
On 17/11/2019 11:11, Tobias Nipkow wrote:
You can instruct Isabelle to dump all the generated files in a separate
directory for post-processing. In the ROOT file, add to your sessionoptions [document_output = "generated"]
where "generated" is some name of your choice.
That is indeed the standard way for manual post-processing of generated
document sources.
More advanced applications can use a "build" script ...
See The Isabelle System Manual.
A quote from the text:
"""
In more complex situations, a separate ▩‹build› script for the document
sources may be given. It is invoked with command-line arguments for the
document format and the document variant name. The script needs to produce
corresponding output files, e.g.\ ▩‹root.pdf› for target format ▩‹pdf›
(and
default variants). The main work can be again delegated to @{tool latex},
but it is also possible to harvest generated {\LaTeX} sources and copy
them
elsewhere.
"""
An example is the manual itself:
https://isabelle.in.tum.de/repos/isabelle/file/Isabelle2019/src/Doc/System/document/build
Side-remark: for portable postpressing of source text you should use
perl instead of sed. Thus it will work on Linux, Windows, macOS without
further worries.
Makarius
Last updated: Apr 23 2024 at 08:19 UTC