*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] Presenting theories without running a session*From*: Robert Lamar <rlamar at stetson.edu>*Date*: Fri, 11 Feb 2011 16:16:11 +0000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <AANLkTin=YSyQNxL7_nYQ0J8F5_GB-gE9M+PpaPimUME0@mail.gmail.com>*References*: <AANLkTimCaf29TsJFJoCG0gON56Bt53iEoJDPohE+a2Cf@mail.gmail.com> <AANLkTin=YSyQNxL7_nYQ0J8F5_GB-gE9M+PpaPimUME0@mail.gmail.com>*Sender*: lamarmeister at gmail.com

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 >

**References**:**[isabelle] Presenting theories without running a session***From:*Robert Lamar

**Re: [isabelle] Presenting theories without running a session***From:*Brian Huffman

- Previous by Date: Re: [isabelle] formalization of non-classical logic in hilbert style
- Next by Date: [isabelle] Job Opportunities at Kestrel Institute
- Previous by Thread: Re: [isabelle] Presenting theories without running a session
- Next by Thread: Re: [isabelle] Presenting theories without running a session
- Cl-isabelle-users February 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list