Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] documentation

view this post on Zulip Email Gateway (Aug 18 2022 at 14:10):

From: barzan stefania <stefania_barzan@yahoo.com>
Dear Isabelle users,

I have been trying to make the pdf documentation for my theory.
After i creat my session called StefSession, to the command:

$ /usr/local/Isabelle/bin/isatool usedir -v true -i true -d pdf HOL StefSession

i get the following :

Running HOL-StefSession ...
Browser info at /home/stefania/isabelle/browser_info/HOL/StefSession
HOL-StefSession FAILED
(see also /home/stefania/isabelle/heaps/Isabelle2008/polyml_x86-cygwin/log/HOL-S
tefSession)

xmf/fonts/type1/bluesky/cm/cmsy10.pfb></usr/share/texmf/fonts/type1/bluesky/cm/
cmmi10.pfb></usr/share/texmf/fonts/type1/bluesky/cm/cmr10.pfb></usr/share/texmf
/fonts/type1/bluesky/cm/cmti10.pfb></usr/share/texmf/fonts/type1/bluesky/cm/cmb
x10.pfb></usr/share/texmf/fonts/type1/bluesky/cm/cmbx12.pfb></usr/share/texmf/f
onts/type1/bluesky/cm/cmr12.pfb></usr/share/texmf/fonts/type1/bluesky/cm/cmr17.
pfb>
Output written on root.pdf (266 pages, 859174 bytes).
Transcript written on root.log.
Document preparation failure in directory '/home/stefania/isabelle/browser_info/
HOL/StefSession/document'
*** No document: "/home/stefania/isabelle/browser_info/HOL/StefSession/document.
pdf"

Has anyone a solution for this error?

The second question i have is related with the keyword "includes" that exists in the 2008 version but is not anymore in 2009. Does it have a replacement?

Thank you in advance!

Stefania

view this post on Zulip Email Gateway (Aug 18 2022 at 14:10):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Stefania,

$ /usr/local/Isabelle/bin/isatool usedir -v true -i true -d pdf HOL StefSession

Running HOL-StefSession ...
Browser info at /home/stefania/isabelle/browser_info/HOL/StefSession
HOL-StefSession FAILED
(see also /home/stefania/isabelle/heaps/Isabelle2008/polyml_x86-cygwin/log/HOL-S
tefSession)

xmf/fonts/type1/bluesky/cm/cmsy10.pfb></usr/share/texmf/fonts/type1/bluesky/cm/
cmmi10.pfb></usr/share/texmf/fonts/type1/bluesky/cm/cmr10.pfb></usr/share/texmf
/fonts/type1/bluesky/cm/cmti10.pfb></usr/share/texmf/fonts/type1/bluesky/cm/cmb
x10.pfb></usr/share/texmf/fonts/type1/bluesky/cm/cmbx12.pfb></usr/share/texmf/f
onts/type1/bluesky/cm/cmr12.pfb></usr/share/texmf/fonts/type1/bluesky/cm/cmr17.
pfb>
Output written on root.pdf (266 pages, 859174 bytes).
Transcript written on root.log.
Document preparation failure in directory '/home/stefania/isabelle/browser_info/
HOL/StefSession/document'
*** No document: "/home/stefania/isabelle/browser_info/HOL/StefSession/document.
pdf"

It is often difficult to extract a particular problem from the verbose
output of the tex-related processes. Have you tried to inspect the log
file see also
/home/stefania/isabelle/heaps/Isabelle2008/polyml_x86-cygwin/log/HOL-StefSession?
It seems that this contains important clues what actually went wrong.

The second question i have is related with the keyword "includes" that exists in the 2008 version but is not anymore in 2009. Does it have a replacement?

The "includes" feature was sacrificed in favour of a refined locale
implementation; there is no one-to-one substitute. In which context
does "inludes" appear in your theories?

Hope this helps,
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 14:11):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Stefania,

Thank you for the hints but still i didn't solve the error.
I looked in log/HOL-StefSession file and the only error i fond is this:

Loading theory "Abstract"
val it = () : unit
val it = () : unit

Browser info: cannot access session index of

"/home/stefania/isabelle/browser_info/HOL"
"$ISATOOL" document -c -o 'pdf' -n 'document' -t ''
'/home/stefania/isabelle/browser_info/HOL/StefSession/document' 2>&1
This is pdfeTeXk, Version 3.141592-1.21a-2.2 (Web2C 7.5.4)
file:line:error style messages enabled.
%&-line parsing enabled.

Hmmm... can you send me the log (not via the mailing list please)?

About the "includes" command. i am using it for example in:

lemma(in comm_group) :
includes group G1+ group G2
assumes ....
shows...

In that case just use the corresponding locale predicate expressions as
assumptions, e.g. like in lemma subgroup_is_group in
src/HOL/Algebra/Group.thy:

lemma (in comm_group):
assumes "group G1" and "group G2"
fixes ...
assumes ...
shows ...

Hope this helps,
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 14:11):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Stefania,

the first error mistake is at line 10051.

It seems that you have (accidentally?) put some Isar text into text {*
*} sections, upon which tex will choke of course.

To debug such tex issues it can also be helpful to run tex manually on
the generated sources, usually by switching to the directory with the
generated sources and running pdflatex root.tex or something alike.

Hope this helps
Florian
signature.asc

Last updated: Apr 25 2024 at 04:18 UTC