Email Gateway (Aug 23 2022 at 08:20): 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"
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.
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: Nov 21 2024 at 12:39 UTC