2019-08-15 14:09:55 +00:00
(*************************************************************************
* Copyright (C)
* 2019 The University of Exeter
* 2018-2019 The University of Paris-Saclay
* 2018 The University of Sheffield
*
* License:
* This program can be redistributed and/or modified under the terms
* of the 2-clause BSD-style license.
*
* SPDX-License-Identifier: BSD-2-Clause
*************************************************************************)
2019-07-17 13:41:03 +00:00
(*<*)
2019-08-04 19:06:45 +00:00
theory
"03_GuidedTour"
imports
"02_Background"
"Isabelle_DOF.CENELEC_50128"
2019-07-17 13:41:03 +00:00
begin
(*>*)
2020-08-26 15:08:45 +00:00
chapter*[isadof_tour::text_section]\<open>\<^isadof>: A Guided Tour\<close>
2019-07-18 20:40:55 +00:00
2019-08-04 12:37:57 +00:00
text\<open>
2020-08-26 15:08:45 +00:00
In this chapter, we will give a introduction into using \<^isadof> for users that want to create and
2019-08-04 12:37:57 +00:00
maintain documents following an existing document ontology.
\<close>
2019-07-18 20:40:55 +00:00
2019-08-03 20:36:06 +00:00
section*[getting_started::technical]\<open>Getting Started\<close>
2019-08-18 13:05:00 +00:00
text\<open>
2020-08-26 15:08:45 +00:00
As an alternative to installing \<^isadof>{} locally, the latest official release \<^isadof> is also
available on \href{https://cloud.docker.com/u/logicalhacking/}{Docker Hub}. Thus, if you have
\href{https://www.docker.com}{Docker} installed and
your installation of Docker supports X11 application, you can start \<^isadof> as follows:
2019-08-18 13:05:00 +00:00
2020-08-28 15:41:16 +00:00
@{boxed_bash [display]
\<open>ë\prompt{}ë docker run -ti --rm -e DISPLAY=$DISPLAY \
2019-08-18 17:02:54 +00:00
-v /tmp/.X11-unix:/tmp/.X11-unix \
logicalhacking/isabelle_dof-ë\doflatestversionë_ë\MakeLowercase{\isabellelatestversion}ë \
isabelle jedit
2020-08-28 15:41:16 +00:00
\<close>}
2019-08-18 13:05:00 +00:00
\<close>
2019-08-03 20:36:06 +00:00
2019-08-04 12:37:57 +00:00
subsection*[installation::technical]\<open>Installation\<close>
text\<open>
2020-08-26 15:08:45 +00:00
In this section, we will show how to install \<^isadof> and its pre-requisites: Isabelle and
\<^LaTeX>. We assume a basic familiarity with a Linux/Unix-like command line (i.e., a shell).
2019-08-04 12:37:57 +00:00
\<close>
2019-07-18 20:40:55 +00:00
2019-08-04 17:15:30 +00:00
subsubsection*[prerequisites::technical]\<open>Pre-requisites\<close>
2019-08-04 12:37:57 +00:00
text\<open>
2020-08-26 15:08:45 +00:00
\<^isadof> has to major pre-requisites:
2020-08-28 15:41:16 +00:00
\<^item> \<^bold>\<open>Isabelle\<close>\<^bindex>\<open>Isabelle\<close> (\isabellefullversion).
\<^isadof> uses a two-part version system (e.g., 1.0.0/2020), where the first part is the version
of \<^isadof> (using semantic versioning) and the second part is the supported version of Isabelle.
Thus, the same version of \<^isadof> might be available for different versions of Isabelle.
\<^item> \<^bold>\<open>\<^TeXLive> 2020\<close>\<^bindex>\<open>TexLive@\<^TeXLive>\<close> (or any other modern \<^LaTeX>-distribution where
\<^pdftex> supports the \<^boxed_latex>\<open>\expanded\<close> primitive).
2020-08-26 15:08:45 +00:00
\<^footnote>\<open>see \<^url>\<open>https://www.texdev.net/2018/12/06/a-new-primitive-expanded\<close>\<close>
2019-08-04 12:37:57 +00:00
\<close>
2019-07-18 20:40:55 +00:00
2019-08-04 12:37:57 +00:00
paragraph\<open>Installing Isabelle\<close>
text\<open>
2020-08-28 15:41:16 +00:00
%\enlargethispage{\baselineskip}
2019-08-04 12:37:57 +00:00
Please download and install the Isabelle \isabelleversion distribution for your operating system
2019-08-13 07:55:57 +00:00
from the \href{\isabelleurl}{Isabelle website} (\url{\isabelleurl}). After the successful
2020-08-28 15:41:16 +00:00
installation of Isabelle, you should be able to call the \<^boxed_bash>\<open>isabelle\<close> tool on the
2019-08-04 12:37:57 +00:00
command line:
\begin{bash}
ë\prompt{}ë isabelle version
ë\isabellefullversionë
\end{bash}
2020-08-28 15:41:16 +00:00
% bu : do not know why this does not work here ...
%@ {boxed_bash [display]\<open>
%ë\prompt{}ë isabelle version
%ë\isabellefullversionë
%\<close>}
Depending on your operating system and depending if you put Isabelle's \<^boxed_bash>\<open>bin\<close> directory
in your \<^boxed_bash>\<open>PATH\<close>, you will need to invoke \<^boxed_bash>\<open>isabelle\<close> using its
2020-08-26 15:08:45 +00:00
full qualified path, \<^eg>:
2019-07-18 20:40:55 +00:00
2019-08-04 12:37:57 +00:00
\begin{bash}
2019-08-14 19:04:37 +00:00
ë\prompt{}ë /usr/local/Isabelleë\isabelleversion/ëbin/isabelle version
2019-08-04 12:37:57 +00:00
ë\isabellefullversionë
\end{bash}
2020-08-28 15:41:16 +00:00
%@ {boxed_bash [display]\<open>
%ë\prompt{}ë /usr/local/Isabelleë\isabelleversion/ëbin/isabelle version
%ë\isabellefullversionë
%\<close>}
2019-08-04 12:37:57 +00:00
\<close>
2020-08-28 15:41:16 +00:00
paragraph\<open>Installing \<^TeXLive>\<close>
2019-08-04 12:37:57 +00:00
text\<open>
2020-08-28 15:41:16 +00:00
Modern Linux distribution will allow you to install \<^TeXLive> using their respective package
2020-08-26 15:08:45 +00:00
managers. On a modern Debian system or a Debian derivative (\<^eg>, Ubuntu), the following command
should install all required \<^LaTeX> packages:
2019-08-04 12:37:57 +00:00
\begin{bash}
2019-08-12 07:33:17 +00:00
ë\prompt{}ë sudo aptitude install texlive-latex-extra texlive-fonts-extra
2019-08-04 12:37:57 +00:00
\end{bash}
2020-08-28 15:41:16 +00:00
%@ {boxed_bash [display]\<open>
%ë\prompt{}ë sudo aptitude install texlive-latex-extra texlive-fonts-extra
%\<close>}
2019-08-04 12:37:57 +00:00
2020-08-26 15:08:45 +00:00
Please check that this, indeed, installs a version of \<^pdftex> that supports the
2020-08-28 15:41:16 +00:00
\<^boxed_latex>\<open>\expanded\<close>. To check your \<^pdftex>-binary, execute
2019-08-04 12:37:57 +00:00
\begin{bash}
ë\prompt{}ë pdftex \\expanded{Success}\\end
2019-08-14 19:04:37 +00:00
This is pdfTeX, Version 3.14159265-2.6-1.40.20 (TeX Live 2019/Debian).
2019-08-04 12:37:57 +00:00
Output written on texput.pdf (1 page, 8650 bytes).
Transcript written on texput.log.
\end{bash}
2020-08-28 15:41:16 +00:00
%@ {boxed_bash [display]\<open>
%ë\prompt{}ë pdftex \\expanded{Success}\\end
%This is pdfTeX, Version 3.14159265-2.6-1.40.20 (TeX Live 2019/Debian).
%Output written on texput.pdf (1 page, 8650 bytes).
%Transcript written on texput.log.
%\<close>}
2019-08-04 12:37:57 +00:00
2020-08-26 15:08:45 +00:00
If this generates successfully a file \inlinebash|texput.pdf|, your \<^pdftex>-binary supports
2020-08-28 15:41:16 +00:00
the \<^boxed_latex>\<open>\expanded\<close>-primitive. If your Linux distribution does not (yet) ship \<^TeXLive>
2020-08-26 15:08:45 +00:00
2019 or your are running Windows or OS X, please follow the installation instructions from
\<^url>\<open>https://www.tug.org/texlive/acquire-netinstall.html\<close>.
2019-08-04 12:37:57 +00:00
\<close>
2020-08-26 15:08:45 +00:00
subsubsection*[isadof::technical]\<open>Installing \<^isadof>\<close>
2019-08-03 20:36:06 +00:00
text\<open>
2020-08-26 15:08:45 +00:00
In the following, we assume that you already downloaded the \<^isadof> distribution
(\href{\isadofarchiveurl}{\isadofarchiven}) from the \<^isadof> web site. The main steps for
installing are extracting the \<^isadof> distribution and calling its \inlinebash|install| script.
We start by extracting the \<^isadof> archive:
2019-08-04 12:37:57 +00:00
2019-07-18 20:40:55 +00:00
\begin{bash}
2019-08-03 20:36:06 +00:00
ë\prompt{}ë tar xf ë\href{\isadofarchiveurl}{\isadofarchiven}ë
2019-08-04 12:37:57 +00:00
\end{bash}
2020-08-26 15:08:45 +00:00
This will create a directory \texttt{\isadofdirn} containing \<^isadof> distribution.
2020-08-28 15:41:16 +00:00
Next, we need to invoke the \<^boxed_bash>\<open>install\<close> script. If necessary, the installations
automatically downloads additional dependencies from the AFP (\<^url>\<open>https://www.isa-afp.org\<close>),
2020-08-26 15:08:45 +00:00
namely the AFP entries ``Functional Automata''~@{cite "nipkow.ea:functional-Automata-afp:2004"}
and ``Regular Sets and Expressions''~@{cite "kraus.ea:regular-sets-afp:2010"}. This might take a
few minutes to complete. Moreover, the installation script applies a patch to the Isabelle system,
which requires \<^emph>\<open>write permissions for the Isabelle system directory\<close> and registers \<^isadof> as
Isabelle component.
2019-08-04 12:37:57 +00:00
2020-08-28 15:41:16 +00:00
If the \<^boxed_bash>\<open>isabelle\<close> tool is not in your \<^boxed_bash>\<open>PATH\<close>, you need to call the
\<^boxed_bash>\<open>install\<close> script with the \<^boxed_bash>\<open>--isabelle\<close> option, passing the full-qualified
path of the \<^boxed_bash>\<open>isabelle\<close> tool ( \<^boxed_bash>\<open>install --help\<close> gives
2019-08-04 12:37:57 +00:00
you an overview of all available configuration options):
\begin{bash}
2019-08-03 20:36:06 +00:00
ë\prompt{}ë cd ë\isadofdirnë
2019-08-04 12:37:57 +00:00
ë\prompt{\isadofdirn}ë ./install --isabelle /usr/local/Isabelleë\isabelleversion/bin/isabelleë
Isabelle/DOF Installer
======================
* Checking Isabelle version:
Success: found supported Isabelle version ë(\isabellefullversion)ë
2019-08-04 21:31:52 +00:00
* Checking (La)TeX installation:
Success: pdftex supports \expanded{} primitive.
2019-08-04 12:37:57 +00:00
* Check availability of Isabelle/DOF patch:
Warning: Isabelle/DOF patch is not available or outdated.
Trying to patch system ....
Applied patch successfully, Isabelle/HOL will be rebuilt during
the next start of Isabelle.
* Checking availability of AFP entries:
Warning: could not find AFP entry Regular-Sets.
Warning: could not find AFP entry Functional-Automata.
Trying to install AFP (this might take a few *minutes*) ....
Registering Regular-Sets iëën
/home/achim/.isabelle/Isabelleë\isabelleversion/ROOTSë
Registering Functional-Automata iëën
/home/achim/.isabelle/Isabelleë\isabelleversion/ROOTSë
AFP installation successful.
* Searching fëëor existing installation:
No old installation found.
* Installing Isabelle/DOF
- Installing Tools iëën
/home/achim/.isabelle/Isabelleë\isabelleversion/DOF/Toolsë
- Installing document templates iëën
/home/achim/.isabelle/Isabelleë\isabelleversion/DOF/document-templateë
- Installing LaTeX styles iëën
2019-08-10 19:43:29 +00:00
/home/achim/.isabelle/Isabelleë\isabelleversion/DOF/latexë
2019-08-04 12:37:57 +00:00
- Registering Isabelle/DOF
* Registering tools iëën
/home/achim/.isabelle/Isabelleë\isabelleversion/etc/settingsë
2019-08-04 21:31:52 +00:00
* Installation successful. Enjoy Isabelle/DOF, you can build the session
2019-08-17 22:27:04 +00:00
Isabelle/DOF and all example documents by executing:
2019-08-04 12:37:57 +00:00
/usr/local/Isabelleë\isabelleversion/bin/isabelleë build -D .
2019-07-18 20:40:55 +00:00
\end{bash}
2019-08-04 12:37:57 +00:00
After the successful installation, you can now explore the examples (in the sub-directory
\inlinebash|examples| or create your own project. On the first start, the session
\inlinebash|Isabelle_DOF| will be built automatically. If you want to pre-build this
session and all example documents, execute:
2019-07-18 20:40:55 +00:00
\begin{bash}
2019-08-04 12:37:57 +00:00
ë\prompt{\isadofdirn}ë isabelle build -D .
2019-07-18 20:40:55 +00:00
\end{bash}
\<close>
2020-08-26 15:08:45 +00:00
subsection*[first_project::technical]\<open>Creating an \<^isadof> Project\<close>
2019-08-04 12:37:57 +00:00
text\<open>
2020-08-26 15:08:45 +00:00
\<^isadof> provides its own variant of Isabelle's
2019-08-04 17:15:30 +00:00
\inlinebash|mkroot| tool, called \inlinebash|mkroot_DOF|:\index{mkroot\_DOF}
2019-08-04 12:37:57 +00:00
2019-08-04 14:32:16 +00:00
\begin{bash}
2019-08-04 12:37:57 +00:00
ë\prompt{}ë isabelle mkroot_DOF -h
Usage: isabelle mkroot_DOF [OPTIONS] [DIR]
Options are:
-h print this hëëelp text and exëëit
-n NAME alternative session name (default: DIR base name)
-o ONTOLOGY (default: scholarly_paper)
Available ontologies:
* CENELEC_50128
* math_exam
* scholarly_paper
* technical_report
-t TEMPLATE (default: scrartcl)
Available document templates:
* lncs
* scrartcl
* scrreprt-modern
* scrreprt
Prepare session root DIR (default: current directory).
2019-08-04 14:32:16 +00:00
\end{bash}
2019-08-04 12:37:57 +00:00
Creating a new document setup requires two decisions:
2020-08-26 15:08:45 +00:00
\<^item> which ontologies (\<^eg>, scholarly\_paper) are required and
2019-08-04 20:16:25 +00:00
\<^item> which document template (layout)\index{document template} should be used
2020-08-26 15:08:45 +00:00
(\<^eg>, scrartcl\index{scrartcl}). Some templates (\<^eg>, lncs) require that the users manually
obtains and adds the necessary \<^LaTeX> class file (\<^eg>, \inlinebash|llncs.cls|.
2019-08-04 20:16:25 +00:00
This is mostly due to licensing restrictions.
2019-08-04 12:37:57 +00:00
\<close>
text\<open>
If you are happy with the defaults, \ie, using the ontology for writing academic papers
(scholarly\_paper) using a report layout based on the article class (\inlineltx|scrartcl|) of
the KOMA-Script bundle~@{cite "kohm:koma-script:2019"}, you can create your first project
\inlinebash|myproject| as follows:
\begin{bash}
ë\prompt{}ë isabelle mkroot_DOF myproject
Preparing session "myproject" iëën "myproject"
creating "myproject/ROOT"
creating "myproject/document/root.tex"
Now use the following coëëmmand line to build the session:
isabelle build -D myproject
\end{bash}
2020-08-26 15:08:45 +00:00
This creates a directory \inlinebash|myproject| containing the \<^isadof>-setup for your
2019-08-04 12:37:57 +00:00
new document. To check the document formally, including the generation of the document in PDF,
2019-08-04 21:31:52 +00:00
you only need to execute
2019-08-04 12:37:57 +00:00
\begin{bash}
ë\prompt{}ë isabelle build -d . myproject
\end{bash}
2019-08-04 14:32:16 +00:00
This will create the directory \inlinebash|myproject|:
\begin{center}
\begin{minipage}{.9\textwidth}
\dirtree{%
.1 .
.2 myproject.
.3 document.
.4 build\DTcomment{Build Script}.
.4 isadof.cfg\DTcomment{\isadof configuraiton}.
2020-08-26 15:08:45 +00:00
.4 preamble.tex\DTcomment{Manual \<^LaTeX>-configuration}.
2019-08-04 14:32:16 +00:00
.3 ROOT\DTcomment{Isabelle build-configuration}.
}
\end{minipage}
\end{center}
2020-08-26 15:08:45 +00:00
The \<^isadof> configuration (\inlinebash|isadof.cfg|) specifies the required
2019-08-04 14:32:16 +00:00
ontologies and the document template using a YAML syntax.\<^footnote>\<open>Isabelle power users will recognize that
2020-08-26 15:08:45 +00:00
\<^isadof>'s document setup does not make use of a file \inlinebash|root.tex|: this file is
2019-08-04 14:32:16 +00:00
replaced by built-in document templates.\<close> The main two configuration files for
users are:
2020-08-28 15:41:16 +00:00
\<^item> The file \<^boxed_bash>\<open>ROOT\<close>\<^index>\<open>ROOT\<close>, which defines the Isabelle session. New theory files as well as new
files required by the document generation (\<^eg>, images, bibliography database using \<^BibTeX>, local
2020-08-26 15:08:45 +00:00
\<^LaTeX>-styles) need to be registered in this file. For details of Isabelle's build system, please
2020-04-08 20:40:34 +00:00
consult the Isabelle System Manual~@{cite "wenzel:system-manual:2020"}.
2020-08-28 15:41:16 +00:00
\<^item> The file \<^boxed_bash>\<open>praemble.tex\<close>\<^index>\<open>praemble.tex\<close>, which allows users to add additional
2020-08-26 15:08:45 +00:00
\<^LaTeX>-packages or to add/modify \<^LaTeX>-commands.
2019-08-04 12:37:57 +00:00
\<close>
2019-07-18 20:40:55 +00:00
2019-08-04 17:15:30 +00:00
section*[scholar_onto::example]\<open>Writing Academic Publications (scholarly\_paper)\<close>
2020-08-28 15:41:16 +00:00
subsection\<open>The Scholarly Paper Examples\<close>
2019-08-04 14:32:16 +00:00
text\<open>
2020-08-28 15:41:16 +00:00
The ontology ``scholarly\_paper''\<^index>\<open>ontology!scholarly\_paper\<close> is an ontology modeling
academic/scientific papers, with a slight bias to texts in the domain of mathematics and engineering.
We explain first the principles of its underlying ontology, and then we present two ''real''
example instances of our own.
\<^enum> The iFM 2020 paper~@{cite "taha.ea:philosophers:2020"} is a typical mathematical text, heavy in
definitions with complex mathematical notation and a lot of complex cross-referencing
between statements, definitions and proofs which is ontologically tracked. However, wrt.
to the possible linking between the underlying formal theory and this mathematical presentation,
it follows a pragmatic path without any ``deep'' linking to types, terms and theorems, deliberately
not exploiting \<^isadof>'s full potential with this regard.
\<^enum> In the CICM 2018 paper~@{cite "brucker.ea:isabelle-ontologies:2018"}, we deliberately
refrain from integrating references to formal content in order demonstrate that \<^isadof> is not
a framework from Isabelle users to Isabelle users only, but people just avoiding as much as
possible \<^LaTeX> notation.
The \<^isadof> distribution contains both examples using the ontology ``scholarly\_paper'' in
the directory \nolinkurl{examples/scholarly_paper/2018-cicm-isabelle_dof-applications/} or
\nolinkurl{examples/scholarly_paper/2020-ifm-csp-applications/}.
You can inspect/edit the example in Isabelle's IDE, by either
2020-08-26 15:08:45 +00:00
\<^item> starting Isabelle/jedit using your graphical user interface (\<^eg>, by clicking on the
2019-08-04 14:32:16 +00:00
Isabelle-Icon provided by the Isabelle installation) and loading the file
\nolinkurl{examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy}.
2020-08-28 15:41:16 +00:00
\<^item> starting Isabelle/jedit from the command line by,\<^eg>, calling:
2019-08-04 14:32:16 +00:00
\begin{bash}
ë\prompt{\isadofdirn}ë
isabelle jedit examples/scholarly_paper/2018-cicm-isabelle_dof-applications/\
IsaDofApplications.thy
\end{bash}
2019-08-04 19:06:45 +00:00
\<close>
2020-08-28 15:41:16 +00:00
(* We should discuss if we shouldn't put the iFM paper more in the foreground *)
2019-08-04 14:32:16 +00:00
2020-08-28 15:41:16 +00:00
text\<open> You can build the PDF-document at the command line by calling:
@{boxed_bash [display]
\<open>ë\prompt{}ë isabelle build \
2018-cicm-isabelle_dof-applications\<close>}
2019-08-04 17:15:30 +00:00
\<close>
2019-08-04 14:32:16 +00:00
2020-08-28 15:41:16 +00:00
subsection\<open>A Bluffers Guide to the "scholarly\_paper" Ontology\<close>
text\<open> In this section we give a minimal overview of the ontology formalized in
@{theory \<open>Isabelle_DOF.scholarly_paper\<close>}.\<close>
2019-08-04 14:32:16 +00:00
2020-08-28 15:41:16 +00:00
text\<open> We start by modeling the usual text-elements of an academic paper: the title and author
2019-08-04 17:15:30 +00:00
information, abstract, and text section:
2020-08-28 15:41:16 +00:00
@{theory_text [display]
\<open>doc_class title =
short_title :: "string option" <= "None"
2019-07-17 13:41:03 +00:00
doc_class subtitle =
2020-08-28 15:41:16 +00:00
abbrev :: "string option" <= "None"
2019-07-17 13:41:03 +00:00
doc_class author =
2020-08-28 15:41:16 +00:00
email :: "string" <= "''''"
http_site :: "string" <= "''''"
orcid :: "string" <= "''''"
2019-07-17 13:41:03 +00:00
affiliation :: "string"
doc_class abstract =
2020-08-28 15:41:16 +00:00
keywordlist :: "string list" <= "[]"
principal_theorems :: "thm list"\<close>}
\<close>
2019-07-17 13:41:03 +00:00
2020-08-28 15:41:16 +00:00
text\<open>Note \<open>short_title\<close> and \<open>abbrev\<close> are optional and have the default \<open>None\<close> (no value).
Note further, that abstracts may have a \<open>principal_theorems\<close> list, where the built-in \<^isadof> type
\<open>thm list\<close> which contain references to formally proven theorems that must exist in the logical
context of this document; this is a decisive feature of \<^isadof> that conventional ontological
languages lack.\<close>
text\<open>We continue by the introduction of a main class: the text-element \<open>text_section\<close> (in contrast
to \<open>figure\<close> or \<open>table\<close> or similar. Note that
the \<open>main_author\<close> is typed with the class \<open>author\<close>, a HOL type that is automatically derived from
the document class definition \<open>author\<close> shown above. It is used to express which author currently
``owns'' this \<open>text_section\<close>, an information that can give rise to presentational or even
access-control features in a suitably adapted front-end.
@{theory_text [display] \<open>
doc_class text_section = text_element +
2019-07-17 13:41:03 +00:00
main_author :: "author option" <= None
2020-08-28 15:41:16 +00:00
fixme_list :: "string list" <= "[]"
level :: "int option" <= "None"
\<close>}
2020-09-01 07:23:02 +00:00
The \<open>level\<close>-attibute \<^index>\<open>level\<close> enables doc-notation support for headers, chapters, sections, and
subsections; we follow here the \<^LaTeX> terminology on levels to which \<^isadof> is currently targeting at.
2020-08-28 15:41:16 +00:00
The values are interpreted accordingly to the \<^LaTeX> standard.
2020-09-01 07:23:02 +00:00
\<^enum> part \<^index>\<open>part\<close> \<^bigskip>\<^bigskip> \<open>Some -1\<close>
\<^enum> chapter \<^index>\<open>chapter\<close> \<^bigskip>\<^bigskip> \<open>Some 0\<close>
\<^enum> section \<^index>\<open>section\<close> \<^bigskip>\<^bigskip> \<open>Some 1\<close>
\<^enum> subsection \<^index>\<open>subsection\<close> \<^bigskip>\<^bigskip> \<open>Some 2\<close>
2020-08-28 15:41:16 +00:00
\<^enum> subsubsection \<^index>\<open>subsubsection\<close> \<^bigskip>\<^bigskip> \<open>Some 3\<close>
Additional means assure that the following invariant is maintained in a document
conforming to @{theory \<open>Isabelle_DOF.scholarly_paper\<close>}:
\center {\<open>level > 0\<close>}
\<close>
text\<open> The rest of the ontology introduces concepts for \<open>introductions\<close>, \<open>conclusion\<close>, \<open>related_work\<close>,
\<open>bibliography\<close> etc. More details can be found in \<close>
2020-09-01 07:23:02 +00:00
subsection\<open>Writing Academic Publications `I : A Mathematics Text \<close>
text*[csp_paper_synthesis::technical, main_author = "Some bu"]\<open>We present a typical mathematical
paper focussing on its form, not refering in any sense to its content which is out of scope here.
As mentioned before, we chose the paper~@{cite "taha.ea:philosophers:2020"} for this purpose.
The corpus of the beginning looks like this (the setup seaquence is described later):\<close>
(* . Focus: Mathematical content. Definition, theorem, and citations... *)
figure*[fig0::figure,spawn_columns=False,relative_width="95",src="''figures/header_CSP_source.png''"]
\<open> A mathematics paper as a document source ... \<close>
text\<open>The document build process converts this to the following \<^pdf>-output:\<close>
figure*[fig0B::figure,spawn_columns=False,relative_width="95",src="''figures/header_CSP_pdf.png''"]
\<open> \ldots and as its resulting \<^pdf>-output. \<close>
text\<open>Recall that the standard syntax for a text-element in \<^isadof> is
2020-09-02 13:35:38 +00:00
\<^theory_text>\<open>text*[<id>::<class_id>,<attrs>]\<open> ... text ...\<close>\<close>, but there are a few built-in abbreviations like
2020-09-01 07:23:02 +00:00
\<^theory_text>\<open>title*[<id>,<attrs>]\<open> ... text ...\<close>\<close> that provide special command-level syntax for text-elements.
The other text-elements provide the authors and the abstract as specified by their class-id referring
to the \<^theory_text>\<open>doc_class\<close>es of \<^verbatim>\<open>scholarly_paper\<close>; we say that these text elements are \<^emph>\<open>instances\<close>
2020-09-02 13:35:38 +00:00
\<^bindex>\<open>instance\<close> of the \<^theory_text>\<open>doc_class\<close>es \<^bindex>\<open>doc\_class\<close> of the underlying ontology. \<close>
text\<open>The paper proceeds by providing instances for introduction, technical sections, examples, \<^etc>.
We would like to concentrate on one --- mathematical paper oriented --- detail in the ontology
\<^verbatim>\<open>scholarly_paper\<close>:
@{theory_text [display]
\<open>doc_class technical = text_section +
. . .
type_synonym tc = technical (* technical content *)
datatype math_content_class = "defn" | "axm" | "thm" | "lem" | "cor" | "prop" | ...
doc_class math_content = tc +
...
doc_class "definition" = math_content +
mcc :: "math_content_class" <= "defn"
...
doc_class "theorem" = math_content +
mcc :: "math_content_class" <= "thm"
...
\<close>}\<close>
text\<open>The class \<^verbatim>\<open>technical\<close> regroups a number of text-elements that contain typical
"technical content" in mathematical or engineering papers: code, definitions, theorems,
lemmas, examples. From this class, the more stricter class of @{typ \<open>math_content\<close>} is derived,
which is grouped into @{typ "definition"}s and @{typ "theorem"}s (the details of these
class definitions are omitted here). Note, however, that class identifiers can be abbreviated by
standard \<^theory_text>\<open>type_synonym\<close>s for convenience and enumeration types can be defined by the
standard inductive \<^theory_text>\<open>datatype\<close> definition mechanism in Isabelle, since any HOL type is admitted
for attibute declarations. Vice-versa, document class definitions imply a corresponding HOL type
definition. \<close>
2020-09-01 07:23:02 +00:00
2020-08-28 15:41:16 +00:00
subsection\<open>Writing Academic Publications II (somewhat outdated)\<close>
2020-09-01 07:23:02 +00:00
text\<open> In our next example we concentrate on non-text-elements. Focus on Figures...
2019-08-04 17:15:30 +00:00
\<close>
2019-07-17 13:41:03 +00:00
figure*[fig1::figure,spawn_columns=False,relative_width="95",src="''figures/Dogfood-Intro''"]
\<open> Ouroboros I: This paper from inside \ldots \<close>
2019-08-04 17:15:30 +00:00
text\<open>
@{docitem \<open>fig1\<close>} shows the corresponding view in the Isabelle/jedit of the start of an academic
2020-08-26 15:08:45 +00:00
paper. The text uses \<^isadof>'s own text-commands containing the meta-information provided by the
2020-09-08 06:30:14 +00:00
underlying ontology. We proceed by a definition of \<^boxed_theory_text>\<open>introduction\<close>'s, which we define
as the extension of \<^boxed_theory_text>\<open>text_section\<close> which is intended to capture common infrastructure:
2019-08-04 17:15:30 +00:00
2020-09-08 05:18:01 +00:00
@{boxed_theory_text [display]\<open>
2019-07-17 13:41:03 +00:00
doc_class introduction = text_section +
comment :: string
2020-09-08 05:18:01 +00:00
\<close>}
2019-07-17 13:41:03 +00:00
2020-09-08 06:30:14 +00:00
As a consequence of the definition as extension, the \<^boxed_theory_text>\<open>introduction\<close> class
inherits the attributes \<^boxed_theory_text>\<open>main_author\<close> and \<^boxed_theory_text>\<open>todo_list\<close>
together with the corresponding default values.
2019-08-04 17:15:30 +00:00
We proceed more or less conventionally by the subsequent sections:
2019-07-17 13:41:03 +00:00
2020-09-08 05:18:01 +00:00
@{boxed_theory_text [display]\<open>
2019-07-17 13:41:03 +00:00
doc_class technical = text_section +
definition_list :: "string list" <= "[]"
doc_class example = text_section +
comment :: string
doc_class conclusion = text_section +
main_author :: "author option" <= None
doc_class related_work = conclusion +
main_author :: "author option" <= None
2020-09-08 05:18:01 +00:00
\<close>}
2019-08-04 17:15:30 +00:00
Moreover, we model a document class for including figures (actually, this document class is already
2020-08-26 15:08:45 +00:00
defined in the core ontology of \<^isadof>):
2019-08-04 17:15:30 +00:00
2020-09-08 05:18:01 +00:00
@{boxed_theory_text [display]\<open>
2019-08-04 17:15:30 +00:00
datatype placement = h | t | b | ht | hb
doc_class figure = text_section +
2019-08-17 09:07:08 +00:00
relative_width :: "int" (* percent of textwidth *)
src :: "string"
placement :: placement
spawn_columns :: bool <= True
2020-09-08 05:18:01 +00:00
\<close>}
2019-08-04 17:15:30 +00:00
\<close>
figure*[fig_figures::figure,spawn_columns=False,relative_width="85",src="''figures/Dogfood-figures''"]
\<open> Ouroboros II: figures \ldots \<close>
text\<open>
2020-09-08 06:30:14 +00:00
The document class \<^boxed_theory_text>\<open>figure\<close> (supported by the \<^isadof> command
\<^boxed_theory_text>\<open>figure*\<close>) makes it possible to express the pictures and diagrams
such as @{docitem \<open>fig_figures\<close>}.
2019-08-04 17:15:30 +00:00
Finally, we define a monitor class definition that enforces a textual ordering
in the document core by a regular expression:
2020-09-08 05:18:01 +00:00
@{boxed_theory_text [display]\<open>
2019-07-17 13:41:03 +00:00
doc_class article =
2019-08-17 08:48:15 +00:00
style_id :: string <= "''LNCS''"
version :: "(int \<times> int \<times> int)" <= "(0,0,0)"
2019-07-17 13:41:03 +00:00
where "(title ~~ \<lbrakk>subtitle\<rbrakk> ~~ \<lbrace>author\<rbrace>$^+$+ ~~ abstract ~~
introduction ~~ \<lbrace>technical || example\<rbrace>$^+$ ~~ conclusion ~~
bibliography)"
2020-09-08 05:18:01 +00:00
\<close>}
2019-07-17 13:41:03 +00:00
\<close>
2019-08-04 17:15:30 +00:00
subsection*[scholar_pide::example]\<open>Editing Support for Academic Papers\<close>
side_by_side_figure*[exploring::side_by_side_figure,anchor="''fig-Dogfood-II-bgnd1''",
caption="''Exploring a reference of a text-element.''",relative_width="48",
src="''figures/Dogfood-II-bgnd1''",anchor2="''fig-bgnd-text_section''",
caption2="''Exploring the class of a text element.''",relative_width2="47",
src2="''figures/Dogfood-III-bgnd-text_section''"]\<open>Exploring text elements.\<close>
2019-07-17 13:41:03 +00:00
2019-08-04 17:15:30 +00:00
side_by_side_figure*["hyperlinks"::side_by_side_figure,anchor="''fig:Dogfood-IV-jumpInDocCLass''",
caption="''Hyperlink to class-definition.''",relative_width="48",
src="''figures/Dogfood-IV-jumpInDocCLass''",anchor2="''fig:Dogfood-V-attribute''",
caption2="''Exploring an attribute.''",relative_width2="47",
src2="''figures/Dogfood-III-bgnd-text_section''"]\<open> Hyperlinks.\<close>
text\<open>
2020-08-26 15:08:45 +00:00
From these class definitions, \<^isadof> also automatically generated editing
2019-08-04 17:15:30 +00:00
support for Isabelle/jedit. In \autoref{fig-Dogfood-II-bgnd1} and
\autoref{fig-bgnd-text_section} we show how hovering over links permits to explore its
meta-information. Clicking on a document class identifier permits to hyperlink into the
corresponding class definition (\autoref{fig:Dogfood-IV-jumpInDocCLass}); hovering over an
attribute-definition (which is qualified in order to disambiguate;
\autoref{fig:Dogfood-V-attribute}).
\<close>
2020-08-28 15:41:16 +00:00
(* Bu : This autoref stuff could be avoided if we would finally have monitors... *)
2019-08-04 17:15:30 +00:00
figure*[figDogfoodVIlinkappl::figure,relative_width="80",src="''figures/Dogfood-V-attribute''"]
\<open> Exploring an attribute (hyperlinked to the class). \<close>
text\<open>
2020-08-26 15:08:45 +00:00
An ontological reference application in @{figure "figDogfoodVIlinkappl"}: the
2020-09-08 06:30:14 +00:00
ontology-dependant antiquotation \<^boxed_theory_text>\<open>@ {example ...}\<close> refers to the corresponding
2019-08-04 17:15:30 +00:00
text-elements. Hovering allows for inspection, clicking for jumping to the definition. If the
link does not exist or has a non-compatible type, the text is not validated.
2019-07-17 13:41:03 +00:00
\<close>
2019-07-17 19:10:18 +00:00
2019-08-04 17:15:30 +00:00
section*[cenelec_onto::example]\<open>Writing Certification Documents (CENELEC\_50128)\<close>
2019-08-04 19:06:45 +00:00
subsection\<open>The CENELEC 50128 Example\<close>
text\<open>
The ontology ``CENELEC\_50128''\index{ontology!CENELEC\_50128} is a small ontology modeling
documents for a certification following CENELEC 50128~@{cite "boulanger:cenelec-50128:2015"}.
2020-08-26 15:08:45 +00:00
The \<^isadof> distribution contains a small example using the ontology ``CENELEC\_50128'' in
2019-08-04 19:34:22 +00:00
the directory \nolinkurl{examples/CENELEC_50128/mini_odo/}. You can inspect/edit the example
2019-08-04 19:06:45 +00:00
in Isabelle's IDE, by either
2020-08-26 15:08:45 +00:00
\<^item> starting Isabelle/jedit using your graphical user interface (\<^eg>, by clicking on the
2019-08-04 19:06:45 +00:00
Isabelle-Icon provided by the Isabelle installation) and loading the file
\nolinkurl{examples/CENELEC_50128/mini_odo/mini_odo.thy}.
\<^item> starting Isabelle/jedit from the command line by calling:
\begin{bash}
ë\prompt{\isadofdirn}ë
isabelle jedit examples/CENELEC_50128/mini_odo/mini_odo.thy
\end{bash}
\<close>
text\<open>
You can build the PDF-document by calling:
\begin{bash}
ë\prompt{}ë isabelle build mini_odo
\end{bash}
2019-07-17 19:10:18 +00:00
\<close>
2019-08-04 19:06:45 +00:00
subsection\<open>Modeling CENELEC 50128\<close>
text\<open>
Documents to be provided in formal certifications (such as CENELEC
50128~@{cite "boulanger:cenelec-50128:2015"} or Common Criteria~@{cite "cc:cc-part3:2006"}) can
much profit from the control of ontological consistency: a lot of an evaluators work consists in
tracing down the links from requirements over assumptions down to elements of evidence, be it in
the models, the code, or the tests. In a certification process, traceability becomes a major
concern; and providing mechanisms to ensure complete traceability already at the development of
the global document will clearly increase speed and reduce risk and cost of a certification
process. Making the link-structure machine-checkable, be it between requirements, assumptions,
their implementation and their discharge by evidence (be it tests, proofs, or authoritative
arguments), is therefore natural and has the potential to decrease the cost of developments
targeting certifications. Continuously checking the links between the formal and the semi-formal
parts of such documents is particularly valuable during the (usually collaborative) development
effort.
As in many other cases, formal certification documents come with an own terminology and pragmatics
of what has to be demonstrated and where, and how the trace-ability of requirements through
design-models over code to system environment assumptions has to be assured.
In the sequel, we present a simplified version of an ontological model used in a
case-study~@{cite "bezzecchi.ea:making:2018"}. We start with an introduction of the concept of
requirement:
2020-09-08 05:18:01 +00:00
@{boxed_theory_text [display]\<open>
2019-07-17 19:10:18 +00:00
doc_class requirement = long_name :: "string option"
doc_class requirement_analysis = no :: "nat"
where "requirement_item +"
doc_class hypothesis = requirement +
hyp_type :: hyp_type <= physical (* default *)
datatype ass_kind = informal | semiformal | formal
doc_class assumption = requirement +
assumption_kind :: ass_kind <= informal
2020-09-08 05:18:01 +00:00
\<close>}
2019-08-04 19:06:45 +00:00
2019-07-17 19:10:18 +00:00
Such ontologies can be enriched by larger explanations and examples, which may help
the team of engineers substantially when developing the central document for a certification,
like an explication what is precisely the difference between an \<^emph>\<open>hypothesis\<close> and an
\<^emph>\<open>assumption\<close> in the context of the evaluation standard. Since the PIDE makes for each
document class its definition available by a simple mouse-click, this kind on meta-knowledge
can be made far more accessible during the document evolution.
For example, the term of category \<^emph>\<open>assumption\<close> is used for domain-specific assumptions.
It has formal, semi-formal and informal sub-categories. They have to be
tracked and discharged by appropriate validation procedures within a
certification process, by it by test or proof. It is different from a hypothesis, which is
globally assumed and accepted.
In the sequel, the category \<^emph>\<open>exported constraint\<close> (or \<^emph>\<open>ec\<close> for short)
is used for formal assumptions, that arise during the analysis,
design or implementation and have to be tracked till the final
evaluation target, and discharged by appropriate validation procedures
within the certification process, by it by test or proof. A particular class of interest
is the category \<^emph>\<open>safety related application condition\<close> (or \<^emph>\<open>srac\<close>
for short) which is used for \<^emph>\<open>ec\<close>'s that establish safety properties
of the evaluation target. Their track-ability throughout the certification
is therefore particularly critical. This is naturally modeled as follows:
2020-09-08 05:18:01 +00:00
@{boxed_theory_text [display]\<open>
2019-07-17 19:10:18 +00:00
doc_class ec = assumption +
assumption_kind :: ass_kind <= (*default *) formal
doc_class srac = ec +
assumption_kind :: ass_kind <= (*default *) formal
2020-09-08 05:18:01 +00:00
\<close>}
2019-07-17 19:10:18 +00:00
2020-08-26 15:08:45 +00:00
We now can, \<^eg>, write
2019-08-04 17:15:30 +00:00
2020-09-08 05:18:01 +00:00
@{boxed_theory_text [display]\<open>
text*[ass123::SRAC]\<open>
2019-08-04 19:06:45 +00:00
The overall sampling frequence of the odometer subsystem is therefore
14 khz, which includes sampling, computing a$$nd result communication
times \ldots
2020-09-08 05:18:01 +00:00
\<close>
\<close>}
2019-08-04 17:15:30 +00:00
2019-08-04 19:06:45 +00:00
This will be shown in the PDF as follows:
\<close>
text*[ass123::SRAC] \<open> The overall sampling frequence of the odometer
subsystem is therefore 14 khz, which includes sampling, computing and
result communication times \ldots \<close>
subsection*[ontopide::technical]\<open>Editing Support for CENELEC 50128\<close>
figure*[figfig3::figure,relative_width="95",src="''figures/antiquotations-PIDE''"]
2019-08-04 17:15:30 +00:00
\<open> Standard antiquotations referring to theory elements.\<close>
2020-04-09 21:58:58 +00:00
text\<open> The corresponding view in @{docitem \<open>figfig3\<close>} shows core part of a document
2019-08-04 19:06:45 +00:00
conformimg to the CENELEC 50128 ontology. The first sample shows standard Isabelle antiquotations
2020-04-08 20:40:34 +00:00
@{cite "wenzel:isabelle-isar:2020"} into formal entities of a theory. This way, the informal parts
2019-08-04 19:06:45 +00:00
of a document get ``formal content'' and become more robust under change.\<close>
2019-08-04 17:15:30 +00:00
2019-08-04 19:06:45 +00:00
figure*[figfig5::figure, relative_width="95", src="''figures/srac-definition''"]
\<open> Defining a SRAC reference \ldots \<close>
figure*[figfig7::figure, relative_width="95", src="''figures/srac-as-es-application''"]
\<open> Using a SRAC as EC document reference. \<close>
2020-04-09 21:58:58 +00:00
text\<open> The subsequent sample in @{docitem \<open>figfig5\<close>} shows the definition of an
2019-08-04 17:15:30 +00:00
\<^emph>\<open>safety-related application condition\<close>, a side-condition of a theorem which
has the consequence that a certain calculation must be executed sufficiently fast on an embedded
device. This condition can not be established inside the formal theory but has to be
2020-04-09 21:58:58 +00:00
checked by system integration tests. Now we reference in @{docitem \<open>figfig7\<close>} this
2019-08-04 19:06:45 +00:00
safety-related condition; however, this happens in a context where general \<^emph>\<open>exported constraints\<close>
2020-08-26 15:08:45 +00:00
are listed. \<^isadof>'s checks establish that this is legal in the given ontology.
2019-08-04 19:34:22 +00:00
\<close>
2019-08-04 17:15:30 +00:00
2020-09-02 13:35:38 +00:00
(*
2019-08-04 19:34:22 +00:00
section*[math_exam::example]\<open>Writing Exams (math\_exam)\<close>
subsection\<open>The Math Exam Example\<close>
text\<open>
The ontology ``math\_exam''\index{ontology!math\_exam} is an experimental ontology modeling
the process of writing exams at higher education institution in the United Kingdom, where exams
2020-08-26 15:08:45 +00:00
undergo both an internal and external review process. The \<^isadof> distribution contains a tiny
2019-08-04 19:34:22 +00:00
example using the ontology ``math\_exam'' in the directory
\nolinkurl{examples/math_exam/MathExam/}. You can inspect/edit the example
in Isabelle's IDE, by either
2020-08-26 15:08:45 +00:00
\<^item> starting Isabelle/jedit using your graphical user interface (\<^eg>, by clicking on the
2019-08-04 19:34:22 +00:00
Isabelle-Icon provided by the Isabelle installation) and loading the file
\nolinkurl{examples/math_exam/MathExam/MathExam.thy}.
\<^item> starting Isabelle/jedit from the command line by calling:
\begin{bash}
ë\prompt{\isadofdirn}ë
isabelle jedit examples/math_exam/MathExam/MathExam.thy
\end{bash}
\<close>
text\<open>
You can build the PDF-document by calling:
\begin{bash}
ë\prompt{}ë isabelle build MathExam
\end{bash}
2019-07-17 13:41:03 +00:00
\<close>
2019-08-04 19:34:22 +00:00
subsection\<open>Modeling Exams\<close>
text\<open>
The math-exam scenario is an application with mixed formal and semi-formal content. It addresses
applications where the author of the exam is not present during the exam and the preparation
requires a very rigorous process.
We assume that the content has four different types of addressees, which have a different
\<^emph>\<open>view\<close> on the integrated document:
\<^item> the \<^emph>\<open>setter\<close>, \ie, the author of the exam,
\<^item> the \<^emph>\<open>checker\<close>, \ie, an internal person that checks
the exam for feasibility and non-ambiguity,
\<^item> the \<^emph>\<open>external\<close>, \ie, an external person that checks
the exam for feasibility and non-ambiguity, and
\<^item> the \<^emph>\<open>student\<close>, \ie, the addressee of the exam.
\<close>
text\<open>
The latter quality assurance mechanism is used in many universities,
where for organizational reasons the execution of an exam takes place in facilities
where the author of the exam is not expected to be physically present.
Furthermore, we assume a simple grade system (thus, some calculation is required). We
can model this as follows:
2019-07-17 13:41:03 +00:00
2020-09-08 05:18:01 +00:00
@{boxed_theory_text [display]\<open>
2019-07-17 13:41:03 +00:00
doc_class Author = ...
datatype Subject = algebra | geometry | statistical
datatype Grade = A1 | A2 | A3
doc_class Header = examTitle :: string
examSubject :: Subject
date :: string
timeAllowed :: int -- minutes
datatype ContentClass = setter
| checker
| external_examiner
| student
2019-08-04 19:34:22 +00:00
doc_class Exam_item = concerns :: "ContentClass set"
doc_class Exam_item = concerns :: "ContentClass set"
2019-07-17 13:41:03 +00:00
type_synonym SubQuestion = string
2020-09-08 05:18:01 +00:00
\<close>}
2019-08-04 19:34:22 +00:00
The heart of this ontology is an alternation of questions and answers, where the answers can
consist of simple yes-no answers or lists of formulas. Since we do not assume familiarity of
2020-09-08 06:30:14 +00:00
the students with Isabelle (\<^boxed_theory_text>\<open>term\<close> would assume that this is a parse-able and
2019-08-04 19:34:22 +00:00
type-checkable entity), we basically model a derivation as a sequence of strings:
2020-09-08 05:18:01 +00:00
@{boxed_theory_text [display]\<open>
2019-07-17 13:41:03 +00:00
doc_class Answer_Formal_Step = Exam_item +
justification :: string
"term" :: "string"
doc_class Answer_YesNo = Exam_item +
step_label :: string
yes_no :: bool -- \<open>for checkboxes\<close>
datatype Question_Type =
formal | informal | mixed
doc_class Task = Exam_item +
level :: Level
type :: Question_Type
subitems :: "(SubQuestion *
(Answer_Formal_Step list + Answer_YesNo) list) list"
concerns :: "ContentClass set" <= "UNIV"
mark :: int
doc_class Exercise = Exam_item +
type :: Question_Type
content :: "(Task) list"
concerns :: "ContentClass set" <= "UNIV"
mark :: int
2020-09-08 05:18:01 +00:00
\<close>}
2019-08-04 19:34:22 +00:00
In many institutions, having a rigorous process of validation for exam subjects makes sense: is
the initial question correct? Is a proof in the sense of the question possible? We model the
possibility that the @{term examiner} validates a question by a sample proof validated by Isabelle:
2020-09-08 05:18:01 +00:00
@{boxed_theory_text [display]\<open>
2019-07-17 13:41:03 +00:00
doc_class Validation =
tests :: "term list" <="[]"
proofs :: "thm list" <="[]"
doc_class Solution = Exam_item +
content :: "Exercise list"
valids :: "Validation list"
concerns :: "ContentClass set" <= "{setter,checker,external_examiner}"
doc_class MathExam=
content :: "(Header + Author + Exercise) list"
global_grade :: Grade
where "\<lbrace>Author\<rbrace>$^+$ ~~ Header ~~ \<lbrace>Exercise ~~ Solution\<rbrace>$^+$ "
2020-09-08 05:18:01 +00:00
\<close>}
2019-07-17 13:41:03 +00:00
2019-08-04 19:34:22 +00:00
In our scenario this sample proofs are completely \<^emph>\<open>intern\<close>, \ie, not exposed to the
students but just additional material for the internal review process of the exam.
\<close>
2019-08-05 10:05:19 +00:00
2020-09-02 13:35:38 +00:00
*)
2019-08-05 10:05:19 +00:00
section\<open>Style Guide\<close>
text\<open>
2020-08-26 15:08:45 +00:00
The document generation process of \<^isadof> is based on Isabelle's document generation framework,
using \<^LaTeX>{} as the underlying back-end. As Isabelle's document generation framework, it is
possible to embed (nearly) arbitrary \<^LaTeX>-commands in text-commands, \<^eg>:
2019-08-05 10:05:19 +00:00
2020-09-08 05:18:01 +00:00
@{boxed_theory_text [display]\<open>
text\<open> This is \emph{emphasized} a$$nd this is a
citation~\cite{brucker.ea:isabelle-ontologies:2018}\<close>
\<close>}
2019-08-05 10:05:19 +00:00
2020-08-26 15:08:45 +00:00
In general, we advise against this practice and, whenever positive, use the \<^isadof> (respetively
2019-08-05 10:05:19 +00:00
Isabelle) provided alternatives:
2020-09-08 05:18:01 +00:00
@{boxed_theory_text [display]\<open>
text\<open> This is *\<open>emphasized\<close> a$$nd this is a
citation <@>{cite "brucker.ea:isabelle-ontologies:2018"}.\<close>
\<close>}
2019-08-05 10:05:19 +00:00
2020-08-26 15:08:45 +00:00
Clearly, this is not always possible and, in fact, often \<^isadof> documents will contain
\<^LaTeX>-commands, this should be restricted to layout improvements that otherwise are (currently)
not possible. As far as possible, the use of \<^LaTeX>-commands should be restricted to the definition
2020-04-09 21:58:58 +00:00
of ontologies and document templates (see @{docitem (unchecked) \<open>isadof_ontologies\<close>}).
2019-08-05 10:05:19 +00:00
2020-08-26 15:08:45 +00:00
Restricting the use of \<^LaTeX> has two advantages: first, \<^LaTeX> commands can circumvent the
consistency checks of \<^isadof> and, hence, only if no \<^LaTeX> commands are used, \<^isadof> can
2019-08-05 10:05:19 +00:00
ensure that a document that does not generate any error messages in Isabelle/jedit also generated
2020-08-26 15:08:45 +00:00
a PDF document. Second, future version of \<^isadof> might support different targets for the
document generation (\<^eg>, HTML) which, naturally, are only available to documents not using
native \<^LaTeX>-commands.
2019-08-05 10:05:19 +00:00
Similarly, (unchecked) forward references should, if possible, be avoided, as they also might
create dangeling references during the document generation that break the document generation.
Finally, we recommend to use the @{command "check_doc_global"} command at the end of your
document to check the global reference structure.
2019-08-14 15:22:55 +00:00
2019-08-05 10:05:19 +00:00
\<close>
2019-08-14 15:22:55 +00:00
2019-07-17 13:41:03 +00:00
(*<*)
end
(*>*)
