Re: [isabelle] Presenting theories without running a session



Hello Brian,

Very interesting.  Thank you for your thoughts on the matter.

As I think about it, the Isabelle session will also determine the
dependencies between theories, and thus the order that they will appear in
session.tex.  I am not suprised to hear that the document preparation system
relies heavily on the results of an Isabelle session; I suppose I was just
writing in to confirm that this was the case.

Robert

On Fri, Feb 11, 2011 at 12:32 AM, Brian Huffman <brianh at cs.pdx.edu> wrote:

> 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.