Email Gateway (Aug 22 2022 at 10:46): Email Gateway (Aug 22 2022 at 10:46):From: Makarius <makarius@sketis.net>
Makefiles are a historical misunderstanding. It is better to forget that
they ever existed.
The Isabelle document preparation allows to define a specific build
function, just by putting a shell script (in fact any executable) of the
right name in the right place.
See also the "system" manual:
In more complex situations, a separate @{verbatim 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.\
@{verbatim root.pdf} for target format @{verbatim 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.
You can take the document setup for this manual itself as an example:
Isabelle2015/src/Doc/ROOT and Isabelle2015/src/Doc/System -- that is not
the most simple version of such a "more complex situation", though.
Makarius
Email Gateway (Aug 22 2022 at 10:47):From: Gergely Buday <gbuday@gmail.com>
Hi,
I would like to use the glossaries LaTeX package through document
preparation.
It needs
pdflatex doc.tex
makeindex -s doc.ist -o doc.gls doc.glo
pdflatex doc.tex
to create the glossary in the document. isabelle latex in theory is capable
of running makeindex but it is not clear how the proper parameters can be
passed.
In lib/Tools/latex there is
function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; }
but FILEBASE is only
FILEBASE="$(basename "$FILE" .tex)"
An idea is to write a Makefile into output/document with the above command
sequence. Is there any better?
Isabelle2014's LaTeX does not have the glossaries package but I copied it
from my own installation with the dependencies.
Cheers
Last updated: Apr 20 2024 at 01:05 UTC