Re: [isabelle] Presenting theories without running a session



Hi Robert,

Due to the possibility of document antiquotations like @{thm foo},
generating the .tex file for a given .thy file is not trivial, and
depends on having access to the current theory database. So you will
need to run an Isabelle session.

You can speed things up a bit by running Isabelle in "skip proofs"
mode. Try adding commands to set the following two references before
"use_thys" in ROOT.ML:

quick_and_dirty := true;
Toplevel.skip_proofs := true;
use_thys ["MyTheory"];

This will cut running time by a fair amount. I do not know whether
there is a command-line option to do the same thing. (Although you can
make a separate copy of ROOT.ML file and select it with a "-f"
option.)

You can also save time by not saving a heap image. Run isabelle usedir
without the "-b" option (note that you may have to run "isabelle
usedir" from the parent directory for this to work).

- Brian

On Thu, Feb 10, 2011 at 12:31 PM, Robert Lamar <rlamar at stetson.edu> wrote:
> Hello, Isabelle users,
>
> I am curious about converting .thy files to .tex files without running a
> session to verify the document (with Isabelle 2011).  Is this possible?  I
> have been looking at the documentation for 'isabelle make', 'isabelle
> usedir', 'isabelle document', and 'isabelle latex', but I cannot conclude if
> producing LaTeX code depends on processing the documents, producing the
> heap, and so on.  Clearly, running the following is sufficient to produce
> the .tex files.  What is necessary?
>
> isabelle usedir -D generated HOL Foo





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.