Document preparation in Isabelle

Question

I want to use isabelle build -D xxx to produce a LaTeX .tex file out of an Isabelle .thy file. But Isabelle checks all the theory dependencies, and all the related .thy files must be involved.

Is it possible that I casually use a .thy file that has syntax errors to produce a .tex file? In fact I only need a part of it to write a paper.

Answer 1

To the best of my knowledge, no. The LaTeX generation requires the file to be processed successfully, e.g. due to notation (latex) commands, and due to antiquotations.

If you only need parts of your file, simply copy’n’paste it from the generated .tex file or, if you want something more automated, have a look at the Generate TeX Snippets wiki page.

Answer 2

Does that mean you want to write a paper based on a faulty or incomplete formal theory?

The Isabelle document preparation system was intended to publish formal theories that actually work out, with nice typography so that this does not look like "code". So all the defaults are for producing LaTeX from well-formed and checked theories.

Nonetheless, there are numerous ways to get unofficial LaTeX output from the system. A very basic mechanism is the latex print mode. Various diagnostic commands of Isabelle allow such print mode specifications in round parentheses, e.g. like this:

thm (latex) exI exE

or

print_statement (latex) exI exE

You can do this interactively and copy-paste the output into your raw tex file. You need to ensure that it gets proper surroundings with environments from the isabelle.sty file.