Re: [isabelle] Latex / Isabelle (Beginner)



There are several ways to build documents. One way is with the IsaMakeFile. See page 19 of system.pdf, http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2011-1/doc/

Attached is a screenshot of the two commands I executed, and a zip file of the test files. Nothing's completely automated for you.

ME FIRST:

What I'm trying to do is execute

    "isabelle usdir -i true -g true HOL Thytest"

in the folder which contains my ROOT.ML, but it wants to change to folder /cygdrive/e/test/Thytest/Thytest, which doesn't exist.

If I do "isabelle usdir -i true -g true -b HOL Thytest", then it works, because of the "-b", but I don't want to build the heap when I'm importing a big theory, like Multivariate_Analysis. It takes forever to build.

YOU NOW:

You first go to the folder where you want to create the IsaMakeFile, for example, I'm working in /cygdrive/e/test, with a file named Thytest.thy.

Execute "isabelle mkdir HOL Thytest" in your current folder. It will do 3 things for you:
      Create the file IsaMakefile
      Create the file ./Thytest/ROOT.ML
      Create the folder and file ./Thytest/document/root.tex

Now, copy your .thy files to the new folder. I copied Thytest.thy to ./Thytest. It contains this:

    theory Thytest
    imports Main
    begin
    text{* This is a test. *}
    end

Next, edit your new ROOT.ML. I edited ./Thytest/ROOT.ML to look like this:

    (*
      no_document use_thys ["This_Theory1", "This_Theory2"];
      use_thys ["That_Theory1", "That_Theory2", "That_Theory3"];
    *)
    use_thys ["Thytest"];

Now, execute "isabelle make -B" in the folder containing your IsaMakeFile. It'll build all your session info in:
    ~/.isabelle/Isabelle2011-1/browser_info/HOL/Thytest

The "-B" forces it to build it.

CAVEAT:

Your system has to be set up correctly for LaTeX. If your .thy has no error in Proof General, i3p, or jEdit, it should build the HTML and session.graph, but you might get errors trying to build document.pdf.

So, to make sure LaTeX isn't causing problems, edit your IsaMakeFile, and remove the "-d pdf" from: USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -d pdf ## -D generated

If you can build HTML info, but not document.pdf, then you have LaTeX errors in your .thy, or your system's not set up correctly for LaTeX, such as not having the right packages.

LEARNING FROM THE SOURCE:

If you have success with the above, you can copy the "Isabelle-2011/src/HOL/document/root.tex" to your document folder and edit it to your liking.

--James











On 12/3/2011 1:30 PM, Nemo wrote:
Hello all,

I am new to extracting Latex files from Isabelle files. I read the
documentation but does not make sense to me. It says to use 'isabelle mkdir
NAME', but where do I even type this in? A terminal? Isabelle? Within a
file? Which?
I'm so confused.

Any help would be greatly appreciated.

Thank you so much.

Nemo Curiel


Attachment: test.zip
Description: Binary data

Attachment: screenshot.1.png
Description: PNG image



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