diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index c25f3303..73a9641d 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -666,142 +666,234 @@ fun check_result_inv oid {is_monitor:bool} ctxt = section*["document-templates"::technical]\Defining Document Templates\ +subsection\The Core Template\ text\ - Document-templates\index{document template} define the overall layout (page size, margins, fonts, + Document-templates\bindex{document template} define the overall layout (page size, margins, fonts, etc.) of the generated documents and are the the main technical means for implementing layout - requirements that are, \eg, required by publishers or standardization bodies. Document-templates + requirements that are, \eg, required by publishers or standardization bodies. + The common structure of an \isadof document template looks as follows: - - - -Current \isadof comes with a number of setups for the PDF generation, notably -Springer LNCS, lipics, ..., as well as setupqs of technical reports this the present one. - -The question arises, what to do if \isadof has to be accoustomed to a new LaTeX style -file configuration in order to generate PDF. -\ -text\ -In theory, this is simple - in practice, the efforts required -depends mostly on two factors: - -\<^item> how compatible is the required LaTeX class with Isabelle's LateX - setup in general (e.g., does it work with an antique version - of \comment.sty\ required by Isabelle) - -\<^item> how much magic does the required LaTeX class wrt the title page - information (author, affiliation). - -\<^item> which ontologies should be supported. While most ontologies are - generic, some only support a very specific subset of LaTeX - templates (classes). For example, \<^theory_text>\scholarly_paper\ does currently - \<^emph>\only\ support \llncs\, \rartcl\, and \lipics\. - -The general process as such is straight-forward: - -\<^enum> From the supported LaTeX classes, try to find the one that is - most similar to the one that you want to support. For the sake - of the this example, let's assume this is llncs -\<^enum> Use the template for this class (llncs) as starting point, i.e., - \<^verbatim>\cp document-generator/document-template/root-lncs.tex - document-generator/document-template/root-eptcs.tex\ - - The mandatory naming scheme for the templates is - - \<^verbatim>\root-.tex\ - - That is to say that \<^verbatim>\\ should be the name of the - new LaTeX class (all lowercase preferred) that will be used - in config files and also will be shown in the help text - shown by executing - - \<^verbatim>\isabelle mkroot_DOF -h\ - -\<^enum> Edit the new template as necessary (using the provided - example from the target class as reference): - - \<^verbatim>\vim document-generator/document-template/root-foo.tex\ - - and do the needful. - -\<^enum> Install the new template: - - \<^verbatim>\./install\ - - (If you have a working installation of the required AFP entries - and the Isabelle/DOF patch, you can use \<^verbatim>\./install -s\ - which will \<^emph>\ONLY\ install the \<^verbatim>\LaTeX styles/templates\, see - \<^verbatim>\./install -h)\ - -\<^enum> Now the new template should be available, you can check this with - - \<^verbatim>\isabelle mkroot_DOF -h\ - -\<^enum> Create an "tiny/empty" Isabelle project using the ontology "core" - and test your template. If everything works, celebrate. If it does - not work, understand what you need to change and continue - with step 3. - - (of course, if the new class is not available in TeXLive, you need - to add them locally to the documents folder of your Isabelle - project and, as usual, it needs to be registered in your ROOTS - file) - -\<^enum> If the ontologies that should be used together with this LaTeX - class do not require specific adaptions (e.g., CENELEC 50128), - everything should work. If one of the required ontology LaTeX - setups only supports a subset of LaTeX classes (e.g., \<^theory_text>\scholarly_paper\ - due to the different setups for authors/affiliations blurb), - you need to develop support for you new class in the ontology - specific LaTeX styles, e.g., - \document-generator/latex/DOF-scholarly_paper.sty\ - (mandatory naming convention: \DOF-.sty\) - -\<^enum> After updating the ontology style (or styles), you need - to install them (again, you might want to use ./install -s) - and test your setup with a paper configuration using - your new LaTeX template and the required styles. In case - of errors, go back to step 7. - -\begin{ltx} -\documentclass{article} -\usepackage[T1]{fontenc} -\usepackage[utf8]{inputenc} -\usepackage{isabelle} +\begin{ltx}[escapechar=ë, numbers=left,numberstyle=\tiny,xleftmargin=5mm] +\documentclass{article} % The LaTeX-class of your template ë\label{lst:dc}ë +%% The following part is (mostly) required by Isabelle/DOF, do not modify +\usepackage[T1]{fontenc} % Font encoding +\usepackage[utf8]{inputenc} % UTF8 support +\usepackage{isabelle} % Required (by Isabelle) \usepackage{xcolor} -\usepackage{isabellesym} -\usepackage{amsmath} -\usepackage{amssymb} -\IfFileExists{DOF-core.sty}{}{% +\usepackage{isabellesym} % Required (by Isabelle) +\usepackage{amsmath} % Used by some ontologies +\usepackage{amssymb} % Strongly recommended (by Isabelle) +\bibliographystyle{abbrv} +\IfFileExists{DOF-core.sty}{}{ % Required by Isabelle/DOF \PackageError{DOF-core}{Isabelle/DOF not installed. - This is a Isabelle_DOF project. The document preparation requires - the Isabelle_DOF framework. Please obtain the framework by cloning - the Isabelle_DOF git repository, i.e.: - "git clone https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF" - You can install the framework as follows: - "cd Isabelle_DOF/document-generator && ./install"}{% + This is a Isabelle_DOF project. The doëëcument preparation requires + the Isabelle_DOF framework. }{% For further help, see https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF} } -\input{ontologies} -\IfFileExists{preamble.tex}{\input{preamble.tex}}{}% -\usepackage{graphicx} -\usepackage{hyperref} -\urlstyle{rm} -\isabellestyle{it} +\input{ontologies} % This will include the document specific + % ontologies from isadof.cfg +\IfFileExists{preamble.tex} % Include preamble.tex, if it exists. + {\input{preamble.tex}}{} +\usepackage{graphicx} % Required for images. \usepackage[caption]{subfig} \usepackage[size=footnotesize]{caption} +\usepackage{hyperref} % Required by Isabelle/DOF +%% Begin of template specific configuration ë\label{lst:config-start}ë +\urlstyle{rm} +\isabellestyle{it} ë\label{lst:config-end}ë + +%% Main document, do not modify \begin{document} \maketitle \input{session} -% optional bibliography -\IfFileExists{root.bib}{% - \bibliographystyle{abbrv} - \bibliography{root} -}{} +\IfFileExists{root.bib}{\bibliography{root}}{} \end{document} \end{ltx} + + If a new layout is already supported by a \LaTeX-class, then developing basic support for it + is straight forwards: after reading the authors guidelines of the new template, + Developing basic support for a new document template is straight forwards In most cases, it is + sufficient to replace the document class in \autoref{lst:dc} of the template and add the + \LaTeX-packages that are (strictly) required by the used \LaTeX-setup. In general, we recommend + to only add \LaTeX-packages that are always necessary fro this particular template, as loading + packages in the templates minimizes the freedom users have by adapting the \path{preample.tex}. + Moreover, you might want to add/modify the template specific configuration + (\autoref{lst:config-start}-\ref{lst:config-end}). The new template should be stored in + \path{src/document-templates} and its file name should start with the prefix \path{root-}. After + adding a new template, call the \inlinebash{install} script (see @{docref "infrastructure"} +\ + +subsection\Tips, Tricks, and Known Limitations\ +text\ + For readers with basic knowledge of \LaTeX{}, adapting existing templates and ontologies) to + support new layouts should be rather straight forward, there are several things to consider that + we discuss in this section. +\ + +subsubsection\Getting Started\ +text\ + In general, we recommend to create a test project (\eg, using \inlinebash|isabelle mkroot_DOF|) + to develop new document templates or ontology representations. The default setup of the \isadof + build system generated a \path{output/document} directory with a self-contained \LaTeX-setup. In + this directory, you can directly use \LaTeX on the main file, called \path{root.tex}: + +\begin{bash} +ë\prompt{MyProject/output/document}ë pdflatex root.tex +\end{bash} + + This allows you to develop and check your \LaTeX-setup without the overhead of running + \inlinebash|isabelle build| after each change of your template (or ontology-style). Note that + the content of the \path{output} directory is overwritten by executing + \inlinebash|isabelle build|. +\ + +subsubsection\Truncated Warning and Error Messages\ +text\ + By default, \LaTeX{} cuts of many warning or error messages after 79 characters. Due to the + use of full-qualified names in \isadof, this can often result in important information being + cut off. Thus, it can be very helpful to configure \LaTeX{} in such a way that it prints + long error or warning messages. This can easily be done on the command line for individual + \LaTeX{} invocations: + +\begin{bash} +ë\prompt{MyProject/output/document}ë max_print_line=200 error_line=200 half_error_line=100 pdflatex root.tex +\end{bash} +\ + +subsubsection\Deferred Declaration of Information\ +text\ + During document generation, sometimes, information needs to be printed prior to its + declaration in a \isadof theory. This violation the declaration-before-use-principle + requires that information is written into an auxiliary file during the first run of \LaTeX{} + so that the information is available at further runs of \LaTeX{}. While, on the one hand, + this is a standard process (\eg, used for updating references), implementing it correctly + requires a solid understanding of \LaTeX's expansion mechanism. In this context, the recently + introduced \inlineltx|\expanded{}|-primitive + (see \url{https://www.texdev.net/2018/12/06/a-new-primitive-expanded}) is particularly useful. + Examples of its use can be found, \eg, in the ontology-styles + \path{ontologies/scholarly_paper/DOF-scholarly_paper.sty} or + \path{ontologies/CENELEC_50128/DOF-CENELEC_50128.sty}. For details about the expansion mechanism + in general, we refer the reader to the \LaTeX{} literature (\eg,~@{cite "knuth:texbook:1986" + and "mittelbach.ea:latex:1999" and "eijkhout:latex-cs:2012"}). +\ + + +subsubsection\Authors and Affiliation Information\ +text\ + In the context of academic papers, the defining the representations for the author and + affiliation information is particularly challenges as, firstly, they inherently are breaking + the declare-before-use-principle and, secondly, each publisher uses a different \LaTeX-setup + for their declaration. Moreover, the mapping from the ontological modeling to the document + representation might also need to bridge the gap between different common modeling styles of + authors and their affiliations, namely: affiliations as attributes of authors vs. authors and + affiliations both as entities with a many-to-many relationship. + + The ontology representation + \path{ontologies/scholarly_paper/DOF-scholarly_paper.sty} contains an example that, firstly, + shows how to write the author and affiliation information into the auxiliary file for re-use + in the next \LaTeX-run and, secondly, shows how to collect the author and affiliation + information into an \inlineltx|\author| and a \inlineltx|\institution| statement, each of + which containing the information for all authors. The collection of the author information + is provided by the following \LaTeX-code: + +\begin{ltx} +\def\dof@author{}% +\newcommand{\DOFauthor}{\author{\dof@author}} +\AtBeginDocument{\DOFauthor} +\def\leftadd#1#2{\expandafter\leftaddaux\expandafter{#1}{#2}{#1}} +\def\leftaddaux#1#2#3{\gdef#3{#1#2}} +\newcounter{dof@cnt@author} +\newcommand{\addauthor}[1]{% + \ifthenelse{\equal{\dof@author}{}}{% + \gdef\dof@author{#1}% + }{% + \leftadd\dof@author{\protect\and #1}% + } +} +\end{ltx} + +The new command \inlineltx|\addauthor| and a similarly defined command \inlineltx|\addaffiliation| +can now be used in the definition of the representation of the concept +\inlineisar|text.scholarly_paper.author|, which writes the collected information in the +job's aux-file. The intermediate step of writing this information into the job's aux-file is necessary, +as the author and affiliation information is required right at the begin of the document +(\ie, when \LaTeX's \inlineltx|\maketitle| is invoked) while \isadof allows to define authors at +any place within a document: + +\begin{ltx} +\provideisadof{text.scholarly_paper.author}% +[label=,type=% +,scholarly_paper.author.email=% +,scholarly_paper.author.affiliation=% +,scholarly_paper.author.orcid=% +,scholarly_paper.author.http_site=% +][1]{% + \stepcounter{dof@cnt@author} + \def\dof@a{\commandkey{scholarly_paper.author.affiliation}} + \ifthenelse{\equal{\commandkey{scholarly_paper.author.orcid}}{}}{% + \immediate\write\@auxout% + {\noexpand\addauthor{#1\noexpand\inst{\thedof@cnt@author}}}% + }{% + \immediate\write\@auxout% + {\noexpand\addauthor{#1\noexpand% + \inst{\thedof@cnt@author}% + \orcidID{\commandkey{scholarly_paper.author.orcid}}}}% + } + \protected@write\@auxout{}{% + \string\addaffiliation{\dof@a\\\string\email{% + \commandkey{scholarly_paper.author.email}}}}% +} +\end{ltx} + +Finally, the collected information is used in the \inlineltx|\author| command using the +\inlineltx|AtBeginDocument|-hook: + +\begin{ltx} +\newcommand{\DOFauthor}{\author{\dof@author}} +\AtBeginDocument{% + \DOFauthor +} + +\end{ltx} + + +\ + +subsubsection\Restricting the Use of Ontologies to Specific Templates\ + +text\ + As ontology representations might rely on features only provided by certain templates + (\LaTeX-classes), authors of ontology representations might restrict their use to + specific classes. This can, \eg, be done using the \inlineltx|\@ifclassloaded{}| command: + +\begin{ltx} +\@ifclassloaded{llncs}{}% +{% LLNCS class not loaded + \PackageError{DOF-scholarly_paper} + {Scholarly Paper only supports LNCS as document class.}{}\stop% +} +\end{ltx} + + For a real-world example testing for multiple classes, see + \path{ontologies/scholarly_paper/DOF-scholarly_paper.sty}): + + We encourage this clear and machine-checkable enforcement of restrictions while, at the same + time, we also encourage to provide a package option to overwrite them. The latter allows + inherited ontologies to overwrite these restrictions and, therefore, to provide also support + for additional document templates. For example, the ontology \inlineisar|technical_report| + extends the \inlineisar|scholarly_paper| ontology and its \LaTeX supports provides support + for the \inlineltx|scrrept|-class which is not supported by the \LaTeX support for + \inlineisar|scholarly_paper|. +\ + +subsubsection\Outdated Version of \path{comment.sty}\ +text\ + Isabelle's \LaTeX-setup relies on an ancient version of \path{comment.sty} that, moreover, + is used in plain\TeX-mode. This is known to cause issues with some modern \LaTeX-classes + such as LPICS. Such a conflict might require the help of an Isabelle wizard. \ diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex b/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex index 56344f65..f10bcab7 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex +++ b/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex @@ -124,5 +124,5 @@ France, and therefore granted with public funds of the Program ``Investissements \end{minipage} } -\AtBeginDocument{\isabellestyle{literal}} +\AtBeginDocument{\isabellestyle{literal}\newcommand{\lstnumberautorefname}{Line}} \renewcommand{\isacommand}[1]{\textcolor{OliveGreen!60}{\ttfamily\bfseries #1}} diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/root.bib b/examples/technical_report/Isabelle_DOF-Manual/document/root.bib index 40c1d21d..9097cb9b 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/document/root.bib +++ b/examples/technical_report/Isabelle_DOF-Manual/document/root.bib @@ -606,3 +606,27 @@ for commands and environments in {\LaTeX}.}, year = 2010 } + +@book{knuth:texbook:1986, + author = {Knuth, Donald E.}, + title = {The TeXbook}, + year = {1986}, + isbn = {0201134470}, + publisher = {Addison-Wesley Professional}, +} + +@book{mittelbach.ea:latex:1999, + author = {Mittelbach, Frank and Goossens, Michel and Braams, Johannes and Carlisle, David and Rowley, Chris}, + title = {The LaTeX Companion (Tools and Techniques for Computer Typesetting)}, + year = {2004}, + isbn = {0201362996}, + edition = {2nd}, + publisher = {Addison-Wesley Longman Publishing Co., Inc.}, + address = {Boston, MA, USA}, +} + +@book{ eijkhout:latex-cs:2012, + author={Victor Eijkhout}, + title={The Computer Science of TeX and LaTeX}, + year=2012, +}