See system.pdf ch. 3.

There are two options for generating documents from Isabelle proof sources; either (or both) can be used to showcase results.

• PDF (using $\LaTeX$)
  • standard academic LaTeX style
  • customizable, offers more control over presentation
    • specify LaTeX code for definitions (may differ from in-IDE presentation)
  • a single document; can be segmented into chapters, sections, ...
• HTML
  • close resemblance to viewing sources in Isabelle/jEdit
  • links facts to their definition
    • allows for session dependencies to be included/linked to
  • theories presented as separate pages

Generated HTML page	Theory source file in Isabelle/jEdit	Generated PDF document

For either option, defining and building a session is required. Running isabelle mkroot to create a stub ROOT is especially helpful, as it also creates an initial document/root.tex, required for PDF generation.

To build an existing session use isabelle build -B Session_Name (requires the session to be available to Isabelle) or isabelle build -D path/to/session (only works if the ROOT file is in the session base directory). In the following, only -B will be specified. Adding -v (verbose) to any build or document can help with identifying issues.

To debug document generation or whenever multiple subsequent builds are expected, it may be helpful to temporarily introduce a dummy parent session (session "My_Session" = "My_Dummy_Session" + ...) so that only the required theories need to be built each time.

To generate HTML files build the session with the browser_info system option: isabelle build -o browser_info -B Session_Name.
The generated files will be in $ISABELLE_HOME_USER/browser_info/Session_Group/Session_Name unless an output path is provided with -P path/to/output.
$ISABELLE_HOME_USER is typically ~/.isabelle/Isabelle<version> and the Session_Group is Unsorted unless specified in the session ROOT.

Uses of Isabelle entities (facts, terms) will link to their declaration/proof.

To generate and compile the LaTeX files:

1. Set up the session
   1. generate stubs for ROOT and document/root.tex by running isabelle mkroot path/to/session
   2. complete the ROOT file by adding theories
2. Register the session: isabelle components -u path/to/session
3. Build the session and generate the PDF: isabelle build -B Session_Name
   • Alternatively, run isabelle document -O path/to/output Session_Name

If the session was already set up without mkroot and is lacking the following entries, generating the PDF will fail silently:

session Session_Name = ...
  (* these `options` are not necessary when using `isabelle document ...` *)
  options [document = pdf, document_output = "output"]
  ...
  document_files
    "root.tex"

Note: The line numbers from errors occurring while compiling the generated LaTeX (Latex error (line 123 of "Some_Theory.tex"): ...) seem to reference lines in the theory file itself instead of the generated LaTeX (in this example, the issue appears in (or very close to) line 123 of Some_Theory.thy), which helps in debugging.

• Undefined control sequence for some math symbol.
  • Probably only missing an import;
    The document/root.tex generated by mkroot contains references to a few packages, but all are commented out. Uncomment relevant package imports.
  • To find out which package is required for a given symbol, consult the Detexify Symbol table or The Comprehensive $\LaTeX$ Symbol List
• Missing $ inserted / Extra }, or forgotten \endgroup
  • Possibly caused by special characters, such as $, _, or }, appearing in text (or \<comment>) environments.

Specifying more theories than necessary in the session ROOT may be useful, as theories will appear in the same order as they appear in the ROOT, unless this violates the dependency graph (if A imports B, then B can only appear before A).

Theories can also be excluded from the document while still being checked as part of the session, by listing them in separate theories [document = false] entries. This may be useful for tests and examples but is discouraged for theories containing definitions or proofs, as it could confuse readers. Note that this does not work for the HTML presentation, as pages will be generated for all files that are checked during the build.