Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Bad file 'root.tex'


view this post on Zulip Email Gateway (Aug 22 2022 at 20:37):

From: Walther Neuper <walther.neuper@jku.at>
We use Isabelle's document preparation first time.

In spite of ample documentation in isar-ref.pdf, system.pdf and
jedit.pdf we get stuck with the error message "Bad file 'root.tex'" and
cannot retrieve analogies from the mail archives.

Thus we try the same with a working example: first we go sure that file
access rights cannot get in the way

~~/src/Doc$ chmod -R u+w JEdit/
~~/src/Doc$ chmod -R u+x JEdit/

then we see, that here the following step must be skipped

~~/src/Doc/JEdit$ /usr/local/isabisac/bin/isabelle mkroot
*** Cannot overwrite existing "document"

so we cut the respective session out of ~~/src/Doc/ROOT, place it in
~~/src/Doc/JEdit/ROOT (see the attachment), create the directories

~~/src/Doc/JEdit$ mkdir output
~~/src/Doc/JEdit$ mkdir output/document

and finally see the same error

~~/src/Doc/JEdit$ /usr/local/isabisac/bin/isabelle document
Bad file 'root.tex'
Failed to build document in "~~/src/Doc/JEdit/output/document"

as we saw when doing analogous steps with our own files.

What are we doing wrong in the above sequence?

Thank you in advance for help!

Walther
ROOT

view this post on Zulip Email Gateway (Aug 22 2022 at 20:37):

From: Walther Neuper <walther.neuper@jku.at>
sorry for the noise

isabelle document preparation works as fine for me now as it does for
others; as an early adopter of tex I couldn't believe the extent of
automation provided y isabelle ;-))


Last updated: Nov 21 2024 at 12:39 UTC