Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Show more LaTeX log when there is an error


view this post on Zulip Email Gateway (Aug 19 2022 at 16:24):

From: Joachim Breitner <breitner@kit.edu>
Hi,

maybe my LaTeX is chattier that other people’s LaTeX, but I get:

$ isabelle build -D .
Running Cantor ...

Cantor FAILED
(see also /home/jojo/.isabelle/Isabelle2014/heaps/polyml-5.5.2_x86-linux/log/Cantor)

*** See the LaTeX manual or LaTeX Companion for explanation.
*** Type H <return> for immediate help.
*** ...


*** l.55 \end{document}


*** [2] (./root.aux) )
*** (see the transcript file for additional information)</usr/share/texlive/texmf-d
*** ist/fonts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fo
*** nts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/ty
*** pe1/public/amsfonts/cm/cmr10.pfb></usr/share/texlive/texmf-dist/fonts/type1/pub
*** lic/amsfonts/cm/cmr12.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/ams
*** fonts/cm/cmr17.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/c
*** m/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti
*** 10.pfb>
*** Output written on root.pdf (2 pages, 83996 bytes).
*** Transcript written on root.log.
*** Document preparation failure in directory 'output/document'


*** Failed to build document "/home/jojo/uni/info/Vorträge/2014-11-28 Computer Tools/output/document.pdf"
Unfinished session(s): Cantor
0:00:10 elapsed time, 0:00:17 cpu time, factor 1.70

which is quite unhelpful: The relevant lines are cut of by just 4
lines!

Maybe the build tool could be changed to show 10 or 20 lines more? Some
scrolling is definitely nicer than having to find the log file among
this outpu and copy’n’paste it.

And while we are at it: If the line mentioning the log file would be
printed _after_ the log excerpt it would be easier to spot.

Thanks!
Joachim
signature.asc

view this post on Zulip Email Gateway (Aug 19 2022 at 16:26):

From: Makarius <makarius@sketis.net>
What I usually do here is to open the "see also" file in the editor, and
do a hypersearch for "!" to find actual LaTeX errors. It is also possible
to keep that file open, and rely on jEdit to reload it automatically after
the next build (which can be done from Scala inside Isabelle/jEdit).

Generally, the Isabelle document preparation system is in need of some
substantial reforms. Now that the old TTY loop is already removed, there
are chances to re-open that topic eventually.

I would like to see LaTeX errors within the IDE, in the normal way
directly in the source. This is a bit difficult, because Don Knuth has
very strange ways to emit error messages. I need to study a bit more, how
other LaTeX IDEs do that, presumably with newer latex options like
-file-line-error.

If anybody is aware of existing solutions to extract (La)TeX errors from
the log file, I am very interested to see them.

Makarius


http://stop-ttip.org 925,332 people so far



Last updated: Apr 19 2024 at 01:05 UTC