(*:maxLineLen=78:*)
theory Presentation
imports Base
begin
chapter ‹Presenting theories
\label{ch:present}
›
text ‹
Isabelle provides several ways
to present the outcome of formal
developments, including WWW-based browsable libraries or actual printable
documents. Presentation
is centered around the concept of
🚫‹sessions
›
(
\chref{ch:session}). The
global session
structure is that of a tree,
with
Isabelle Pure at its root, further object-logics derived (e.g.
\ HOLCF
from
HOL,
and HOL
from Pure),
and application sessions further on
in the
hierarchy.
The command-line tools @{tool_ref mkroot}
and @{tool_ref build} provide the
primary means
for managing Isabelle sessions, including options
for
presentation: ``
🍋‹document=pdf
›'' generates PDF
output from the
theory
session,
and ``
🍋‹document_output=dir
›'' emits a copy of the document sources
with the PDF into the given directory (relative
to the session directory).
Alternatively, @{tool_ref document} may be used
to turn the generated
{
\LaTeX} sources of a session (exports
from its session build database) into PDF.
›
section
‹Generating HTML browser information
\label{sec:info}
›
text ‹
As a side-effect of building sessions, Isabelle
is able
to generate
theory
browsing information, including HTML documents that
show the
theory sources
and the relationship
with its ancestors
and descendants. Besides the HTML
file that
is generated
for every
theory, Isabelle stores links
to all
theories of a session
in an index
file. As a second hierarchy, groups of
sessions are organized as
🚫‹chapters
›,
with a separate index.
Note that the
implicit tree
structure of the session build hierarchy
is 🚫‹not
› relevant
for the presentation.
🚫
To generate
theory browsing information
for an existing session, just
invoke
@{tool build}
with suitable options:
@{verbatim [display]
‹isabelle build -o browser_info -v -c FOL
›}
The presentation
output will appear
in a sub-directory
🍋‹$ISABELLE_BROWSER_INFO
›, according
to the
chapter and session name.
Many Isabelle sessions (such as
🚫‹HOL-Library
› in
🍋‹~~/src/HOL/Library
›)
also provide
theory documents
in PDF. These are
prepared automatically as well
if enabled like this:
@{verbatim [display]
‹isabelle build -o browser_info -o document -v -c HOL-Library
›}
Enabling both browser info
and document preparation simultaneously causes an
appropriate ``document
'' link
to be included
in the HTML index. Documents
may be generated independently of browser information as well, see
\secref{sec:tool-document}
for further details.
🚫
The
theory browsing information
is stored
in the directory determined
by the
@{setting_ref ISABELLE_BROWSER_INFO} setting,
with sub-directory
structure
according
to the
chapter and session name.
In order
to present Isabelle
applications on the web, the corresponding subdirectory
from @{setting
ISABELLE_BROWSER_INFO} can be put on a WWW server.
›
section
‹Creating session root directories
\label{sec:tool-mkroot}
›
text ‹
The @{tool_def mkroot} tool configures a given directory as session root,
with some
🍋‹ROOT
› file and optional document source directory. Its usage
is:
@{verbatim [display]
‹Usage: isabelle mkroot [OPTIONS] [DIRECTORY]
Options are:
-A LATEX provide author
in LaTeX
notation (default: user name)
-I init Mercurial repository
and add generated files
-T LATEX provide title
in LaTeX
notation (default: session name)
-n NAME alternative session name (default: directory base name)
-q quiet mode: less verbosity
Create session root directory (default: current directory).
›}
The results are placed
in the given directory
‹dir
›, which refers
to the
current directory
by default. The @{tool mkroot} tool
is conservative
in the
sense that it does not overwrite existing files or directories. Earlier
attempts
to generate a session root need
to be deleted manually.
The generated session template will be accompanied
by a formal document,
with ‹DIRECTORY
›🍋‹/document/root.tex
› as its {
\LaTeX} entry point (see
also
\chref{ch:present}).
Options
🍋‹-T
› and 🍋‹-A
› specify the document title
and author explicitly,
using {
\LaTeX} source
notation.
Option
🍋‹-I
› initializes a Mercurial repository
in the target directory,
and
adds all generated files (without
commit).
Option
🍋‹-n
› specifies an alternative session name;
otherwise the base name
of the given directory
is used.
Option
🍋‹-q
› reduces verbosity.
🚫
The implicit Isabelle settings variable @{setting ISABELLE_LOGIC} specifies
the parent session.
›
subsubsection
‹Examples
›
text ‹
Produce session
🍋‹Test
› within a separate directory of the same name:
@{verbatim [display]
‹isabelle mkroot -q Test && isabelle build -D Test
›}
🚫
Upgrade the current directory into a session ROOT
with document preparation,
and build it:
@{verbatim [display]
‹isabelle mkroot -q && isabelle build -D .
›}
›
section
‹Preparing Isabelle session documents
\label{sec:tool-document}
›
text ‹
The @{tool_def document} tool prepares logic session documents. Its usage
is:
@{verbatim [display]
‹Usage: isabelle document [OPTIONS] SESSION
Options are:
-O DIR
output directory
for LaTeX sources
and resulting PDF
-P DIR
output directory
for resulting PDF
-S DIR
output directory
for LaTeX sources
-V verbose latex
-d DIR include session directory
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-v verbose build
Prepare the
theory document of a session.
›}
Generated {
\LaTeX} sources are taken
from the session build database:
@{tool_ref build}
is invoked beforehand
to ensure that it
is up-to-date.
Further files are generated on the spot, notably essential Isabelle style
files,
and 🍋‹session.tex
› to input all
theory sources
from the session
(excluding
imports from other sessions).
🚫 Options
🍋‹-d
›,
🍋‹-o
›,
🍋‹-v
› have the same meaning as
for @{tool
build}.
🚫 Option
🍋‹-V
› prints full
output of {
\LaTeX} tools.
🚫 Option
🍋‹-O
›~
‹dir
› specifies the
output directory
for generated {
\LaTeX}
sources
and the result PDF
file. Options
🍋‹-P
› and 🍋‹-S
› only refer
to the
PDF
and sources, respectively.
For example,
for output directory ``
🍋‹output›'' and the default document
variant ``
🍋‹document
›'', the generated document sources are placed into the
subdirectory
🍋‹output/document/
› and the resulting PDF into
🍋‹output/document.pdf
›.
🚫 Isabelle
is usually smart enough
to create the PDF
from the given
🍋‹root.tex
› and optional
🍋‹root.bib
› (bibliography)
and 🍋‹root.idx
› (index)
using standard {
\LaTeX} tools. Actual command-lines are given
by settings
@{setting_ref ISABELLE_LUALATEX} (or @{setting_ref ISABELLE_PDFLATEX}),
@{setting_ref ISABELLE_BIBTEX}, @{setting_ref ISABELLE_MAKEINDEX}: these
variables are used without quoting
in shell scripts,
and thus may contain
additional options.
The system option @{system_option_def
"document_build"} specifies an
alternative build engine, e.g. within the session
🍋‹ROOT
› file as
``
🍋‹options [document_build = pdflatex]
›''. The following standard engines
are available:
🚫 🍋‹lualatex
› (default)
uses the shell command
🍋‹$ISABELLE_LUALATEX
› on
the main
🍋‹root.tex
› file,
with further runs of
🍋‹$ISABELLE_BIBTEX
› and
🍋‹$ISABELLE_MAKEINDEX
› as required.
🚫 🍋‹pdflatex
› uses 🍋‹$ISABELLE_PDFLATEX
› instead of
🍋‹$ISABELLE_LUALATEX
›,
and the other tools as above.
🚫 🍋‹build
› invokes an executable script of the same name
in a private
directory containing all
\isakeyword{document
\_files}
and other generated
document sources. The script
is invoked as ``
🍋‹./build pdf
›~
‹name
›'' for
the document variant name; it needs
to produce a corresponding
‹name
›🍋‹.pdf
› file by arbitrary means on its own.
Further engines can be defined
by add-on components
in Isabelle/Scala
(
\secref{sec:scala-build}), providing a service
class derived
from
🍋‹isabelle.Document_Build.Engine
›.
›
subsubsection
‹Examples
›
text ‹
Produce the document
from session
🍋‹FOL
› with full verbosity,
and a copy
in
the current directory (subdirectory
🍋‹document
› and file 🍋‹document.pdf)
›:
@{verbatim [display]
‹isabelle document -v -V -O. FOL
›}
›
section
‹Full-text search
for formal
theory content
›
text ‹
The session information of a regular @{tool_ref build} can
also be used
to
generate a search index
for full-text search over formal
theory content.
To
that
end, the
🍋‹Find_Facts
› module integrates Apache Solr
🚫‹🚫‹https://solr.apache.org››,
a full-text search engine, that can run embedded
in a JVM process. Solr
is
bundled as a separate Isabelle component,
and its run-time dependencies
(as specified
in @{setting SOLR_JARS}) need
to be added separately
to the
classpath of a regular Isabelle/Scala process.
🚫
A search index can be created
using the @{tool_def find_facts_index} tool,
which has options similar
to the regular @{tool_ref build}. User data such
as search indexes
is stored
in @{setting FIND_FACTS_HOME_USER}. The name of
the search index can be specified via system option
@{system_option find_facts_database_name}. A finished search index can be
packed
for later
use as a regular Isabelle component
using the
@{tool_def find_facts_index_build} tool,
with a
🍋‹.db
› file and
🍋‹etc/settings
› to augment @{setting FIND_FACTS_INDEXES}
for use by @{tool
find_facts_server}.
🚫
The user interface of the search
is available as web application that
can be started
with the @{tool_def find_facts_server} tool. Its usage
is:
@{verbatim [display]
‹Usage: isabelle find_facts_server [OPTIONS]
Options are:
-d devel mode
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-p PORT explicit web server port
-v verbose server
Run server
for Find_Facts.
›}
This Isabelle/Scala HTTP server provides the both the front-end
(implemented
in the Elm
🚫‹🚫‹https://elm-lang.org›› language)
and REST
endpoints
for search queries
with JSON data.
Options
🍋‹-o
› and 🍋‹-v
› have the same meaning as
in @{tool build}.
Option
🍋‹-d
› re-compiles the front-end
in 🍋‹$FIND_FACTS_HOME_USER/web
›
on page reload (when sources are changed).
Option
🍋‹-p
› specifies an explicit TCP port
for the server socket (assigned
by the operating system per default).
For public-facing servers, a common
scheme
is 🍋‹-p 8080
› that
is access-restricted via firewall rules,
with a
reverse proxy
🚫‹E.g. via Caddy
🚫‹https://caddyserver.com/docs›› in system
space (that
also handles SSL) on ports 80
and 443.
›
end
