Email Gateway (Aug 18 2022 at 18:49): Email Gateway (Aug 18 2022 at 18:49):From: Nemo <ncuriel@gmail.com>
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
Email Gateway (Aug 18 2022 at 18:50):From: Ramana Kumar <rk436@cam.ac.uk>
On Sat, Dec 3, 2011 at 7:30 PM, Nemo <ncuriel@gmail.com> 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 believe you should type that in a terminal.
I'm so confused.
Any help would be greatly appreciated.
Thank you so much.
Nemo Curiel
Email Gateway (Aug 18 2022 at 18:51):From: James Frank <james.isa@gmx.com>
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
test.zip
screenshot.1.png
Last updated: Apr 26 2024 at 20:16 UTC