Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] isabelle build error message


view this post on Zulip Email Gateway (Aug 23 2022 at 08:20):

From: Gergely Buday <buday.gergely@uni-eszterhazy.hu>
Hi there,

when I run

isabelle build -D .

I get errors:

Running proofs ...
proofs FAILED
(see also C:\Users\gbuday\.isabelle\Isabelle2019\heaps\polyml-5.8_x86_64_32-windows\log\proofs)
Loading theory "proofs.Proofs"

theory "proof.Proofs"

0.016s elapsed time, 0.031s cpu time, 0.000s GC time

isabelle document -d output/document -o pdf -n document
*** D:\programok\texlive\2019\bin\win32\pdflatex.exe: unrecognized option `-c-style-errors'
*** Failed to build document in "/cygdrive/c/Users/gbuday/doctoral/papers/proofs/output/document"
Unfinished session(s): proofs
0:00:15 elapsed time

Unfortunately, these error messages does not tell me the real error. When I change directory into output/document and run

pdflatex root

I get

! Undefined control sequence.
<recently read> \<

l.214 definitional equality and implication: $\<
And> \<equiv> \<Longrightarr...

which is the real error.

Would it be a feature to include the LateX error message into isabelle build's output? The "-c-style-errors" is completely misleading.

view this post on Zulip Email Gateway (Aug 23 2022 at 08:20):

From: Makarius <makarius@sketis.net>
On 27/02/2020 10:50, Gergely Buday wrote:

isabelle document -d output/document -o pdf -n document
*** D:\programok\texlive\2019\bin\win32\pdflatex.exe: unrecognized option `-c-style-errors'
*** Failed to build document in "/cygdrive/c/Users/gbuday/doctoral/papers/proofs/output/document"

Unfortunately, these error messages does not tell me the real error.

I see an explicit error here: "unrecognized option `-c-style-errors'". It
means that you are using an unsupported LaTeX installation.

You should use
https://www.ctan.org/tex-archive/systems/win32/miktex

Would it be a feature to include the LateX error message into isabelle build's output? The "-c-style-errors" is completely misleading.

That very option "-c-style-errors" is there to get proper error messages that
can be relocated to the original Isabelle sources.

Makarius


Last updated: Mar 29 2024 at 01:04 UTC